Commit 41618dd5 authored by MARCHE Claude's avatar MARCHE Claude
Browse files

Gappa needs simplification of quantifiers

parent d7574f33
...@@ -21,7 +21,7 @@ transformation "eliminate_algebraic_smt" ...@@ -21,7 +21,7 @@ transformation "eliminate_algebraic_smt"
transformation "eliminate_if" transformation "eliminate_if"
transformation "eliminate_let" transformation "eliminate_let"
transformation "simplify_formula" transformation "simplify_formula"
(*transformation "simplify_trivial_quantification"*) transformation "simplify_trivial_quantification"
transformation "introduce_premises" transformation "introduce_premises"
theory BuiltIn theory BuiltIn
......
...@@ -221,6 +221,9 @@ let rec print_fmla info fmt f = ...@@ -221,6 +221,9 @@ let rec print_fmla info fmt f =
| Fapp ({ ls_name = id }, []) -> | Fapp ({ ls_name = id }, []) ->
print_ident fmt id print_ident fmt id
| Fapp (ls, [t1;t2]) when ls_equal ls ps_equ -> | Fapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
(* TODO: distinguish between type of t1 and t2
the following is OK only for real of integer
*)
begin try begin try
let c1 = constant_value t1 in let c1 = constant_value t1 in
fprintf fmt "%a in [%s,%s]" term t2 c1 c1 fprintf fmt "%a in [%s,%s]" term t2 c1 c1
...@@ -329,6 +332,9 @@ let print_decls ?old info fmt dl = ...@@ -329,6 +332,9 @@ let print_decls ?old info fmt dl =
let filter_hyp info eqs hyps pr f = let filter_hyp info eqs hyps pr f =
match f.f_node with match f.f_node with
| Fapp(ls,[t1;t2]) when ls == ps_equ -> | Fapp(ls,[t1;t2]) when ls == ps_equ ->
(* TODO: if type of t! and T2 is single or double, then
replace by (value t1) = (value t2) and (exact t1 = exact t2)
*)
begin match t1.t_node with begin match t1.t_node with
| Tapp(_,[]) -> | Tapp(_,[]) ->
((pr,t1,t2)::eqs,hyps) ((pr,t1,t2)::eqs,hyps)
......
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