Class type Wp.Conditions.simplifier

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.