Commit 6d11889d authored by Andrei Paskevich's avatar Andrei Paskevich

in "eliminate_algebraic", use "let" instead of quantifiers, when possible

parent 4caec4bf
......@@ -5,7 +5,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "compile_match"
transformation "eliminate_algebraic"
transformation "eliminate_if"
transformation "eliminate_if_term"
transformation "eliminate_if_fmla"
transformation "eliminate_let"
theory BuiltIn
......
......@@ -238,6 +238,7 @@ val f_open_exists : fmla -> vsymbol list * fmla
val e_map : (term -> term) -> (fmla -> fmla) -> expr -> expr
val e_fold : ('a -> term -> 'a) -> ('a -> fmla -> 'a) -> 'a -> expr -> 'a
val e_apply : (term -> 'a) -> (fmla -> 'a) -> expr -> 'a
val e_equal : expr -> expr -> bool
val tr_map : (term -> term) ->
(fmla -> fmla) -> trigger list -> trigger list
......@@ -245,6 +246,8 @@ val tr_map : (term -> term) ->
val tr_fold : ('a -> term -> 'a) ->
('a -> fmla -> 'a) -> 'a -> trigger list -> 'a
val tr_equal : trigger list -> trigger list -> bool
(* map/fold over symbols *)
val t_s_map : (tysymbol -> tysymbol) -> (lsymbol -> lsymbol) -> term -> term
......
......@@ -64,14 +64,15 @@ let rec rewriteT kn state t = match t.t_node with
let tl = List.map find (find_constructors kn ts) in
t_app (Mts.find ts state.mt_map) (t1::tl) t.t_ty
| Tcase _ -> Register.unsupportedExpression (Term t) uncompiled
| _ -> t_map (rewriteT kn state) (rewriteF kn state true) t
| _ -> t_map (rewriteT kn state) (rewriteF kn state Svs.empty true) t
and rewriteF kn state sign f = match f.f_node with
and rewriteF kn state av sign f = match f.f_node with
| Fcase ([t1],bl) ->
let t1 = rewriteT kn state t1 in
let av' = Svs.diff av (t_freevars Svs.empty t1) in
let mk_br (w,m) br =
let (pl,e) = f_open_branch br in
let e = rewriteF kn state sign e in
let e = rewriteF kn state av' sign e in
match pl with
| [{ pat_node = Papp (cs,pl) }] ->
let get_var p = match p.pat_node with
......@@ -92,10 +93,15 @@ and rewriteF kn state sign f = match f.f_node with
in
let hd = t_app cs (List.map t_var vl) t1.t_ty in
let tr = [] (* FIXME? [[Term hd]] *) in
let hd = f_equ t1 hd in
if sign
then f_forall_simp vl tr (f_implies_simp hd e)
else f_exists_simp vl tr (f_and_simp hd e)
match t1.t_node with
| Tvar v when Svs.mem v av ->
let hd = f_let v hd e in if sign
then f_forall_simp vl tr hd
else f_exists_simp vl tr hd
| _ ->
let hd = f_equ t1 hd in if sign
then f_forall_simp vl tr (f_implies_simp hd e)
else f_exists_simp vl tr (f_and_simp hd e)
in
let ts = match t1.t_ty.ty_node with
| Tyapp (ts,_) -> ts
......@@ -104,7 +110,20 @@ and rewriteF kn state sign f = match f.f_node with
let op = if sign then f_and_simp else f_or_simp in
map_join_left find op (find_constructors kn ts)
| Fcase _ -> Register.unsupportedExpression (Fmla f) uncompiled
| _ -> f_map_sign (rewriteT kn state) (rewriteF kn state) sign f
| Fquant (q, bf) when (q = Fforall && sign) || (q = Fexists && not sign) ->
let vl, tr, f1 = f_open_quant bf in
let tr' = tr_map (rewriteT kn state)
(rewriteF kn state Svs.empty sign) tr in
let av = List.fold_left (fun s v -> Svs.add v s) av vl in
let f1' = rewriteF kn state av sign f1 in
if f1' == f1 && tr_equal tr' tr then f else f_quant q vl tr' f1'
| Fbinop (o, _, _) when (o = Fand && sign) || (o = For && not sign) ->
f_map_sign (rewriteT kn state) (rewriteF kn state av) sign f
| Flet (t1, _) ->
let av = Svs.diff av (t_freevars Svs.empty t1) in
f_map_sign (rewriteT kn state) (rewriteF kn state av) sign f
| _ ->
f_map_sign (rewriteT kn state) (rewriteF kn state Svs.empty) sign f
let add_type (state, task) ts csl =
(* declare constructors as abstract functions *)
......@@ -182,7 +201,7 @@ let comp t (state,task) = match t.task_decl with
List.fold_left add (state,task) dl
| Decl d ->
let fnT = rewriteT t.task_known state in
let fnF = rewriteF t.task_known state true in
let fnF = rewriteF t.task_known state Svs.empty true in
state, add_decl task (decl_map fnT fnF d)
| td ->
state, add_tdecl task td
......
......@@ -65,6 +65,8 @@ end
theory TestIte
use import int.Int
use list.Length
use list.Mem
logic abs(x:int) : int = if x >= 0 then x else -x
goal G : forall x:int. abs(x) >= 0
goal G2 : forall x:int. if x>=0 then x >= 0 else -x>=0
......
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