Skip to content

GitLab

Commit 4035a124 authored by Martin Clochard's avatar Martin Clochard
Browse files

Merge branch 'master' of git+ssh://scm.gforge.inria.fr//gitroot/why3/why3

parents e6f2f3ff bb4e54da
Hide whitespace changes
Inline Side-by-side
Showing with 95 additions and 87 deletions
drivers/z3_432.drv
View file @ 4035a124
......@@ -77,6 +77,8 @@ end
*)
(* REMOVED: we do not use BV theory from Z3 in 4.3.2 but starting from 4.4.0
(* bitvector modules, is not in smt-libv2.drv since cvc4 and z3 don't
have the same name for the function to_uint *)
theory bv.BV64
......@@ -98,3 +100,5 @@ theory bv.BV8
syntax converter of_int "((_ int2bv 8) %1)"
syntax function to_uint "(bv2int %1)"
end
*)
\ No newline at end of file
plugins/tptp/tptp_printer.ml
View file @ 4035a124
......@@ -263,28 +263,30 @@ let print_decl info fmt d = match d.d_node with
head print_pr pr (print_fmla info) f
| Dprop ((Plemma|Pskip), _, _) -> assert false
let print_decls fm nm rew_rules =
let print_decls fm nm =
(*
Format.eprintf "rewrite rules:";
Spr.iter (fun pr -> Format.eprintf " %s" pr.pr_name.id_string) rew_rules;
Format.eprintf "@.";
*)
let print_decl (sm,fm,ct) fmt d =
let print_decl (sm,fm,rr,ct) fmt d =
let info = { info_syn = sm;
info_fmt = fm;
info_num = nm;
info_srt = ref ct;
info_urg = ref [];
info_rules = rew_rules } in
info_rules = rr } in
try print_decl info fmt d;
(sm,fm,!(info.info_srt)), !(info.info_urg)
(sm,fm,rr,!(info.info_srt)), !(info.info_urg)
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Trans.fold print_decl ((sm,fm,Mty.empty),[]))
Trans.on_tagged_pr Compute.meta_rewrite (fun rr ->
Trans.fold print_decl ((sm,fm,rr,Mty.empty),[])))
let print_task fm nm =
let print_decls = print_decls fm nm in
fun args ?old:_ fmt task ->
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
......@@ -293,10 +295,7 @@ let print_task fm nm =
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
let print_decls_with_meta =
Trans.on_tagged_pr Compute.meta_rewrite (print_decls fm nm)
in
print (snd (Trans.apply print_decls_with_meta task));
print (snd (Trans.apply print_decls task));
pp_print_flush fmt ()
let () =
......
share/provers-detection-data.conf
View file @ 4035a124
......@@ -355,7 +355,6 @@ name = "Z3"
exec = "z3-4.3.2"
version_switch = "-version"
version_regexp = "Z3 version \\([^ \n\r]+\\)"
version_ok = "4.4.0"
version_ok = "4.3.2"
driver = "drivers/z3_432.drv"
command = "%e -smt2 sat.random_seed=42 nlsat.randomize=false smt.random_seed=42 %f"
......
src/printer/smtv2.ml
View file @ 4035a124
......@@ -24,7 +24,7 @@ let debug = Debug.register_info_flag "smtv2_printer"
the@ input@ of@ smtv2."
(** SMTLIB tokens taken from CVC4: src/parser/smt2/Smt2.g *)
let ident_printer =
let ident_printer () =
let bls = (*["and";" benchmark";" distinct";"exists";"false";"flet";"forall";
"if then else";"iff";"implies";"ite";"let";"logic";"not";"or";
"sat";"theory";"true";"unknown";"unsat";"xor";
......@@ -77,9 +77,6 @@ let ident_printer =
let san = sanitizer char_to_alpha char_to_alnumus in
create_ident_printer bls ~sanitizer:san
let print_ident fmt id =
fprintf fmt "%s" (id_unique ident_printer id)
(* Information about the term that triggers VC. *)
type vc_term_info = {
mutable vc_inside : bool;
......@@ -128,6 +125,7 @@ type info = {
mutable info_model : S.t;
mutable info_in_goal : bool;
info_vc_term : vc_term_info;
info_printer : ident_printer;
}
let debug_print_term message t =
......@@ -139,14 +137,17 @@ let debug_print_term message t =
Debug.dprintf debug "@.";
end
let print_ident info fmt id =
fprintf fmt "%s" (id_unique info.info_printer id)
(** type *)
let rec print_type info fmt ty = match ty.ty_node with
| Tyvar _ -> unsupported "smt : you must encode the polymorphism"
| Tyapp (ts, l) ->
begin match query_syntax info.info_syn ts.ts_name, l with
| Some s, _ -> syntax_arguments s (print_type info) fmt l
| None, [] -> fprintf fmt "%a" print_ident ts.ts_name
| None, _ -> fprintf fmt "(%a %a)" print_ident ts.ts_name
| None, [] -> fprintf fmt "%a" (print_ident info) ts.ts_name
| None, _ -> fprintf fmt "(%a %a)" (print_ident info) ts.ts_name
(print_list space (print_type info)) l
end
......@@ -158,14 +159,14 @@ let print_type_value info fmt = function
| Some ty -> print_type info fmt ty
(** var *)
let forget_var v = forget_id ident_printer v.vs_name
let forget_var info v = forget_id info.info_printer v.vs_name
let print_var fmt {vs_name = id} =
let n = id_unique ident_printer id in
let print_var info fmt {vs_name = id} =
let n = id_unique info.info_printer id in
fprintf fmt "%s" n
let print_typed_var info fmt vs =
fprintf fmt "(%a %a)" print_var vs
fprintf fmt "(%a %a)" (print_var info) vs
(print_type info) vs.vs_ty
let print_var_list info fmt vsl =
......@@ -310,7 +311,7 @@ let rec print_term info fmt t =
Number.def_real_support = Number.Number_unsupported;
} in
Number.print number_format fmt c
| Tvar v -> print_var fmt v
| Tvar v -> print_var info fmt v
| Tapp (ls, tl) ->
(* let's check if a converter applies *)
begin try
......@@ -343,16 +344,17 @@ let rec print_term info fmt t =
(*info.info_model <- add_model_element t_check_pos info.info_model;*)
()
end;
fprintf fmt "@[%a@]" print_ident ls.ls_name
fprintf fmt "@[%a@]" (print_ident info) ls.ls_name
| _ ->
fprintf fmt "@[(%a@ %a)@]"
print_ident ls.ls_name (print_list space (print_term info)) tl
(print_ident info) ls.ls_name
(print_list space (print_term info)) tl
end end
| Tlet (t1, tb) ->
let v, t2 = t_open_bound tb in
fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
fprintf fmt "@[(let ((%a %a))@ %a)@]" (print_var info) v
(print_term info) t1 (print_term info) t2;
forget_var v
forget_var info v
| Tif (f1,t1,t2) ->
fprintf fmt "@[(ite %a@ %a@ %a)@]"
(print_fmla info) f1 (print_term info) t1 (print_term info) t2
......@@ -368,9 +370,9 @@ let rec print_term info fmt t =
| _ ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_var info) subject (print_term info) t
(print_branches info subject print_term) bl;
forget_var subject
forget_var info subject
end
| Teps _ -> unsupportedTerm t
"smtv2: you must eliminate epsilon"
......@@ -389,14 +391,15 @@ and print_fmla info fmt f =
let () = match f.t_node with
| Tapp ({ ls_name = id }, []) ->
print_ident fmt id
print_ident info fmt id
| Tapp (ls, tl) -> begin match query_syntax info.info_syn ls.ls_name with
| Some s -> syntax_arguments_typed s (print_term info)
(print_type info) f fmt tl
| None -> begin match tl with (* for cvc3 wich doesn't accept (toto ) *)
| [] -> fprintf fmt "%a" print_ident ls.ls_name
| [] -> print_ident info fmt ls.ls_name
| _ -> fprintf fmt "(%a@ %a)"
print_ident ls.ls_name (print_list space (print_term info)) tl
(print_ident info) ls.ls_name
(print_list space (print_term info)) tl
end end
| Tquant (q, fq) ->
let q = match q with Tforall -> "forall" | Texists -> "exists" in
......@@ -414,7 +417,7 @@ and print_fmla info fmt f =
(print_var_list info) vl
(print_fmla info) f
(print_triggers info) tl;
List.iter forget_var vl
List.iter (forget_var info) vl
| Tbinop (Tand, f1, f2) ->
fprintf fmt "@[(and@ %a@ %a)@]" (print_fmla info) f1 (print_fmla info) f2
| Tbinop (Tor, f1, f2) ->
......@@ -435,9 +438,9 @@ and print_fmla info fmt f =
(print_fmla info) f1 (print_fmla info) f2 (print_fmla info) f3
| Tlet (t1, tb) ->
let v, f2 = t_open_bound tb in
fprintf fmt "@[(let ((%a %a))@ %a)@]" print_var v
fprintf fmt "@[(let ((%a %a))@ %a)@]" (print_var info) v
(print_term info) t1 (print_fmla info) f2;
forget_var v
forget_var info v
| Tcase(t, bl) ->
let ty = t_type t in
begin
......@@ -450,9 +453,9 @@ and print_fmla info fmt f =
| _ ->
let subject = create_vsymbol (id_fresh "subject") (t_type t) in
fprintf fmt "@[(let ((%a @[%a@]))@ %a)@]"
print_var subject (print_term info) t
(print_var info) subject (print_term info) t
(print_branches info subject print_fmla) bl;
forget_var subject
forget_var info subject
end
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f) in
......@@ -492,7 +495,7 @@ and print_branches info subject pr fmt bl = match bl with
| {pat_node = Pvar v} -> v | _ -> error ()) args in
if bl = [] then print_branch info subject pr fmt (cs,args,t)
else fprintf fmt "@[(ite (is-%a %a) %a %a)@]"
print_ident cs.ls_name print_var subject
(print_ident info) cs.ls_name (print_var info) subject
(print_branch info subject pr) (cs,args,t)
(print_branches info subject pr) bl
| _ -> error ()
......@@ -504,7 +507,8 @@ and print_branch info subject pr fmt (cs,vars,t) =
let i = ref 0 in
let pr_proj fmt v = incr i;
if Mvs.mem v tvs then fprintf fmt "(%a (%a_proj_%d %a))"
print_var v print_ident cs.ls_name !i print_var subject in
(print_var info) v (print_ident info) cs.ls_name
!i (print_var info) subject in
fprintf fmt "@[(let (%a) %a)@]" (print_list space pr_proj) vars (pr info) t
and print_expr info fmt =
......@@ -522,12 +526,12 @@ let print_type_decl info fmt ts =
if ts.ts_def <> None then () else
if Mid.mem ts.ts_name info.info_syn then () else
fprintf fmt "(declare-sort %a %i)@\n@\n"
print_ident ts.ts_name (List.length ts.ts_args)
(print_ident info) ts.ts_name (List.length ts.ts_args)
let print_param_decl info fmt ls =
if Mid.mem ls.ls_name info.info_syn then () else
fprintf fmt "@[<hov 2>(declare-fun %a (%a) %a)@]@\n@\n"
print_ident ls.ls_name
(print_ident info) ls.ls_name
(print_list space (print_type info)) ls.ls_args
(print_type_value info) ls.ls_value
......@@ -536,11 +540,11 @@ let print_logic_decl info fmt (ls,def) =
collect_model_ls info ls;
let vsl,expr = Decl.open_ls_defn def in
fprintf fmt "@[<hov 2>(define-fun %a (%a) %a %a)@]@\n@\n"
print_ident ls.ls_name
(print_ident info) ls.ls_name
(print_var_list info) vsl
(print_type_value info) ls.ls_value
(print_expr info) expr;
List.iter forget_var vsl
List.iter (forget_var info) vsl
end
let print_info_model cntexample fmt model_list info =
......@@ -571,7 +575,7 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
(print_fmla info) f
| Pgoal ->
fprintf fmt "@[(assert@\n";
fprintf fmt "@[;; %a@]@\n" print_ident pr.pr_name;
fprintf fmt "@[;; %a@]@\n" (print_ident info) pr.pr_name;
(match pr.pr_name.id_loc with
| None -> ()
| Some loc -> fprintf fmt " @[;; %a@]@\n"
......@@ -595,15 +599,15 @@ let print_prop_decl vc_loc cntexample args info fmt k pr f = match k with
let print_constructor_decl info fmt (ls,args) =
match args with
| [] -> fprintf fmt "(%a)" print_ident ls.ls_name
| [] -> fprintf fmt "(%a)" (print_ident info) ls.ls_name
| _ ->
fprintf fmt "@[(%a@ " print_ident ls.ls_name;
fprintf fmt "@[(%a@ " (print_ident info) ls.ls_name;
let _ =
List.fold_left2
(fun i ty pr ->
begin match pr with
| Some pr -> fprintf fmt "(%a" print_ident pr.ls_name
| None -> fprintf fmt "(%a_proj_%d" print_ident ls.ls_name i
| Some pr -> fprintf fmt "(%a" (print_ident info) pr.ls_name
| None -> fprintf fmt "(%a_proj_%d" (print_ident info) ls.ls_name i
end;
fprintf fmt " %a)" (print_type info) ty;
succ i) 1 ls.ls_args args
......@@ -612,7 +616,7 @@ let print_constructor_decl info fmt (ls,args) =
let print_data_decl info fmt (ts,cl) =
fprintf fmt "@[(%a@ %a)@]"
print_ident ts.ts_name
(print_ident info) ts.ts_name
(print_list space (print_constructor_decl info)) cl
let print_decl vc_loc cntexample args info fmt d = match d.d_node with
......@@ -633,42 +637,34 @@ let print_decl vc_loc cntexample args info fmt d = match d.d_node with
if Mid.mem pr.pr_name info.info_syn then () else
print_prop_decl vc_loc cntexample args info fmt k pr f
let print_decls vc_loc cntexample args =
let print_decl (sm, cm, model) fmt d =
try
let vc_term_info = { vc_inside = false; vc_loc = None; vc_func_name = None } in
let info = {
info_syn = sm;
info_converters = cm;
info_model = model;
info_in_goal = false;
info_vc_term = vc_term_info} in
print_decl vc_loc cntexample args info fmt d; (sm, cm, info.info_model), []
with Unsupported s -> raise (UnsupportedDecl (d,s)) in
let print_decl = Printer.sprint_decl print_decl in
let print_decl task acc = print_decl task.Task.task_decl acc in
Discriminate.on_syntax_map (fun sm ->
Printer.on_converter_map (fun cm ->
Trans.fold print_decl ((sm, cm, S.empty),[])))
let set_produce_models fmt cntexample =
if cntexample then
fprintf fmt "(set-option :produce-models true)@\n"
let print_task args ?old:_ fmt task =
(* In trans-based p-printing [forget_all] is a no-no *)
(* forget_all ident_printer; *)
let cntexample = Prepare_for_counterexmp.get_counterexmp task in
let vc_loc = Intro_vc_vars_counterexmp.get_location_of_vc task in
let vc_info = {vc_inside = false; vc_loc = None; vc_func_name = None} in
let info = {
info_syn = Discriminate.get_syntax_map task;
info_converters = Printer.get_converter_map task;
info_model = S.empty;
info_in_goal = false;
info_vc_term = vc_info;
info_printer = ident_printer () } in
print_prelude fmt args.prelude;
set_produce_models fmt cntexample;
print_th_prelude task fmt args.th_prelude;
let rec print = function
| x :: r -> print r; Pp.string fmt x
| [] -> () in
print (snd (Trans.apply (print_decls vc_loc cntexample args) task));
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
with Unsupported s -> raise (UnsupportedDecl (d,s)) end
| _ -> () end
| None -> () in
print_decls task;
pp_print_flush fmt ()
let () = register_printer "smtv2" print_task
......
src/transform/discriminate.ml
View file @ 4035a124
......@@ -367,21 +367,30 @@ let () =
discriminate_if_poly
~desc:"Same@ as@ discriminate@ but@ only@ if@ polymorphism@ appear."
let li_add_ls acc = function
| [MAls ls; MAls nls] -> Mls.add nls ls acc
| _ -> assert false
let get_lsinst task =
Task.on_meta meta_lsinst li_add_ls Mls.empty task
let on_lsinst fn =
let add_ls acc = function
| [MAls ls; MAls nls] -> Mls.add nls ls acc
| _ -> assert false in
Trans.on_meta meta_lsinst (fun dls ->
fn (List.fold_left add_ls Mls.empty dls))
fn (List.fold_left li_add_ls Mls.empty dls))
let sm_add_ls sm0 sm = function
| [MAls ls; MAls nls] ->
begin match Mid.find_opt ls.ls_name sm0 with
| Some s -> Mid.add nls.ls_name s sm
| None -> sm
end
| _ -> assert false
let get_syntax_map task =
let sm0 = Printer.get_syntax_map task in
Task.on_meta meta_lsinst (sm_add_ls sm0) sm0 task
let on_syntax_map fn =
let add_ls sm0 sm = function
| [MAls ls; MAls nls] ->
begin match Mid.find_opt ls.ls_name sm0 with
| Some s -> Mid.add nls.ls_name s sm
| None -> sm
end
| _ -> assert false in
Printer.on_syntax_map (fun sm0 ->
Trans.on_meta meta_lsinst (fun dls ->
fn (List.fold_left (fun sm dl -> add_ls sm0 sm dl) sm0 dls)))
fn (List.fold_left (sm_add_ls sm0) sm0 dls)))
src/transform/discriminate.mli
View file @ 4035a124
......@@ -23,5 +23,8 @@ val ft_select_inst : (Env.env,Ty.Sty.t) Trans.flag_trans
val ft_select_lskept : (Env.env,Term.Sls.t) Trans.flag_trans
val ft_select_lsinst : (Env.env,Lsmap.t) Trans.flag_trans
val get_lsinst : Task.task -> Term.lsymbol Term.Mls.t
val get_syntax_map : Task.task -> Printer.syntax_map
val on_lsinst : (Term.lsymbol Term.Mls.t -> 'a Trans.trans) -> 'a Trans.trans
val on_syntax_map : (Printer.syntax_map -> 'a Trans.trans) -> 'a Trans.trans
theories/seq.why
View file @ 4035a124
......@@ -409,8 +409,6 @@ end
(* TODO / TO DISCUSS
- reverse
- what about s[i..j] when i..j is not a valid range?
left undefined? empty sequence?
......
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