Commit 00d95af9 authored by Martin Clochard's avatar Martin Clochard

Aggressive simplification in transformation chains

parent e8a48006
......@@ -25,6 +25,8 @@ transformation "eliminate_epsilon"
transformation "eliminate_if"
transformation "eliminate_let"
transformation "simplify_formula"
transformation "discriminate"
transformation "encoding_tptp"
......
......@@ -9,10 +9,16 @@
(* *)
(********************************************************************)
open Ident
open Term
open Decl
let rec fmla_simpl f = TermTF.t_map_simp t_fmla_simpl fmla_simpl f
let labset = Slab.of_list [keep_on_simp_label;asym_label]
let rec fmla_simpl f =
let f = if Slab.disjoint f.t_label labset then f else
t_label ?loc:f.t_loc (Slab.diff f.t_label labset) f in
TermTF.t_map_simp t_fmla_simpl fmla_simpl f
and t_fmla_simpl t = TermTF.t_map t_fmla_simpl fmla_simpl t
......
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