Commit e2a3605f authored by Martin Clochard's avatar Martin Clochard

simplify_trivial_quantification: restore equality removal

parent 0bd8a2b7
......@@ -93,6 +93,21 @@ let rec fmla_find_subst boundvars var sign f =
| Tapp _ | Tfalse | Ttrue -> ()
| Tvar _ | Tconst _ | Teps _ -> raise (FmlaExpected f)
(* Simplify out equalities that could be selected. *)
let rec equ_simp f = t_label_copy f (match f.t_node with
| Tbinop (op, f1, f2) ->
begin match op, equ_simp f1, equ_simp f2 with
| Tor, { t_node = Tfalse }, f
| Tor, f, { t_node = Tfalse }
| Tand, { t_node = Ttrue }, f
| Tand, f, { t_node = Ttrue }
| Timplies, { t_node = Ttrue }, f -> f
| op, f1, f2 -> t_binary op f1 f2
end
| Tapp (p,[f1;f2]) when ls_equal p ps_equ ->
t_equ_simp (equ_simp f1) (equ_simp f2)
| _ -> t_map equ_simp f)
let rec fmla_quant sign f = function
| [] -> [], f
| vs::l ->
......@@ -102,7 +117,7 @@ let rec fmla_quant sign f = function
vs::vsl, f
with Subst_found t ->
let f = t_subst_single vs t f in
vsl, f
vsl, equ_simp f
let rec fmla_remove_quant f =
match f.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