From 23d62745bc72bdafcbad835e5eb55127dce54dc7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 16 Sep 2020 14:56:33 +0200
Subject: [PATCH] [wp] fix simplification callback in prover script
---
src/plugins/wp/ProverScript.ml | 23 +++++++++++++----------
src/plugins/wp/prover.mli | 5 +++++
src/plugins/wp/wpo.ml | 3 +--
3 files changed, 19 insertions(+), 12 deletions(-)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index e9b4d301ca5..2a96d02786d 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -392,16 +392,19 @@ let task
~depth ~width ~backtrack ~auto
~start ~progress ~result ~success wpo =
begin fun () ->
- start wpo ;
- let json = ProofSession.load wpo in
- let script = Priority.sort (ProofScript.decode json) in
- let tree = ProofEngine.proof ~main:wpo in
- let env = Env.make tree
- ~valid ~failed ~provers
- ~depth ~width ~backtrack ~auto
- ~progress ~result ~success in
- crawl env (process env) None script >>?
- (fun _ -> ProofEngine.forward tree) ;
+ Prover.simplify ~start ~result wpo >>= fun succeed ->
+ if succeed
+ then Task.return ()
+ else
+ let json = ProofSession.load wpo in
+ let script = Priority.sort (ProofScript.decode json) in
+ let tree = ProofEngine.proof ~main:wpo in
+ let env = Env.make tree
+ ~valid ~failed ~provers
+ ~depth ~width ~backtrack ~auto
+ ~progress ~result ~success in
+ crawl env (process env) None script >>?
+ (fun _ -> ProofEngine.forward tree) ;
end
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/prover.mli b/src/plugins/wp/prover.mli
index 6a2711c2704..32e1ca6ff6a 100644
--- a/src/plugins/wp/prover.mli
+++ b/src/plugins/wp/prover.mli
@@ -26,6 +26,11 @@ open VCS
(* --- Prover Implementation against Task API --- *)
(* -------------------------------------------------------------------------- *)
+val simplify :
+ ?start:(Wpo.t -> unit) ->
+ ?result:(Wpo.t -> prover -> result -> unit) ->
+ Wpo.t -> bool Task.task
+
val prove : Wpo.t ->
?config:config ->
?mode:mode ->
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index e84e2fec240..867d238326d 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -814,8 +814,7 @@ let resolve g =
let valid = reduce g in
if valid then
let result = VCS.result ~solver:(qed_time g) VCS.Valid in
- ignore (set_result g VCS.Qed result) ;
- true
+ ( set_result g VCS.Qed result ; true )
else false
let compute g =
--
GitLab