From fa07e4a8416e1845985d6eb8a48dfc1e185b5fbe Mon Sep 17 00:00:00 2001
From: Patrick Baudin <patrick.baudin@cea.fr>
Date: Thu, 9 May 2019 10:40:34 +0200
Subject: [PATCH] [WP] fixes Cint solver
---
src/plugins/wp/Changelog | 1 +
src/plugins/wp/Cint.ml | 7 ++++++-
2 files changed, 7 insertions(+), 1 deletion(-)
diff --git a/src/plugins/wp/Changelog b/src/plugins/wp/Changelog
index 1bbd1d8265a..611e7dd2923 100644
--- a/src/plugins/wp/Changelog
+++ b/src/plugins/wp/Changelog
@@ -20,6 +20,7 @@
# <Prover>: prover
###############################################################################
+ - Wp [2019/05/09] Fixes -wp-simplify-is-cint simplifier
- Wp [2019/04/26] Now requires -warn-invalid-bool
- Wp [2019/04/26] Removed option -wp-bool-range
- Wp [2019/04/24] Support for Why3 1.* and Coq 8.{7-9}
diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index db97213a0c4..874efe45760 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -815,6 +815,7 @@ let c_int_bounds_ival f =
let max_reduce_quantifiers = 1000
+(** We know that t is a predicate which is the opened body of a forall *)
let reduce_bound v dom t : term =
let module Exc = struct
exception True
@@ -831,8 +832,9 @@ let reduce_bound v dom t : term =
Ival.fold_int red dom (); raise Exc.True
with Exc.Unknown i -> i in
let max_bound = try
- Ival.fold_int(*_decrease*) red dom (); raise Exc.True
+ Ival.fold_int_decrease red dom (); raise Exc.True
with Exc.Unknown i -> i in
+ (** we try to reduce the bounds of the domains, when trivially false *)
let dom_red = Ival.inject_range (Some min_bound) (Some max_bound) in
if not (Ival.equal dom_red dom) && Ival.is_included dom_red dom
then t
@@ -929,6 +931,8 @@ let is_cint_simplifier = object (self)
domain <- Tmap.add tvar !var_domain domain;
let t = walk ~is_goal t in
domain <- Tmap.remove tvar domain;
+ (** Bonus: Add additionnal hypothesis in forall when we could deduce
+ better constraint on the variable *)
let t = if quant = Forall &&
is_goal &&
Ival.cardinal_is_less_than !var_domain max_reduce_quantifiers
@@ -936,6 +940,7 @@ let is_cint_simplifier = object (self)
else t in
e_bind quant var t
| Fun(g,[a]) ->
+ (** Here we simplifies the cints which are redoundant *)
begin try
let ubound = c_int_bounds_ival (is_cint g) in
let dom = (Tmap.find a domain) in
--
GitLab