class type simplifier =object
..end
method name : string
method copy : simplifier
method assume : F.pred -> unit
Assumes the hypothesis
method target : F.pred -> unit
Give the predicate that will be simplified later
method fixpoint : unit
Called after assuming hypothesis and knowing the goal
method infer : F.pred list
Add new hypotheses implied by the original hypothesis.
method equivalent_exp : F.term -> F.term
Currently simplify an expression. It must returns a equivalent formula from the assumed hypotheses.
method weaker_hyp : F.pred -> F.pred
Currently simplify an hypothesis before assuming it. It must return a weaker formula from the assumed hypotheses.
method equivalent_branch : F.pred -> F.pred
Currently simplify a branch condition. It must return an equivalent formula from the assumed hypotheses.
method stronger_goal : F.pred -> F.pred
Simplify the goal. It must return a stronger formula from the assumed hypotheses.