Class type Lang.simplifier

class type simplifier = object .. end

method name : string

method copy : simplifier

method assume : F.pred -> unit

Assumes the hypothesis

method target : F.pred -> unit

Give the predicate that will be simplified later

method fixpoint : unit

Called after assuming hypothesis and knowing the goal

method infer : F.pred list

Add new hypotheses implied by the original hypothesis.

method equivalent_exp : F.term -> F.term

Currently simplify an expression. It must returns a equivalent formula from the assumed hypotheses.

method weaker_hyp : F.pred -> F.pred

Currently simplify an hypothesis before assuming it. It must return a weaker formula from the assumed hypotheses.

method equivalent_branch : F.pred -> F.pred

Currently simplify a branch condition. It must return an equivalent formula from the assumed hypotheses.

method stronger_goal : F.pred -> F.pred

Simplify the goal. It must return a stronger formula from the assumed hypotheses.