MAJ terminée. Nous sommes passés en version 14.6.2 . Pour consulter les "releases notes" associées c'est ici :

https://about.gitlab.com/releases/2022/01/11/security-release-gitlab-14-6-2-released/
https://about.gitlab.com/releases/2022/01/04/gitlab-14-6-1-released/

Commit 0bc219e9 authored by Sylvain Dailler's avatar Sylvain Dailler
Browse files

printer: put arguments cntexample into info.

parent 4385c3e0
......@@ -50,6 +50,7 @@ type info = {
mutable info_in_goal: bool;
mutable list_projs: Stdlib.Sstr.t;
meta_model_projection: Sls.t;
info_cntexample: bool
}
let ident_printer () =
......@@ -389,10 +390,10 @@ let print_logic_decl info fmt (ls,ld) =
if Mid.mem ls.ls_name info.info_syn || Sls.mem ls info.info_pjs
then () else (print_logic_decl info fmt ls ld; forget_tvs info)
let print_info_model cntexample info =
let print_info_model info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if not (S.is_empty info_model) && cntexample then
if not (S.is_empty info_model) && info.info_cntexample then
begin
let model_map =
S.fold (fun f acc ->
......@@ -410,13 +411,13 @@ let print_info_model cntexample info =
else
Stdlib.Mstr.empty
let print_prop_decl vc_loc cntexample args info fmt k pr f =
let print_prop_decl vc_loc args info fmt k pr f =
match k with
| Paxiom ->
fprintf fmt "@[<hov 2>axiom %a :@ %a@]@\n@\n"
(print_ident info) pr.pr_name (print_fmla info) f
| Pgoal ->
let model_list = print_info_model cntexample info in
let model_list = print_info_model info in
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
queried_terms = model_list;
......@@ -426,11 +427,11 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f =
(print_ident info) pr.pr_name (print_fmla info) f
| Plemma| Pskip -> assert false
let print_prop_decl vc_loc cntexample args info fmt k pr f =
let print_prop_decl vc_loc args info fmt k pr f =
if Mid.mem pr.pr_name info.info_syn || Spr.mem pr info.info_axs
then () else (print_prop_decl vc_loc cntexample args info fmt k pr f; forget_tvs info)
then () else (print_prop_decl vc_loc args info fmt k pr f; forget_tvs info)
let print_decl vc_loc cntexample args info fmt d = match d.d_node with
let print_decl vc_loc args info fmt d = match d.d_node with
| Dtype ts ->
print_ty_decl info fmt ts
| Ddata dl ->
......@@ -442,7 +443,7 @@ let print_decl vc_loc cntexample args info fmt d = match d.d_node with
print_list nothing (print_logic_decl info) fmt dl
| Dind _ -> unsupportedDecl d
"alt-ergo: inductive definitions are not supported"
| Dprop (k,pr,f) -> print_prop_decl vc_loc cntexample args info fmt k pr f
| Dprop (k,pr,f) -> print_prop_decl vc_loc args info fmt k pr f
let add_projection (csm,pjs,axs) = function
| [Theory.MAls ls; Theory.MAls cs; Theory.MAint ind; Theory.MApr pr] ->
......@@ -482,6 +483,7 @@ let print_task args ?old:_ fmt task =
info_in_goal = false;
list_projs = Stdlib.Sstr.empty;
meta_model_projection = Task.on_tagged_ls meta_projection task;
info_cntexample = cntexample;
} in
print_prelude fmt args.prelude;
print_th_prelude task fmt args.th_prelude;
......@@ -490,7 +492,7 @@ let print_task args ?old:_ fmt task =
print_decls t.Task.task_prev;
begin match t.Task.task_decl.Theory.td_node with
| Theory.Decl d ->
begin try print_decl vc_loc cntexample args info fmt d
begin try print_decl vc_loc args info fmt d
with Unsupported s -> raise (UnsupportedDecl (d,s)) end
| _ -> () end
| None -> () in
......
......@@ -130,6 +130,7 @@ type info = {
meta_model_projection : Sls.t;
mutable list_records : ((string * string) list) Stdlib.Mstr.t;
info_cntexample_need_push : bool;
info_cntexample: bool
}
let debug_print_term message t =
......@@ -475,10 +476,10 @@ let print_logic_decl info fmt (ls,def) =
List.iter (forget_var info) vsl
end
let print_info_model cntexample fmt info =
let print_info_model fmt info =
(* Prints the content of info.info_model *)
let info_model = info.info_model in
if not (S.is_empty info_model) && cntexample then
if not (S.is_empty info_model) && info.info_cntexample then
begin
fprintf fmt "@[(get-model ";
let model_map =
......@@ -498,7 +499,7 @@ let print_info_model cntexample fmt info =
else
Stdlib.Mstr.empty
let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
let print_prop_decl vc_loc args info fmt k pr f = match k with
| Paxiom ->
fprintf fmt "@[<hov 2>;; %s@\n(assert@ %a)@]@\n@\n"
pr.pr_name.id_string (* FIXME? collisions *)
......@@ -513,9 +514,9 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
info.info_in_goal <- true;
fprintf fmt " @[(not@ %a))@]@\n" (print_fmla info) f;
info.info_in_goal <- false;
if cntexample && info.info_cntexample_need_push then fprintf fmt "@[(push)@]@\n";
if info.info_cntexample && info.info_cntexample_need_push then fprintf fmt "@[(push)@]@\n";
fprintf fmt "@[(check-sat)@]@\n";
let model_list = print_info_model cntexample fmt info in
let model_list = print_info_model fmt info in
args.printer_mapping <- { lsymbol_m = args.printer_mapping.lsymbol_m;
vc_term_loc = vc_loc;
......@@ -570,7 +571,7 @@ let print_data_decl info fmt (ts,cl) =
(print_ident info) ts.ts_name
(print_list space (print_constructor_decl info)) cl
let print_decl vc_loc cntexample args info fmt d =
let print_decl vc_loc args info fmt d =
match d.d_node with
| Dtype ts ->
print_type_decl info fmt ts
......@@ -587,10 +588,10 @@ let print_decl vc_loc cntexample args info fmt d =
"smtv2: inductive definitions are not supported"
| Dprop (k,pr,f) ->
if Mid.mem pr.pr_name info.info_syn then () else
print_prop_decl vc_loc cntexample args info fmt k pr f
print_prop_decl vc_loc args info fmt k pr f
let set_produce_models fmt cntexample =
if cntexample then
let set_produce_models fmt info =
if info.info_cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let meta_counterexmp_need_push =
......@@ -617,17 +618,18 @@ let print_task args ?old:_ fmt task =
meta_model_projection = Task.on_tagged_ls meta_projection task;
list_records = Stdlib.Mstr.empty;
info_cntexample_need_push = need_push;
info_cntexample = cntexample;
}
in
print_prelude fmt args.prelude;
set_produce_models fmt cntexample;
set_produce_models fmt info;
print_th_prelude task fmt args.th_prelude;
let rec print_decls = function
| Some t ->
print_decls t.Task.task_prev;
begin match t.Task.task_decl.Theory.td_node with
| Theory.Decl d ->
begin try print_decl vc_loc cntexample args info fmt d
begin try print_decl vc_loc args info fmt d
with Unsupported s -> raise (UnsupportedDecl (d,s)) end
| _ -> () end
| None -> () in
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment