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