Class type Conditions.simplifier

class type simplifier = object .. end

method name : string
method copy : simplifier
method simplify_hyp : Lang.F.pred -> Lang.F.pred
Currently simplify an hypothesis before assuming it. In any case must return a weaker formula.
method assume : Lang.F.pred -> unit
Assumes the hypothesis
method target : Lang.F.pred -> unit
Give the predicate that will be simplified later
method fixpoint : unit
Called after assuming hypothesis and knowing the goal
method simplify_branch : Lang.F.pred -> Lang.F.pred
Currently simplify a branch condition. In any case must return an equivalent formula.
method infer : Lang.F.pred list
Add new hypotheses implyed by the original hypothesis.
method simplify_goal : Lang.F.pred -> Lang.F.pred
Simplify the goal. In any case must return a stronger formula.