Skip to content

why3
why3
Commit 65f7d3c7 authored by Andrei Paskevich's avatar Andrei Paskevich
Browse files
Options

whitespace

parent 795e0d48
Hide whitespace changes
Inline Side-by-side
Showing with 160 additions and 160 deletions
src/transform/abstraction.ml
View file @ 65f7d3c7
......@@ -5,8 +5,8 @@ open Term
open Decl
open Task
let term_table = Hterm.create 257
let fmla_table = Hfmla.create 257
let term_table = Hterm.create 257
let fmla_table = Hfmla.create 257
let extra_decls = ref []
let rec abstract_term keep t : term =
......@@ -21,12 +21,12 @@ let rec abstract_term keep t : term =
extra_decls := ls :: !extra_decls;
Hterm.add term_table t tabs;
tabs
end
end
and abstract_fmla keep f =
match f.f_node with
| Ftrue | Ffalse -> f
| Fnot _ | Fbinop _ ->
| Fnot _ | Fbinop _ ->
f_map (abstract_term keep) (abstract_fmla keep) f
| Fapp(ls,_) when keep ls ->
f_map (abstract_term keep) (abstract_fmla keep) f
......@@ -37,20 +37,20 @@ and abstract_fmla keep f =
extra_decls := ls :: !extra_decls;
Hfmla.add fmla_table f fabs;
fabs
end
let abstract_decl keep (d : decl) : decl list =
end
let abstract_decl keep (d : decl) : decl list =
let d = decl_map (abstract_term keep) (abstract_fmla keep) d in
let l =
let l =
List.fold_left
(fun acc ls -> create_logic_decl [ls,None] :: acc)
[d]
!extra_decls
in
extra_decls := []; l
extra_decls := []; l
let abstraction (keep : lsymbol -> bool) (t: task) : task =
let abstraction (keep : lsymbol -> bool) (t: task) : task =
Hfmla.clear fmla_table;
Hterm.clear term_table;
Trans.apply (Trans.decl (abstract_decl keep) None) t
src/transform/abstraction.mli
View file @ 65f7d3c7
......@@ -13,5 +13,5 @@ val abstraction : (Term.lsymbol -> bool) -> Task.task -> Task.task
[abstraction (fun f -> List.mem f ["+";"-"]) "goal x*x+y*y = 1"]
returns ["logic abs1 = x*x; logic abs2 = y*y; goal abs1+abs2 = 1"]
*)
src/transform/encoding_bridge.ml
View file @ 65f7d3c7
......@@ -39,15 +39,15 @@ type tenv = {kept : Sty.t;
specials : lconv Hty.t;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : tysymbol Hts.t}
(* trans_lsymbol ne depend pour l'instant pas du but,
(* trans_lsymbol ne depend pour l'instant pas du but,
comme specials_type ne depend pas*)
(* Translate a type to a type without kept *)
let rec ty_of_ty tenv ty =
match ty.ty_node with
| Tyapp (ts,[]) ->
let tts = try Hts.find tenv.trans_tsymbol ts
let tts = try Hts.find tenv.trans_tsymbol ts
with Not_found -> ts in
ty_app tts []
| Tyapp (ts,l) -> ty_app ts (List.map (ty_of_ty tenv) l)
......@@ -68,30 +68,30 @@ let load_prelude kept env =
trans_lsymbol = Hls.create 17;
trans_tsymbol = trans_tsymbol} in
let clone_builtin ts (task,sty) =
let ty = match ts.ts_def with
| Some ty -> ty
| None -> try ty_app ts [] with BadTypeArity(_,_,_) ->
let ty = match ts.ts_def with
| Some ty -> ty
| None -> try ty_app ts [] with BadTypeArity(_,_,_) ->
failwith "kept without definition must be constant" in
let add_ts task ts = add_ty_decl task [ts,Tabstract] in
let task = ty_s_fold add_ts task ty in
let is_constant =
match ty.ty_node with
let is_constant =
match ty.ty_node with
| Tyapp (_,[]) -> true
| _ -> false in
let ts_head =
match ty.ty_node with
match ty.ty_node with
| Tyapp (ts,_) -> ts
| _ -> assert false in
let task = add_ts task ts in
let tb = create_tysymbol (id_clone ts_head.ts_name) []
(if is_constant then None else Some (ty_of_ty tenv_tmp ty)) in
let task = add_ts task tb in
let tytb = ty_app tb [] in
let tytb = ty_app tb [] in
let tb2t = create_fsymbol (id_clone logic_tb2t.ls_name) [tytb] ty in
let t2tb = create_fsymbol (id_clone logic_t2tb.ls_name) [ty] tytb in
let task = add_logic_decl task [tb2t,None] in
let task = add_logic_decl task [t2tb,None] in
let th_inst = create_inst
let th_inst = create_inst
~ts:[type_t,ts;type_tb,tb]
~ls:[logic_t2tb,t2tb;logic_tb2t,tb2t] ~lemma:[] ~goal:[] in
let task = Task.clone_export task builtin th_inst in
......@@ -118,21 +118,21 @@ let conv_vs tenv vs =
create_vsymbol (id_dup vs.vs_name) ty
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
let conv_ls tenv ls =
if ls_equal ls ps_equ
then ls
else
let tyl = List.map (conv_ty tenv) ls.ls_args in
let ty_res = Util.option_map (conv_ty tenv) ls.ls_value in
if Util.option_eq ty_equal ty_res ls.ls_value
&& List.for_all2 ty_equal tyl ls.ls_args
if Util.option_eq ty_equal ty_res ls.ls_value
&& List.for_all2 ty_equal tyl ls.ls_args
then ls
else
let preid = id_clone ls.ls_name in
create_lsymbol preid tyl ty_res
(* Convert the argument of a function use the bridge if needed*)
let conv_arg tenv t aty =
let conv_arg tenv t aty =
let tty = t.t_ty in
if ty_equal tty aty then t else
try
......@@ -146,7 +146,7 @@ let conv_arg tenv t aty =
t
(* Convert with a bridge an application if needed *)
let conv_res_app tenv p tl tty =
let conv_res_app tenv p tl tty =
try
(* tty is a special value *)
let tylconv = Hty.find tenv.specials tty in
......@@ -201,7 +201,7 @@ and rewrite_fmla tenv vsvar f =
let f = match f.f_node with
| Fapp(p, [t1;t2]) when ls_equal p ps_equ ->
f_equ (fnT vsvar t1) (fnT vsvar t2)
| Fapp(p, tl) ->
| Fapp(p, tl) ->
let tl = List.map (fnT vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv) tl p.ls_args in
......@@ -212,8 +212,8 @@ and rewrite_fmla tenv vsvar f =
let vs' = conv_vs tenv vs in
Mvs.add vs (t_var vs') vsvar,vs'::l in
let (vsvar,vl) = List.fold_left conv_vs (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut être généré *)
let tl = tr_map (fnT vsvar) (fnF vsvar) tl in
let vl = List.rev vl in
......@@ -243,13 +243,13 @@ let decl (tenv:tenv) d =
(* | Dtype [ts,Tabstract] when is_kept tenv ts -> *)
(* tenv.clone_builtin ts *)
| Dtype [_,Tabstract] -> [create_decl d]
| Dtype _ -> Printer.unsupportedDecl
| Dtype _ -> Printer.unsupportedDecl
d "encoding_decorate : I can work only on abstract \
type which are not in recursive bloc."
| Dlogic l ->
let fn = function
| _ls, Some _ ->
Printer.unsupportedDecl
| _ls, Some _ ->
Printer.unsupportedDecl
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls, None ->
......
src/transform/encoding_decorate_mono.ml
View file @ 65f7d3c7
......@@ -39,7 +39,7 @@ type tenv = {rem_ls : Sls.t;
sort : lsymbol;
real_to_int : lsymbol;
trans_lsymbol : lsymbol Hls.t;
trans_tsymbol : lsymbol Hts.t}
trans_tsymbol : lsymbol Hts.t}
let load_prelude rem_ls env =
let prelude = Env.find_theory env why_filename "Prelude_mono" in
......@@ -61,18 +61,18 @@ let load_prelude rem_ls env =
(* Translate a type to a term *)
let rec term_of_ty tenv tvar ty =
match ty.ty_node with
| Tyapp (ts,l) ->
| Tyapp (ts,l) ->
let tts = Hts.find tenv.trans_tsymbol ts in
t_app tts (List.map (term_of_ty tenv tvar) l) tenv.unsorted
| Tyvar tv ->
| Tyvar tv ->
t_var (try Htv.find tvar tv
with Not_found ->
(let var = create_vsymbol
with Not_found ->
(let var = create_vsymbol
(id_fresh ("tv"^tv.tv_name.id_string))
tenv.unsorted in
Htv.add tvar tv var;
var))
let sort_app tenv tvar t ty =
let tty = term_of_ty tenv tvar ty in
t_app tenv.sort [tty;t] tenv.unsorted
......@@ -84,7 +84,7 @@ let conv_ty_neg tenv _ty = tenv.unsorted
let conv_ty_pos tenv _ty = tenv.unsorted
(* Convert a logic symbols to the encoded one *)
let conv_ls tenv ls =
let conv_ls tenv ls =
if ls_equal ls ps_equ
then ls
else
......@@ -104,18 +104,18 @@ let conv_ts tenv ts =
let conv_arg _tenv _tvar t _ty = t
(* Convert to undeco or to a specials an application *)
let conv_res_app tenv tvar p tl ty =
let conv_res_app tenv tvar p tl ty =
let tty = Util.of_option p.ls_value in
assert (ty_equal tty tenv.unsorted);
let t = t_app p tl tenv.unsorted in
sort_app tenv tvar t ty
let conv_vs tenv tvar (vsvar,acc) vs =
let tres,vsres =
let ty_res = conv_ty_pos tenv vs.vs_ty in
let tty = term_of_ty tenv tvar vs.vs_ty in
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
let t = t_var vsres in
t_app tenv.sort [tty;t] tenv.unsorted, vsres in
(Mvs.add vs tres vsvar,vsres::acc)
......@@ -124,10 +124,10 @@ let conv_vs_let tenv vsvar vs =
let ty_res = conv_ty_neg tenv vs.vs_ty in
if ty_equal ty_res vs.vs_ty then
t_var vs,vs
else
else
let vsres = (create_vsymbol (id_clone vs.vs_name) ty_res) in
let t = t_var vsres in
t, vsres in
let t = t_var vsres in
t, vsres in
(Mvs.add vs tres vsvar,vsres)
......@@ -137,7 +137,7 @@ let rec rewrite_term tenv tvar vsvar t =
let fnF = rewrite_fmla tenv tvar vsvar in
match t.t_node with
| Tconst ConstInt _ -> sort_app tenv tvar t t.t_ty
| Tconst ConstReal _ ->
| Tconst ConstReal _ ->
let t2 = t_app tenv.real_to_int [t] tenv.unsorted in
sort_app tenv tvar t2 t.t_ty
| Tvar x -> Mvs.find x vsvar
......@@ -146,7 +146,7 @@ let rec rewrite_term tenv tvar vsvar t =
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
conv_res_app tenv tvar p tl t.t_ty
| Tif (f, t1, t2) ->
| Tif (f, t1, t2) ->
t_if (fnF f) (fnT vsvar t1) (fnT vsvar t2)
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
......@@ -167,7 +167,7 @@ and rewrite_fmla tenv tvar vsvar f =
let ty = tenv.unsorted in
let tl = List.map2 (conv_arg tenv tvar) tl [ty;ty] in
f_app p tl
| Fapp(p, tl) ->
| Fapp(p, tl) ->
let tl = List.map fnT tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv tvar) tl p.ls_args in
......@@ -175,13 +175,13 @@ and rewrite_fmla tenv tvar vsvar f =
| Fquant (q, b) ->
let vl, tl, f1, close = f_open_quant_cb b in
let (vsvar,vl) = List.fold_left (conv_vs tenv tvar) (vsvar,[]) vl in
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
let f1 = fnF vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut tre gnr *)
let tl = tr_map (rewrite_term tenv tvar vsvar) (fnF vsvar) tl in
let vl = List.rev vl in
f_quant q (close vl tl f1)
| Flet (t1, b) ->
| Flet (t1, b) ->
let u, f2, close = f_open_bound_cb b in
let (vsvar,u) = conv_vs_let tenv vsvar u in
let t1 = fnT t1 in let f2 = fnF vsvar f2 in
......@@ -197,26 +197,26 @@ let decl (tenv:tenv) d =
let fnF = rewrite_fmla tenv in
match d.d_node with
| Dtype [ts,Tabstract] when ts_equal ts ts_int -> []
| Dtype [ts,Tabstract] ->
let tty =
try
Hts.find tenv.trans_tsymbol ts
with Not_found ->
| Dtype [ts,Tabstract] ->
let tty =
try
Hts.find tenv.trans_tsymbol ts
with Not_found ->
let tty = conv_ts tenv ts in
Hts.add tenv.trans_tsymbol ts tty;
tty in
[create_decl (create_logic_decl [(tty,None)])]
| Dtype _ -> Printer.unsupportedDecl
| Dtype _ -> Printer.unsupportedDecl
d "encoding_decorate : I can work only on abstract\
type which are not in recursive bloc."
| Dlogic l ->
let fn acc = function
| _ls, Some _ ->
Printer.unsupportedDecl
| _ls, Some _ ->
Printer.unsupportedDecl
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls1, None ->
let ls2 =
let ls2 =
try
Hls.find tenv.trans_lsymbol ls1
with Not_found -> conv_ls tenv ls1 in
......@@ -227,9 +227,9 @@ Perhaps you could use eliminate_definition"
let vars = List.map make ls1.ls_args in
let terms1 = List.map t_var vars in
let tvar = Htv.create 0 in
let terms2 = List.map
let terms2 = List.map
(fun t -> sort_app tenv tvar t ty_int) terms1 in
let fmla =
let fmla =
match ls1.ls_value with
| None ->
let f1 = f_app ls1 terms1 in
......
src/transform/encoding_instantiate.ml
View file @ 65f7d3c7
......@@ -467,8 +467,8 @@ let collect_green_part tds =
| None -> ty_app ts []
| Some ty -> ty) ts tys in
Sts.fold extract sts Mty.empty
(* Some general env creation function *)
let create_env task tenv tds =
......@@ -524,7 +524,7 @@ let () =
let find_mono ~only_mono sty f =
let rec ty_add sty ty = ty_fold ty_add (Sty.add ty sty) ty in
let add sty ty = if is_ty_mono ~only_mono ty then
let add sty ty = if is_ty_mono ~only_mono ty then
ty_add sty ty else sty in
f_fold_ty add sty f
......
src/transform/encoding_simple2.ml
View file @ 65f7d3c7
......@@ -43,8 +43,8 @@ let init_tenv = {
let conv_ty tenv undefined ty =
match ty.ty_node with
| Tyapp (_,[]) -> ty
| Tyapp (ts,_) ->
let ts =
| Tyapp (ts,_) ->
let ts =
try
Hty.find tenv.specials ty
with Not_found ->
......@@ -52,7 +52,7 @@ let conv_ty tenv undefined ty =
Hty.add tenv.specials ty ts;
ts in
Hts.replace undefined ts ();
ty_app ts []
ty_app ts []
| _ -> Printer.unsupportedType ty "type variable must be encoded"
(* Convert a variable *)
......@@ -154,7 +154,7 @@ let decl tenv d =
let ud = Hts.create 3 in
decl_ud ud [decl_map (fnT ud Mvs.empty) (fnF ud Mvs.empty) d]
let t =
let t =
let tenv = init_tenv in
Trans.decl (decl tenv) None
......
src/transform/filter_trigger.ml
View file @ 65f7d3c7
......@@ -21,7 +21,7 @@ open Term
let make_rt_rf keep =
let rec rt t = t_map rt rf t
and rf f =
and rf f =
let f = f_map rt rf f in
match f.f_node with
| Fquant (Fforall,fq) ->
......@@ -38,8 +38,8 @@ let make_rt_rf keep =
let keep_no_trigger _ = false
let remove_triggers =
let remove_triggers =
let rt,rf = make_rt_rf keep_no_trigger in
Trans.rewrite rt rf None
......@@ -50,12 +50,12 @@ let keep_no_predicate = function
| Term _ -> true
| _ -> false
let filter_trigger_no_predicate =
let filter_trigger_no_predicate =
let rt,rf = make_rt_rf keep_no_predicate in
Trans.rewrite rt rf None
let () = Trans.register_transform "filter_trigger_no_predicate"
let () = Trans.register_transform "filter_trigger_no_predicate"
filter_trigger_no_predicate
......@@ -77,14 +77,14 @@ let keep_no_builtin rem_ls = function
| Fmla {f_node = Fapp (ps,_)} -> not (Sls.mem ps rem_ls)
| _ -> false
let filter_trigger_builtin =
Trans.on_meta Printer.meta_syntax_logic (fun tds ->
let rem_ls =
let rem_ls =
Task.find_tagged_ls Printer.meta_syntax_logic tds Sls.empty
in
let rt,rf = make_rt_rf (keep_no_builtin rem_ls) in
Trans.rewrite rt rf None)
let () = Trans.register_transform "filter_trigger_builtin"
let () = Trans.register_transform "filter_trigger_builtin"
filter_trigger_builtin
src/transform/inlining.ml
View file @ 65f7d3c7
......@@ -37,11 +37,11 @@ let print_env fmt env =
(print_map Mls.iter Pretty.print_term Pretty.print_lsymbol) env.fs
(print_map Mls.iter Pretty.print_fmla Pretty.print_lsymbol) env.ps
*)
let rec replacet env t =
let rec replacet env t =
let t = substt env t in
match t.t_node with
| Tapp (fs,tl) ->
begin try
begin try
let (vs,t) = Mls.find fs env.fs in
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
......@@ -52,11 +52,11 @@ let rec replacet env t =
with Not_found -> t end
| _ -> t
and replacep env f =
and replacep env f =
let f = substp env f in
match f.f_node with
| Fapp (ps,tl) ->
begin try
begin try
let (vs,f) = Mls.find ps env.ps in
let add (mt,mv) x y =
(Ty.ty_match mt x.vs_ty y.t_ty, Mvs.add x y mv)
......@@ -69,7 +69,7 @@ and replacep env f =
and substt env d = t_map (replacet env) (replacep env) d
and substp env d = f_map (replacet env) (replacep env) d
let fold isnotinlinedt isnotinlinedf d (env, task) =
let fold isnotinlinedt isnotinlinedf d (env, task) =
(* Format.printf "I see : %a@\n%a@\n" Pretty.print_decl d print_env env;*)
match d.d_node with
| Dlogic [ls,ld] -> begin
......@@ -81,34 +81,34 @@ let fold isnotinlinedt isnotinlinedf d (env, task) =
| Term t ->
let t = replacet env t in
if isnotinlinedt t || t_s_any ffalse (ls_equal ls) t
then env, add_decl task
then env, add_decl task
(create_logic_decl [make_fs_defn ls vs t])
else {env with fs = Mls.add ls (vs,t) env.fs},task
| Fmla f ->
| Fmla f ->
let f = replacep env f in
if isnotinlinedf f || f_s_any ffalse (ls_equal ls) f
then env, add_decl task
then env, add_decl task
(create_logic_decl [make_ps_defn ls vs f])
else {env with ps = Mls.add ls (vs,f) env.ps},task
end
| Dind dl ->
env, add_decl task (create_ind_decl
(List.map (fun (ps,fmlal) -> ps, List.map
env, add_decl task (create_ind_decl
(List.map (fun (ps,fmlal) -> ps, List.map
(fun (pr,f) -> pr, replacep env f) fmlal) dl))
| Dlogic dl ->
| Dlogic dl ->
env,
add_decl task (create_logic_decl
(List.map (fun (ls,ld) -> match ld with
add_decl task (create_logic_decl
(List.map (fun (ls,ld) -> match ld with
| None -> ls, None
| Some ld ->
let vs,e = open_ls_defn ld in
let e = e_map (replacet env) (replacep env) e in
make_ls_defn ls vs e) dl))
| Dtype _ -> env,add_decl task d
| Dprop (k,pr,f) ->
| Dprop (k,pr,f) ->
env,add_decl task (create_prop_decl k pr (replacep env f))
let fold isnotinlinedt isnotinlinedf task0 (env, task) =
let fold isnotinlinedt isnotinlinedf task0 (env, task) =
match task0.task_decl with
| { Theory.td_node = Theory.Decl d } ->
fold isnotinlinedt isnotinlinedf d (env, task)
......@@ -119,19 +119,19 @@ let t ~isnotinlinedt ~isnotinlinedf =
let all = t ~isnotinlinedt:(fun _ -> false) ~isnotinlinedf:(fun _ -> false)
let trivial = t
let trivial = t
~isnotinlinedt:(fun m -> match m.t_node with
| Tconst _ | Tvar _ -> false
| Tapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| Tapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
| _ -> true )
~isnotinlinedf:(fun m -> match m.f_node with
~isnotinlinedf:(fun m -> match m.f_node with
| Ftrue | Ffalse -> false
| Fapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| Fapp (_,tl) when List.for_all
(fun m -> match m.t_node with
| Tvar _ -> true
| _ -> false) tl -> false
| _ -> true)
......
src/transform/inlining.mli
View file @ 65f7d3c7
......@@ -22,7 +22,7 @@
val t :
isnotinlinedt:(Term.term -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
isnotinlinedf:(Term.fmla -> bool) ->
Task.task Trans.trans
......@@ -44,5 +44,5 @@ val empty_env : env
(*val add_decl : env -> Theory.decl -> env *)
val replacet : env -> Term.term -> Term.term
val replacet : env -> Term.term -> Term.term
val replacep : env -> Term.fmla -> Term.fmla
src/transform/introduction.ml
View file @ 65f7d3c7
......@@ -30,7 +30,7 @@ let rec intros pr f = match f.f_node with
let d = create_prop_decl Paxiom id f1 in
d :: intros pr f2
*)
| Fquant (Fforall,fq) ->
| Fquant (Fforall,fq) ->
let vsl,_trl,f = f_open_quant fq in
let intro_var subst vs =
let ls = create_lsymbol (id_clone vs.vs_name) [] (Some vs.vs_ty) in
......@@ -38,7 +38,7 @@ let rec intros pr f = match f.f_node with
create_logic_decl [ls,None]
in
let subst, dl = Util.map_fold_left intro_var Mvs.empty vsl in
let f = f_subst subst f in
let f = f_subst subst f in
dl @ intros pr f
| _ -> [create_prop_decl Pgoal pr f]
......
src/transform/simplify_array.ml
View file @ 65f7d3c7
......@@ -27,12 +27,12 @@ let store = ["store"]
let select = ["select"]
let make_rt_rf env =
let array =
let array =
try
find_theory env prelude array
with TheoryNotFound (_,s) ->
Format.eprintf "The theory %s is unknown" s;
exit 1 in
with TheoryNotFound (_,s) ->
Format.eprintf "The theory %s is unknown" s;
exit 1 in
let store = (ns_find_ls array.th_export store).ls_name in
let select = (ns_find_ls array.th_export select).ls_name in
let rec rt t =
......@@ -45,7 +45,7 @@ let make_rt_rf env =
| _ -> t
and rf f = f_map rt rf f in
rt,rf
let t env = let rt,rf = make_rt_rf env in Trans.rewrite rt rf None
let () = Trans.register_env_transform "simplify_array" t
src/transform/simplify_formula.ml
View file @ 65f7d3c7
......@@ -24,7 +24,7 @@ let rec fmla_simpl f = f_map_simp (fun t -> t) fmla_simpl f
let decl_l d =
match d.d_node with
| Dprop (k,pr,f) ->
| Dprop (k,pr,f) ->
let f = fmla_simpl f in
begin match f.f_node, k with
| Ftrue, Paxiom -> [[]]
......@@ -38,10 +38,10 @@ let simplify_formula = Trans.rewrite (fun t -> t) fmla_simpl None
let simplify_formula_and_task = Trans.decl_l decl_l None
let () = Trans.register_transform
let () = Trans.register_transform
"simplify_formula" simplify_formula
let () = Trans.register_transform_l
let () = Trans.register_transform_l
"simplify_formula_and_task" simplify_formula_and_task
(** remove_trivial_quantification
......@@ -50,7 +50,7 @@ let () = Trans.register_transform_l
(** transform \exists x. x == y /\ F into F[y/x] *)
(** transform \forall x. x <> y \/ F into F[y/x] *)
(** test if the freevariable of a term
(** test if the freevariable of a term
are included in a given set *)
let t_boundvars_in fvars t =
try
......@@ -64,20 +64,20 @@ let rec fmla_find_subst boundvars var sign f =
let fnF = fmla_find_subst boundvars var in
match f.f_node with
| Fapp (ls,[{t_node=Tvar vs} as tv;t])
| Fapp (ls,[t;{t_node=Tvar vs} as tv])
when sign && ls_equal ls ps_equ && vs_equal vs var
| Fapp (ls,[t;{t_node=Tvar vs} as tv])
when sign && ls_equal ls ps_equ && vs_equal vs var
&& not (t_equal t tv) && not (t_boundvars_in boundvars t) ->
raise (Subst_found t)
| Fbinop (For, f1, f2) when not sign -> (fnF sign f1); (fnF sign f2)
| Fbinop (For, f1, f2) when not sign -> (fnF sign f1); (fnF sign f2)
| Fbinop (Fand, f1, f2) when sign -> (fnF sign f1); (fnF sign f2)
| Fbinop (Fimplies, f1, f2) when not sign ->
| Fbinop (Fimplies, f1, f2) when not sign ->
(fnF (not sign) f1); (fnF sign f2)
| Fnot f1 -> fnF (not sign) f1
| Fquant (_,fb) ->
let vsl,trl,f' = f_open_quant fb in
if trl = []
then
let boundvars =
if trl = []
then
let boundvars =
List.fold_left (fun s v -> Svs.add v s) boundvars vsl in
fmla_find_subst boundvars var sign f'
| Flet (_,fb) ->
......@@ -87,14 +87,14 @@ let rec fmla_find_subst boundvars var sign f =
| Fcase (_,fbs) ->
let iter_fb fb =
let patl,f = f_open_branch fb in
let boundvars = patl.pat_vars in
let boundvars = patl.pat_vars in
fmla_find_subst boundvars var sign f in
List.iter iter_fb fbs
| Fbinop (_, _, _) | Fif ( _, _, _) | Fapp _ | Ffalse | Ftrue-> ()
let rec fmla_quant sign f = function
| [] -> [], f
| vs::l ->
| vs::l ->
let vsl, f = fmla_quant sign f