Commit e7aa3e10 authored by Andrei Paskevich's avatar Andrei Paskevich

preserve non-recursive definitions in z3 and cvc3

parent 68e17edd
......@@ -14,7 +14,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
......
......@@ -16,7 +16,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_builtin"
transformation "eliminate_definition"
transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic_smt"
......
......@@ -85,6 +85,28 @@ let open_ls_defn_cb ld =
let ls_defn_axiom (_,f) = f
let ls_defn_of_axiom f =
let _,_,f = match f.t_node with
| Tquant (Tforall,b) -> t_open_quant b
| _ -> [],[],f in
let hd,e = match f.t_node with
| Tapp (ls, [hd; t]) when ls_equal ls ps_equ -> hd,t
| Tbinop (Tiff, hd, f) -> hd,f
| _ -> raise Exit in
let ls,tl = match hd.t_node with
| Tapp (ls,tl) -> ls,tl
| _ -> raise Exit in
let vs_of_t t = match t.t_node with
| Tvar v -> v
| _ -> raise Exit in
let vl = List.map vs_of_t tl in
make_ls_defn ls vl e
let ls_defn_of_axiom f =
try Some (ls_defn_of_axiom f) with
| Exit | UnboundVar _ | UnboundTypeVar _
| DuplicateVar _ | TypeMismatch _ -> None
(** Termination checking for mutually recursive logic declarations *)
type descent =
......
......@@ -48,6 +48,11 @@ val open_ls_defn_cb : ls_defn -> vsymbol list * term *
val ls_defn_axiom : ls_defn -> term
val ls_defn_of_axiom : term -> logic_decl option
(** tries to reconstruct a definition from a defining axiom. Do not apply
this to recursive definitions: it may successfully build a logic_decl,
which will fail later because of non-assured termination *)
val check_termination : logic_decl list -> (int list) Mls.t
(** [check_termination ldl] returns a mapping of every logical
symbol defined in [ldl] to a list of its argument positions
......
......@@ -150,18 +150,13 @@ let map env d = match d.d_node with
let conv_f tvar (defns,axioms) =
let f = t_ty_subst tvar Mvs.empty f in
let f = t_app_map (find_logic env) f in
let vl,_,e = match f.t_node with
| Tquant (Tforall,b) -> t_open_quant b
| _ -> [],[],f in
let ls,e = match e.t_node with
| Tapp (_, [{t_node = Tapp (ls,_)}; e])
| Tbinop (_, {t_node = Tapp (ls,_)}, e) -> ls,e
| _ -> assert false in
if List.for_all2 (fun ty v -> ty_equal ty v.vs_ty) ls.ls_args vl
&& option_eq ty_equal ls.ls_value e.t_ty
then create_logic_decl [make_ls_defn ls vl e] :: defns, axioms
else let id = id_fresh (ls.ls_name.id_string ^ "_inst") in
defns, create_prop_decl Paxiom (create_prsymbol id) f :: axioms
match ls_defn_of_axiom f with
| Some ld ->
create_logic_decl [ld] :: defns, axioms
| None ->
let nm = ls.ls_name.id_string ^ "_inst" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
defns, create_prop_decl Paxiom pr f :: axioms
in
let defns,axioms = Ssubst.fold conv_f substs ([],[]) in
ts_of_ls env ls (List.rev_append defns axioms)
......
......@@ -159,116 +159,83 @@ let conv_res_app tenv p tl tty =
let rec rewrite_term tenv vsvar t =
(* Format.eprintf "@[<hov 2>Term : %a =>@\n@?" Pretty.print_term t; *)
let fnT = rewrite_term tenv in
let fnF = rewrite_fmla tenv in
let fn = rewrite_term tenv in
let t = match t.t_node with
| Tvar vs -> Mvs.find vs vsvar
| Tconst _ -> t
| Tapp(p,tl) ->
let tl = List.map (fnT vsvar) tl in
| Tapp(p, [t1;t2]) when ls_equal p ps_equ ->
t_equ (fn vsvar t1) (fn vsvar t2)
| Tapp(p, tl) ->
let tl = List.map (fn vsvar) tl in
let p = Hls.find tenv.trans_lsymbol p in
let tl = List.map2 (conv_arg tenv) tl p.ls_args in
if t.t_ty = None then ps_app p tl else
conv_res_app tenv p tl (t_type t)
| Tlet (t1, b) ->
let u,t2,close = t_open_bound_cb b in
let t1 = fnT vsvar t1 in
let t1 = fn vsvar t1 in
let u' = conv_vs tenv u in
let vsvar = Mvs.add u (t_var u') vsvar in
let t2 = fnT vsvar t2 in
let t2 = fn vsvar t2 in
t_let t1 (close u' t2)
| Teps b ->
let u,f,close = t_open_bound_cb b in
let u' = conv_vs tenv u in
let vsvar = Mvs.add u (t_var u') vsvar in
let f = fnF vsvar f in
let f = fn vsvar f in
t_eps (close u' f)
| Tif (f,t1,t2) ->
t_if (fnF vsvar f) (fnT vsvar t1) (fnT vsvar t2)
t_if (fn vsvar f) (fn vsvar t1) (fn vsvar t2)
| Tcase _ ->
Printer.unsupportedTerm t "no match expressions at this point"
| Tquant _ | Tbinop _ | Tnot _ | Ttrue | Tfalse -> raise (TermExpected t)
in
(* Format.eprintf "@[<hov 2>Term : => %a : %a@\n@?" Pretty.print_term t *)
(* Pretty.print_ty t.t_ty; *)
t
and rewrite_fmla tenv vsvar f =
(* Format.eprintf "@[<hov 2>Fmla : %a =>@\n@?" Pretty.print_fmla f; *)
let fnT = rewrite_term tenv in
let fnF = rewrite_fmla tenv in
let f = match f.t_node with
| Tapp(p, [t1;t2]) when ls_equal p ps_equ ->
t_equ (fnT vsvar t1) (fnT vsvar t2)
| Tapp(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
ps_app p tl
| Tquant (q, b) ->
let vl, tl, f1, close = t_open_quant_cb b in
let conv_vs (vsvar,l) vs =
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
let f1 = fn vsvar f1 in
(* Ici un trigger qui ne match pas assez de variables
peut être généré *)
let tl = TermTF.tr_map (fnT vsvar) (fnF vsvar) tl in
let tl = tr_map (fn vsvar) tl in
let vl = List.rev vl in
t_quant q (close vl tl f1)
| Tlet (t1, b) ->
let u,f2,close = t_open_bound_cb b in
let t1 = fnT vsvar t1 in
let u' = conv_vs tenv u in
let vsvar = Mvs.add u (t_var u') vsvar in
let f2 = fnF vsvar f2 in
t_let t1 (close u' f2)
| Tbinop (op,f1,f2) -> t_binary op (fnF vsvar f1) (fnF vsvar f2)
| Tnot f1 -> t_not (fnF vsvar f1)
| Ttrue | Tfalse -> f
| Tif (f1,f2,f3) ->
t_if (fnF vsvar f1) (fnF vsvar f2) (fnF vsvar f3)
| Tcase _ ->
Printer.unsupportedTerm f "no match expressions at this point"
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
| Tbinop (op,f1,f2) -> t_binary op (fn vsvar f1) (fn vsvar f2)
| Tnot f1 -> t_not (fn vsvar f1)
| Ttrue | Tfalse -> t
in
(* Format.eprintf "@[<hov 2>Fmla : => %a@\n@?" Pretty.print_fmla f; *)
f
t
let decl (tenv:tenv) d =
(* let fnT = rewrite_term tenv in *)
let fnF = rewrite_fmla tenv in
match d.d_node with
(* | Dtype [ts,Tabstract] when is_kept tenv ts -> *)
(* tenv.clone_builtin ts *)
| Dtype [_,Tabstract] -> [create_decl d]
| 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
d "encoding_decorate : I can't encode definition. \
Perhaps you could use eliminate_definition"
| ls, None ->
try
let ls = Hls.find tenv.trans_lsymbol ls in
ls,None
let ls_of_tenv tenv ls =
try Hls.find tenv.trans_lsymbol ls
with Not_found ->
let ls_conv = conv_ls tenv ls in
Hls.add tenv.trans_lsymbol ls ls_conv;
ls_conv,None in
[create_decl (create_logic_decl (List.map fn l))]
| Dind _ -> Printer.unsupportedDecl
d "encoding_decorate : I can't work on inductive"
ls_conv
let decl (tenv:tenv) d = match d.d_node with
(* | Dtype [ts,Tabstract] when is_kept tenv ts -> *)
(* tenv.clone_builtin ts *)
| Dtype [_,Tabstract] -> [d]
| Dtype _ -> Printer.unsupportedDecl d
"Algebraic and recursively-defined types are \
not supported, run eliminate_algebraic"
| Dlogic [ls, None] ->
[create_logic_decl [ls_of_tenv tenv ls, None]]
| Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
let ls = ls_of_tenv tenv ls in
let f = rewrite_term tenv Mvs.empty (ls_defn_axiom ld) in
Libencoding.defn_or_axiom ls f
| Dlogic _ -> Printer.unsupportedDecl d
"Recursively-defined symbols are not supported, run eliminate_recursion"
| Dind _ -> Printer.unsupportedDecl d
"Inductive predicates are not supported, run eliminate_inductive"
(* let fn (pr,f) = pr, fnF f in *)
(* let fn (ps,l) = ps, List.map fn l in *)
(* [create_ind_decl (List.map fn l)] *)
| Dprop (k,pr,f) ->
let f = fnF Mvs.empty f in
[create_decl (create_prop_decl k pr f)]
[create_prop_decl k pr (rewrite_term tenv Mvs.empty f)]
(*
let decl tenv d =
......@@ -283,7 +250,7 @@ let t env =
Trans.compose Libencoding.close_kept
(Trans.on_tagged_ty meta_kept (fun s ->
let init_task,tenv = load_prelude s env in
Trans.tdecl (decl tenv) init_task))
Trans.decl (decl tenv) init_task))
let () = Hashtbl.replace Encoding.ft_enco_kept "bridge" t
......@@ -39,30 +39,25 @@ let rec deco_arg kept tvar t =
and deco_term kept tvar t = match t.t_node with
| Tapp (fs,tl) -> t_app fs (List.map (deco_arg kept tvar) tl) t.t_ty
| _ -> TermTF.t_map (deco_term kept tvar) (deco_fmla kept tvar) t
and deco_fmla kept tvar f = match f.t_node with
| Tapp (ps,tl) -> ps_app ps (List.map (deco_arg kept tvar) tl)
| Tquant (q,b) ->
let vl,tl,f,close = t_open_quant_cb b in
let tl = TermTF.tr_map (deco_arg kept tvar) (deco_fmla kept tvar) tl in
t_quant q (close vl tl (deco_fmla kept tvar f))
| _ -> TermTF.t_map (deco_term kept tvar) (deco_fmla kept tvar) f
let tl = TermTF.tr_map (deco_arg kept tvar) (deco_term kept tvar) tl in
t_quant q (close vl tl (deco_term kept tvar f))
| _ -> t_map (deco_term kept tvar) t
let deco_decl kept d = match d.d_node with
| Dtype tdl ->
d :: lsdecl_of_tydecl tdl
| Dlogic ldl ->
let check = function
| _, Some _ -> Printer.unsupportedDecl d "eliminate definitions"
| _ -> ()
in
List.iter check ldl;
[d]
| Dind _ -> Printer.unsupportedDecl d "eliminate inductives"
| Dlogic [_, None] -> [d]
| Dlogic [ls, Some ld] when not (Sid.mem ls.ls_name d.d_syms) ->
let f = t_type_close (deco_term kept) (ls_defn_axiom ld) in
defn_or_axiom ls f
| Dlogic _ -> Printer.unsupportedDecl d
"Recursively-defined symbols are not supported, run eliminate_recursion"
| Dind _ -> Printer.unsupportedDecl d
"Inductive predicates are not supported, run eliminate_inductive"
| Dprop (k,pr,f) ->
let f = t_type_close (deco_fmla kept) f in
[create_prop_decl k pr f]
[create_prop_decl k pr (t_type_close (deco_term kept) f)]
let d_poly_deco = create_logic_decl [ls_poly_deco, None]
......
......@@ -248,3 +248,11 @@ let close_kept =
let fold ty acc =
Theory.create_meta Encoding.meta_kept [Theory.MAty ty] :: acc in
Trans.add_tdecls (Sty.fold fold kept' []))
let defn_or_axiom ls f =
match Decl.ls_defn_of_axiom f with
| Some ld -> [create_logic_decl [ld]]
| None ->
let nm = ls.ls_name.id_string ^ "_def" in
let pr = create_prsymbol (id_derive nm ls.ls_name) in
[create_logic_decl [ls,None]; create_prop_decl Paxiom pr f]
......@@ -57,5 +57,9 @@ val lsdecl_of_tydecl_select : ty_decl list -> decl list
(* monomorphise wrt the base type, the set of kept types, and a symbol map *)
val d_monomorph : ty -> Sty.t -> (lsymbol -> lsymbol) -> decl -> decl list
(* Close by subtype the set of type tagged by the meta "kept" *)
(* close by subtype the set of type tagged by the meta "kept" *)
val close_kept : Task.task Trans.trans
(* reconstruct a definition of an lsymbol or make a defining axiom *)
val defn_or_axiom : lsymbol -> term -> decl list
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