Metis/src/Active.sml

154             case Clause.simplify cl of
211 type simplify = {subsume : bool, reduce : bool, rewrite : bool};
215       prefactor : simplify,
216       postfactor : simplify};
252 val maxSimplify : simplify = {subsume = true, reduce = true, rewrite = true};
369 fun simplify simp units rewr subs =
377             if Clause.equalThms cl cl' then SOME cl else Clause.simplify cl'
381          case Clause.simplify cl of
395 val simplify = fn simp => fn units => fn rewr => fn subs => fn cl =>
397       fun traceCl s = Print.trace Clause.pp ("Active.simplify: " ^ s)
402       val cl' = simplify simp units rewr subs cl
404       val () = Print.trace ppClOpt "Active.simplify: cl'" cl'
411               (case simplify simp units rewr subs cl' of
425                     ("Active.simplify: clause should have been simplified "^e)
436       simplify simp units rewrite subsume
797         simplify prefactor units rewrite subsume
805         simplify postfactor units rewrite subsume