Skip to content

why3
why3
Commit 5d7a985a authored by Quentin Garchery's avatar Quentin Garchery
Browse files
Options

hybrid eliminate_if 

we continue to use the duplicating version of eliminate_if_term for
atomic formulas but we replace if-then-else with epsilon in Tlet and Tcase
parent b6699186
Expand all Hide whitespace changes
Inline Side-by-side
Showing with 354 additions and 333 deletions
drivers/alt_ergo_common.drv
View file @ 5d7a985a
......@@ -27,8 +27,8 @@ transformation "eliminate_recursion"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "split_premise_right"
......
drivers/beagle.drv
View file @ 5d7a985a
......@@ -30,11 +30,11 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
transformation "eliminate_let"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_smt"
......
drivers/coq-ssreflect.drv
View file @ 5d7a985a
......@@ -13,6 +13,7 @@ time "why3cpulimit time : %s s"
transformation "inline_trivial"
transformation "eliminate_non_struct_recursion"
transformation "eliminate_if"
transformation "eliminate_literal"
transformation "eliminate_non_lambda_set_epsilon"
transformation "eliminate_projections"
transformation "simplify_formula"
......
drivers/gappa.drv
View file @ 5d7a985a
......@@ -17,8 +17,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "simplify_unknown_lsymbols"
......
drivers/isabelle-common.gen
View file @ 5d7a985a
......@@ -7,8 +7,8 @@ fail "\\*\\*\\* \\(.*\\)$" "\\1"
time "why3cpulimit time : %s s"
transformation "eliminate_negative_constants"
transformation "eliminate_epsilon"
transformation "eliminate_if_fmla"
transformation "eliminate_epsilon"
transformation "eliminate_let_fmla"
transformation "simplify_formula"
......
drivers/mathematica.drv
View file @ 5d7a985a
......@@ -20,8 +20,8 @@ transformation "eliminate_builtin"
(*transformation "eliminate_algebraic"*)
(*transformation "eliminate_algebraic_math"*)
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(*transformation "eliminate_if"*)
transformation "eliminate_epsilon"
transformation "eliminate_let"
(*transformation "split_premise"*)
......
drivers/metitarski.drv
View file @ 5d7a985a
......@@ -31,8 +31,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "eliminate_negative_constants" (* due to integers, see below *)
......
drivers/polypaver.drv
View file @ 5d7a985a
......@@ -19,8 +19,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "simplify_formula"
......
drivers/princess.drv
View file @ 5d7a985a
......@@ -30,11 +30,11 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
(* currently, princess does not support $let and $ite *)
transformation "eliminate_let"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "discriminate"
transformation "encoding_smt"
......
drivers/simplify.drv
View file @ 5d7a985a
......@@ -16,8 +16,8 @@ transformation "eliminate_definition" (*_func*)
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "simplify_formula"
......
drivers/spass_types.drv
View file @ 5d7a985a
......@@ -22,8 +22,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "discriminate"
......
drivers/tptp.gen
View file @ 5d7a985a
......@@ -23,8 +23,8 @@ transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_negative_constants"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "simplify_formula"
......
drivers/why3_tptp.drv
View file @ 5d7a985a
......@@ -10,8 +10,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "discriminate"
......
drivers/zenon.drv
View file @ 5d7a985a
......@@ -18,8 +18,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
transformation "discriminate"
......
drivers/zenon_modulo.drv
View file @ 5d7a985a
......@@ -18,8 +18,8 @@ transformation "eliminate_definition"
transformation "eliminate_inductive"
transformation "eliminate_algebraic"
transformation "eliminate_literal"
transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_epsilon"
transformation "eliminate_let"
theory BuiltIn
......
examples/bts/231_destruct/why3session.xml
View file @ 5d7a985a
......@@ -66,11 +66,11 @@
</transf>
</goal>
</theory>
<theory name="Incompleteness">
<goal name="t1">
<transf name="destruct_rec" arg1="H">
<goal name="t1.0">
<proof prover="0" obsolete="true"><result status="valid" time="0.00"/></proof>
<theory name="Incompleteness" proved="true">
<goal name="t1" proved="true">
<transf name="destruct_rec" proved="true" arg1="H">
<goal name="t1.0" proved="true">
<proof prover="0"><result status="valid" time="0.00"/></proof>
</goal>
</transf>
</goal>
......
examples/prover/Prover/why3session.xml
View file @ 5d7a985a
This diff is collapsed.
src/transform/eliminate_epsilon.ml
View file @ 5d7a985a
......@@ -178,6 +178,13 @@ let rec lift_f el acc t0 =
(create_param_decl ls :: abst, ax :: axml), t
in
acc, t_attr_copy t0 t
| Teps _ ->
let vl,tr,t = t_open_lambda t0 in
let acc, t = lift_f el acc t in
let acc, tr = Lists.map_fold_left
(Lists.map_fold_left (lift_f el))
acc tr in
acc, t_attr_copy t0 (t_lambda vl tr t)
| _ ->
t_map_fold (lift_f el) acc t0
......
src/transform/eliminate_if.ml
View file @ 5d7a985a
......@@ -43,10 +43,24 @@ let rec elim_t contT t =
| _ ->
TermTF.t_map_cont elim_t elim_f contT t
and elim_t_eps t = match t.t_node with
| Tif (f,t1,t2) when t.t_ty <> None ->
let z = create_vsymbol (id_fresh "if_term") (t_type t) in
let tz = t_var z in
let f = elim_f (fun f -> f) f in
let f1 = t_equ tz (elim_t_eps t1) in
let f2 = t_equ tz (elim_t_eps t2) in
t_attr_copy t (t_eps_close z (t_if f f1 f2))
| _ ->
TermTF.t_map elim_t_eps (elim_f (fun f -> f)) t
and elim_f contF f = match f.t_node with
| Tapp _ | Tlet _ | Tcase _ ->
| Tapp _ ->
contF (TermTF.t_map_cont elim_t elim_f (fun f -> f) f)
| _ -> TermTF.t_map_cont elim_tr elim_f contF f
| Tlet _ | Tcase _ ->
contF (TermTF.t_map elim_t_eps (elim_f (fun f -> f)) f)
| _ ->
TermTF.t_map_cont elim_tr elim_f contF f
(* the only terms we still can meet are the terms in triggers *)
and elim_tr contT t = match t.t_node with
......
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