Commit 9a615c12 authored by François Bobot's avatar François Bobot

encoding_arrays use builtin arrays in smtv1 extended

parent cfeddc81
......@@ -130,6 +130,7 @@ LIB_TRANSFORM = simplify_recursive_definition simplify_formula \
libencoding encoding_decorate encoding_bridge \
encoding_explicit encoding_sort \
encoding_instantiate simplify_array filter_trigger \
encoding_arrays \
introduction abstraction close_epsilon lift_epsilon
LIB_PRINTER = print_real alt_ergo why3 smt coq tptp simplify gappa
......
......@@ -20,6 +20,8 @@ transformation "eliminate_algebraic"
transformation "simplify_formula"
transformation "simplify_trivial_quantification"
transformation "encoding_array"
transformation "encoding_smt"
transformation "encoding_sort"
......@@ -129,6 +131,11 @@ theory int.EuclideanDivision
remove prop Div_1
end
theory transform.array.Array
syntax logic get "(select %1 %2)"
syntax logic get "(store %1 %2)"
end
(*
Local Variables:
mode: why
......
......@@ -25,10 +25,17 @@ open Ident
open Ty
open Term
open Decl
open Theory
open Task
open Printer
let ident_printer =
(** Options of this printer *)
let use_trigger = Theory.register_meta_excl "Smt : trigger" []
let use_builtin_array = Theory.register_meta_excl "Smt : builtin array" []
(** *)
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";
......@@ -52,6 +59,8 @@ let print_var fmt {vs_name = id} =
type info = {
info_syn : string Mid.t;
info_rem : Sid.t;
use_trigger : bool;
barrays : (ty*ty) Mts.t;
}
let rec print_type info fmt ty = match ty.ty_node with
......@@ -155,7 +164,13 @@ let print_logic_binder info fmt v =
let print_type_decl info fmt = function
| ts, Tabstract when Sid.mem ts.ts_name info.info_rem -> false
| ts, Tabstract when ts.ts_args = [] ->
fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true
begin try
let key,elt = Mts.find ts info.barrays in
fprintf fmt ":define_sorts ((%a (array %a %a)))"
print_ident ts.ts_name
(print_type info) key (print_type info) elt; true
with Not_found ->
fprintf fmt ":extrasorts (%a)" print_ident ts.ts_name; true end
| _, Tabstract -> unsupported
"smtv1 : type with argument are not supported"
| _, Talgebraic _ -> unsupported
......@@ -205,6 +220,21 @@ let print_decl info fmt d = match d.d_node with
let print_decl info fmt = catch_unsupportedDecl (print_decl info fmt)
let barrays task =
let sds = find_meta task Encoding_arrays.meta_mono_array in
let fold tdecl barrays =
match tdecl.td_node with
| Meta (_,[MAts tst;MAts tsk;MAts tse]) ->
let extract_ty ts =
if ts.ts_args <> [] then
unsupported "smtv1 : type with argument are not supported";
match ts.ts_def with
| Some ty -> ty
| None -> ty_app ts [] in
Mts.add tst (extract_ty tsk,extract_ty tse) barrays
| _ -> barrays in
Stdecl.fold fold sds.tds_set Mts.empty
let print_task pr thpr fmt task =
fprintf fmt "(benchmark why3@\n"
(*print_ident (Task.task_goal task).pr_name*);
......@@ -213,7 +243,10 @@ let print_task pr thpr fmt task =
print_th_prelude task fmt thpr;
let info = {
info_syn = get_syntax_map task;
info_rem = get_remove_set task }
info_rem = get_remove_set task;
use_trigger = false;
barrays = barrays task;
}
in
let decls = Task.task_decls task in
ignore (print_list_opt (add_flush newline2) (print_decl info) fmt decls);
......
This diff is collapsed.
val meta_mono_array : Theory.meta
......@@ -352,24 +352,6 @@ let conv_to_tty env ts tyl proj_ty =
else let args = ty_args_from_tty tyl in
*)
(* Free type in terms and formulae *)
let rec t_fold_ty fty s t =
let s = t_fold (t_fold_ty fty) (f_fold_ty fty) s t in
let s = fty s t.t_ty in
match t.t_node with
| Teps fb ->
let vs,_ = f_open_bound fb in
fty s vs.vs_ty
| _ -> s
and f_fold_ty fty s f =
let s = f_fold (t_fold_ty fty) (f_fold_ty fty) s f in
match f.f_node with
| Fquant (_,fq) ->
let (vsl,_,_) = f_open_quant fq in
List.fold_left (fun s vs -> fty s vs.vs_ty) s vsl
| _ -> s
let ty_quant =
let rec add_vs s ty = match ty.ty_node with
| Tyvar vs -> Stv.add vs s
......@@ -533,7 +515,7 @@ let create_meta_ty ty =
let ts = create_tysymbol name [] (Some ty) in
(create_meta meta_kept [MAts ts])
(* Weak table is useless since ty is in ts *)
let create_meta_ty = Wty.memoize 17 create_meta_ty
let create_meta_tyl sty d =
......@@ -573,3 +555,54 @@ let () =
"goal", mono_in_goal;
"mono", mono_in_mono;
"all", mono_in_def]
(* Select array *)
let meta_kept_array = register_meta "encoding : kept_array" [MTtysymbol]
(* select the type array which appear as argument of set and get.
set and get must be in sls *)
let find_mono_array ~only_mono sls sty f =
let add sty ls tyl =
match tyl with
| ty::_ when Sls.mem ls sls && is_ty_mono ~only_mono ty ->
Sty.add ty sty
| _ -> sty in
f_fold_sig add sty f
let create_meta_ty ty =
let name = id_fresh "meta_ty" in
let ts = create_tysymbol name [] (Some ty) in
(create_meta meta_kept_array [MAts ts])
let create_meta_ty = Wty.memoize 17 create_meta_ty
let create_meta_tyl sty d =
Sty.fold (flip $ cons create_meta_ty) sty [create_decl d]
let mono_in_goal sls pr f =
let sty = (try find_mono_array ~only_mono:true sls Sty.empty f
with Exit -> assert false) (*monomorphise goal should have been used*) in
create_meta_tyl sty (create_prop_decl Pgoal pr f)
let mono_in_goal sls = Trans.tgoal (mono_in_goal sls)
let trans_array th_array =
let set = ns_find_ls th_array.th_export ["set"] in
let get = ns_find_ls th_array.th_export ["get"] in
let sls = Sls.add set (Sls.add get Sls.empty) in
mono_in_goal sls
let trans_array env =
let th_array = Env.find_theory env ["array"] "Array" in
Trans.on_used_theory th_array (fun used ->
if not used then Trans.identity else trans_array th_array)
let () = Trans.register_env_transform "use_builtin_array" trans_array
(*
Local Variables:
compile-command: "unset LANG; make -C ../.. byte"
End:
*)
......@@ -33,8 +33,11 @@ end
theory Test_simplify_array
use import array.Array
goal G : forall x y:int. forall m: t int int.
goal G1 : forall x y:int. forall m: t int int.
get (set m y x) y = x
goal G2 : forall x y:int. forall m: t int int.
get (set m y x) y = y
end
theory Test_conjunction
......
......@@ -20,4 +20,9 @@ theory Array
axiom Const : forall b:elt, a:key. get (create_const b) a = b
meta "encoding_arrays : mono_arrays" type t, type key, type elt
meta "encoding : kept" type key
meta "encoding : kept" type t
meta "encoding : kept" type elt
end
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