diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index 65ff69a9b88586d14ad5200049359a688a392bb6..18d0d1a9ace4418a952940ed5bfe33e1006b41b8 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -1232,13 +1232,13 @@ let is_cint_simplifier =
Lang.F.QED.f_map ~pool ~forall:false ~exists:false walk_both_pol t in
Lang.F.p_bool (walk ~term_pol:(Polarity.from_bool is_goal) (Lang.F.e_prop p))
- method simplify_exp (e : term) = e
+ method equivalent_exp (e : term) = e
- method simplify_hyp p = self#simplify ~is_goal:false p
+ method weaker_hyp p = self#simplify ~is_goal:false p
- method simplify_goal p = self#simplify ~is_goal:true p
+ method stronger_goal p = self#simplify ~is_goal:true p
- method simplify_branch p = p
+ method equivalent_branch p = p
method infer = []
end
@@ -1292,19 +1292,19 @@ let mask_simplifier =
end
| _ -> ()) (F.e_prop p)
- method simplify_exp e =
+ method equivalent_exp e =
if Tmap.is_empty magnitude then e else
Lang.e_subst (rewrite magnitude) e
- method simplify_hyp p =
+ method weaker_hyp p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
- method simplify_branch p =
+ method equivalent_branch p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
- method simplify_goal p =
+ method stronger_goal p =
if Tmap.is_empty magnitude then p else
Lang.p_subst (rewrite magnitude) p
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index ffa7a82d5f57cde14c430a9c3dc0eb8c967cf823..d7f79eb1d398ab4ce7431124e38f5d84b27d4d69 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -880,32 +880,25 @@ and letify_case sigma ~target ~export seq =
(* --- External Simplifier --- *)
(* -------------------------------------------------------------------------- *)
-(* Simplify an expression. *)
-let simplify_exp solvers e =
- List.fold_left (fun e s -> s#simplify_exp e) e solvers
-
-(* Simplify the goal.
- In any case must return a stronger formula. *)
-let simplify_goal solvers p =
- List.fold_left (fun p s -> s#simplify_goal p) p solvers
-
-(** Simplify an hypothesis before assuming it.
- In any case must return a weaker formula. *)
-let simplify_hyp solvers p =
- List.fold_left (fun p s -> s#simplify_hyp p) p solvers
-
-(* Simplify a branch condition.
- In any case must return an equivalent formula. *)
-let simplify_branch solvers p =
- List.fold_left (fun p s -> s#simplify_branch p) p solvers
+let equivalent_exp solvers e =
+ List.fold_left (fun e s -> s#equivalent_exp e) e solvers
+let stronger_goal solvers p =
+ List.fold_left (fun p s -> s#stronger_goal p) p solvers
+let weaker_hyp solvers p =
+ List.fold_left (fun p s -> s#weaker_hyp p) p solvers
+let equivalent_branch solvers p =
+ List.fold_left (fun p s -> s#equivalent_branch p) p solvers
+
+let apply_goal solvers p =
+ stronger_goal solvers p
let apply_hyp modified solvers h =
let weaken_and_then_assume p =
- let p' = simplify_hyp solvers p in
+ let p' = weaker_hyp solvers p in
if not (Lang.F.eqp p p') then modified := true;
List.iter (fun s -> s#assume p') solvers; p'
in
- let weaken_hyp p = match F.p_expr p with
+ let weaken p = match F.p_expr p with
| And ps ->
let unmodified,qs = List.fold_left (fun (unmodified,qs) p ->
let p' = weaken_and_then_assume p in
@@ -915,19 +908,19 @@ let apply_hyp modified solvers h =
| _ -> weaken_and_then_assume p
in
match h.condition with
- | State s -> update_cond h (State (Mstate.apply (simplify_exp solvers) s))
- | Init p -> update_cond h (Init (weaken_hyp p))
- | Type p -> update_cond h (Type (weaken_hyp p))
- | Have p -> update_cond h (Have (weaken_hyp p))
- | When p -> update_cond h (When (weaken_hyp p))
- | Core p -> update_cond h (Core (weaken_hyp p))
+ | State s -> update_cond h (State (Mstate.apply (equivalent_exp solvers) s))
+ | Init p -> update_cond h (Init (weaken p))
+ | Type p -> update_cond h (Type (weaken p))
+ | Have p -> update_cond h (Have (weaken p))
+ | When p -> update_cond h (When (weaken p))
+ | Core p -> update_cond h (Core (weaken p))
| Branch(p,_,_) -> List.iter (fun s -> s#target p) solvers; h
| Either _ -> h
let decide_branch modified solvers h =
match h.condition with
| Branch(p,a,b) ->
- let q = simplify_branch solvers p in
+ let q = equivalent_branch solvers p in
if q != p then
( modified := true ; update_cond h (Branch(q,a,b)) )
else h
@@ -958,7 +951,7 @@ let apply_simplifiers (solvers : simplifier list) (hs,g) =
List.iter (fun s -> s#fixpoint) solvers ;
let hs = List.map (decide_branch modified solvers) hs in
let hs = List.fold_right (add_infer modified) solvers hs in
- let p = simplify_goal solvers g in
+ let p = apply_goal solvers g in
if p != g || !modified then
Simplified (hs,p)
else
diff --git a/src/plugins/wp/Lang.ml b/src/plugins/wp/Lang.ml
index a2f02f254515b8036e078a1966612b9bb8cc827b..4a3f934474aa58370c7287b07ce8816cca658362 100644
--- a/src/plugins/wp/Lang.ml
+++ b/src/plugins/wp/Lang.ml
@@ -1067,10 +1067,10 @@ class type simplifier =
method fixpoint : unit
method infer : F.pred list
- method simplify_exp : F.term -> F.term
- method simplify_hyp : F.pred -> F.pred
- method simplify_branch : F.pred -> F.pred
- method simplify_goal : F.pred -> F.pred
+ method equivalent_exp : F.term -> F.term
+ method weaker_hyp : F.pred -> F.pred
+ method equivalent_branch : F.pred -> F.pred
+ method stronger_goal : F.pred -> F.pred
end
let is_atomic_pred = function
diff --git a/src/plugins/wp/Lang.mli b/src/plugins/wp/Lang.mli
index 514110749b1f0336eb4f14377b20cd5e78ea32ec..ed9978d3a29740e35762419b90f09e44a4354bd9 100644
--- a/src/plugins/wp/Lang.mli
+++ b/src/plugins/wp/Lang.mli
@@ -576,16 +576,18 @@ class type simplifier =
method infer : F.pred list
(** Add new hypotheses implied by the original hypothesis. *)
- method simplify_exp : F.term -> F.term
- (** Currently simplify an expression. *)
- method simplify_hyp : F.pred -> F.pred
- (** Currently simplify an hypothesis before assuming it. In any
- case must return a weaker formula. *)
- method simplify_branch : F.pred -> F.pred
- (** Currently simplify a branch condition. In any case must return an
- equivalent formula. *)
- method simplify_goal : F.pred -> F.pred
- (** Simplify the goal. In any case must return a stronger formula. *)
+ 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. *)
end
(* -------------------------------------------------------------------------- *)