class type simplifier =object..end
method name : string
method copy : simplifier
method assume : F.pred -> unitAssumes the hypothesis
method target : F.pred -> unitGive the predicate that will be simplified later
method fixpoint : unitCalled after assuming hypothesis and knowing the goal
method infer : F.pred listAdd new hypotheses implied by the original hypothesis.
method simplify_exp : F.term -> F.termCurrently simplify an expression.
method simplify_hyp : F.pred -> F.predCurrently simplify an hypothesis before assuming it. In any case must return a weaker formula.
method simplify_branch : F.pred -> F.predCurrently simplify a branch condition. In any case must return an equivalent formula.
method simplify_goal : F.pred -> F.predSimplify the goal. In any case must return a stronger formula.