From 3fff959874a5eed07ac11a96daf645e0f77e5978 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Tue, 9 May 2023 16:49:13 +0200
Subject: [PATCH] [wp] replay stronger prover alternative
---
src/plugins/wp/Cache.ml | 4 ++--
src/plugins/wp/Cache.mli | 5 +++++
src/plugins/wp/ProverScript.ml | 2 +-
3 files changed, 8 insertions(+), 3 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 1a7bcaac2e5..76ff4b37443 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -162,7 +162,7 @@ let steps_seized steps steplimit =
| None | Some 0 -> false
| Some limit -> limit <= steps
-let promote ~timeout ~steplimit (res : VCS.result) =
+let promote ?timeout ?steplimit (res : VCS.result) =
match res.verdict with
| VCS.NoResult | VCS.Computing _ -> VCS.no_result
| VCS.Failed -> res
@@ -273,7 +273,7 @@ let get_result ~digest ~runner ~timeout ~steplimit prover goal =
let hash = lazy (digest prover goal) in
let result =
get_cache_result ~mode hash
- |> promote ~timeout ~steplimit |> VCS.cached in
+ |> promote ?timeout ?steplimit |> VCS.cached in
if VCS.is_verdict result
then
begin
diff --git a/src/plugins/wp/Cache.mli b/src/plugins/wp/Cache.mli
index f017a12efeb..5ee0e5deec0 100644
--- a/src/plugins/wp/Cache.mli
+++ b/src/plugins/wp/Cache.mli
@@ -41,6 +41,11 @@ type 'a runner =
timeout:float option -> steplimit:int option -> Why3Provers.t -> 'a ->
VCS.result Task.task
+val promote: ?timeout:float -> ?steplimit:int -> VCS.result -> VCS.result
+(** Converts some known results to the given limits.
+ In particular, if the result shall be discarded with respect to the limits,
+ the function returns [VCS.no_result]. *)
+
val get_result: digest:('a digest) -> runner:('a runner) -> 'a runner
val clear_result: digest:('a digest) -> Why3Provers.t -> 'a -> unit
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 9277e1d3beb..bb8daa671f0 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -349,7 +349,7 @@ and explore_provers env alternative : solver =
and explore_prover env timeout prover node =
let wpo = ProofEngine.goal node in
- let result = Wpo.get_result wpo prover in
+ let result = Cache.promote ~timeout @@ Wpo.get_result wpo prover in
if VCS.is_valid result then success else
if VCS.is_verdict result then failed else
let config = { VCS.default with timeout = Some timeout } in
--
GitLab