Class type Conditions.simplifier

class type simplifier = object .. end

method name : string
method copy : simplifier
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 infer : Lang.F.pred list

Add new hypotheses implied by the original hypothesis.

method simplify_exp : Lang.F.term -> Lang.F.term

Currently simplify an expression.

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 simplify_branch : Lang.F.pred -> Lang.F.pred

Currently simplify a branch condition. In any case must return an equivalent formula.

method simplify_goal : Lang.F.pred -> Lang.F.pred

Simplify the goal. In any case must return a stronger formula.