From b19195ad9c1736153763f1f91ea39d9077d9641e Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Tue, 1 Feb 2022 17:06:13 +0100
Subject: [PATCH] [Wp] generic sequent simplifier: applies simplify+assume
succesively on eacterms of a the conjective hypothesis
---
src/plugins/wp/Conditions.ml | 31 +++++++++++++++++++++++++------
1 file changed, 25 insertions(+), 6 deletions(-)
diff --git a/src/plugins/wp/Conditions.ml b/src/plugins/wp/Conditions.ml
index fcf91379566..ffa7a82d5f5 100644
--- a/src/plugins/wp/Conditions.ml
+++ b/src/plugins/wp/Conditions.ml
@@ -880,28 +880,47 @@ 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 apply_hyp modified solvers h =
- let simple p =
+ let weaken_and_then_assume p =
let p' = simplify_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
+ | And ps ->
+ let unmodified,qs = List.fold_left (fun (unmodified,qs) p ->
+ let p' = weaken_and_then_assume p in
+ (unmodified && (Lang.F.eqp p p')), (p'::qs))
+ (true,[]) ps
+ in if unmodified then p else p_conj qs
+ | _ -> 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 (simple p))
- | Type p -> update_cond h (Type (simple p))
- | Have p -> update_cond h (Have (simple p))
- | When p -> update_cond h (When (simple p))
- | Core p -> update_cond h (Core (simple p))
+ | 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))
| Branch(p,_,_) -> List.iter (fun s -> s#target p) solvers; h
| Either _ -> h
--
GitLab