From d8f24238fdcfe401d981e88ec2695b789b13d77d Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Fri, 8 Feb 2019 11:28:01 +0100
Subject: [PATCH] [wp] better consolidation of scripts
---
src/plugins/wp/ProofEngine.ml | 46 ++++++++++++++-----
src/plugins/wp/ProofEngine.mli | 2 +-
src/plugins/wp/ProverScript.ml | 4 +-
src/plugins/wp/VCS.ml | 29 ++++++++++++
src/plugins/wp/VCS.mli | 3 ++
.../oracle_qualif/unsigned.res.oracle | 2 +-
.../tests/wp_plugin/unsigned.i.0.report.json | 17 ++++---
7 files changed, 80 insertions(+), 23 deletions(-)
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index af909388a75..8e8d7bcb37a 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -116,7 +116,7 @@ let saved t = t.saved
let set_saved t s = t.saved <- s
(* -------------------------------------------------------------------------- *)
-(* --- Indexing --- *)
+(* --- Walking --- *)
(* -------------------------------------------------------------------------- *)
let rec walk f node =
@@ -125,6 +125,24 @@ let rec walk f node =
| Tactic (_,children) -> iter_all (walk f) children
| Opened | Script _ -> f node
+let rec witer f node =
+ let proved = Wpo.is_proved node.goal in
+ if proved then f ~proved node else
+ match node.script with
+ | Tactic (_,children) -> iter_all (witer f) children
+ | Opened | Script _ -> f ~proved node
+
+let iteri f tree =
+ match tree.root with
+ | None -> ()
+ | Some r ->
+ let k = ref 0 in
+ walk (fun node -> f !k node ; incr k) r
+
+(* -------------------------------------------------------------------------- *)
+(* --- Consolidating --- *)
+(* -------------------------------------------------------------------------- *)
+
let pending n =
let k = ref 0 in
walk (fun _ -> incr k) n ; !k
@@ -133,22 +151,26 @@ let has_pending n =
try walk (fun _ -> raise Exit) n ; false
with Exit -> true
-let iteri f tree =
- match tree.root with
- | None -> ()
- | Some r ->
- let k = ref 0 in
- walk (fun node -> f !k node ; incr k) r
+let consolidate root =
+ let result = ref VCS.valid in
+ witer
+ (fun ~proved:_ node ->
+ let rs = List.map snd (Wpo.get_results node.goal) in
+ result := VCS.merge !result (VCS.best rs) ;
+ ) root ;
+ !result
-let validate ?(unknown=false) tree =
+let validate ?(incomplete=false) tree =
match tree.root with
| None -> ()
- | Some r ->
+ | Some root ->
if not (Wpo.is_proved tree.main) then
- if not (has_pending r) then
+ if incomplete then
+ let result = consolidate root in
+ Wpo.set_result tree.main VCS.Tactical result
+ else
+ if not (has_pending root) then
Wpo.set_result tree.main VCS.Tactical VCS.valid
- else if unknown then
- Wpo.set_result tree.main VCS.Tactical VCS.unknown
(* -------------------------------------------------------------------------- *)
(* --- Accessors --- *)
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 78174d15cdf..8d8078f18d5 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -31,7 +31,7 @@ val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree
val reset : tree -> unit
val remove : Wpo.t -> unit
-val validate : ?unknown:bool -> tree -> unit
+val validate : ?incomplete:bool -> tree -> unit
(** Leaves are numbered from 0 to n-1 *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 6893ddb2781..ceb23c74de9 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -138,13 +138,13 @@ struct
let stuck env =
if not env.signaled then
begin
- ProofEngine.validate ~unknown:true env.tree ;
+ ProofEngine.validate ~incomplete:true env.tree ;
env.success (ProofEngine.main env.tree) None ;
env.signaled <- true ;
end
let validate ?(finalize=false) env =
- ProofEngine.validate ~unknown:true env.tree ;
+ ProofEngine.validate ~incomplete:true env.tree ;
if not env.signaled then
let wpo = ProofEngine.main env.tree in
let proved = Wpo.is_proved wpo in
diff --git a/src/plugins/wp/VCS.ml b/src/plugins/wp/VCS.ml
index b343e24d20c..4be16e756bd 100644
--- a/src/plugins/wp/VCS.ml
+++ b/src/plugins/wp/VCS.ml
@@ -366,3 +366,32 @@ let compare p q =
let t = Pervasives.compare p.prover_time q.prover_time in
if t <> 0 then t else
Pervasives.compare p.solver_time q.solver_time
+
+let combine v1 v2 =
+ match v1 , v2 with
+ | Valid , Valid -> Valid
+ | Failed , _ | _ , Failed -> Failed
+ | Invalid , _ | _ , Invalid -> Invalid
+ | Timeout , _ | _ , Timeout -> Timeout
+ | Stepout , _ | _ , Stepout -> Stepout
+ | _ -> Unknown
+
+let merge r1 r2 =
+ let err = if r1.prover_errmsg <> "" then r1 else r2 in
+ {
+ verdict = combine r1.verdict r2.verdict ;
+ solver_time = max r1.solver_time r2.solver_time ;
+ prover_time = max r1.prover_time r2.prover_time ;
+ prover_steps = max r1.prover_steps r2.prover_steps ;
+ prover_depth = max r1.prover_depth r2.prover_depth ;
+ prover_errpos = err.prover_errpos ;
+ prover_errmsg = err.prover_errmsg ;
+ }
+
+let choose r1 r2 =
+ match is_valid r1 , is_valid r2 with
+ | true , false -> r1
+ | false , true -> r2
+ | _ -> if compare r1 r2 <= 0 then r1 else r2
+
+let best = List.fold_left choose no_result
diff --git a/src/plugins/wp/VCS.mli b/src/plugins/wp/VCS.mli
index 31bf3423feb..ef6079503fc 100644
--- a/src/plugins/wp/VCS.mli
+++ b/src/plugins/wp/VCS.mli
@@ -131,6 +131,9 @@ val pp_result : Format.formatter -> result -> unit
val pp_result_perf : Format.formatter -> result -> unit
val compare : result -> result -> int (* best is minimal *)
+val merge : result -> result -> result
+val choose : result -> result -> result
+val best : result list -> result
val dkey_no_time_info: Wp_parameters.category
val dkey_no_step_info: Wp_parameters.category
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 4f621599bac..8a4e9399f45 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -10,5 +10,5 @@
[wp] Report 'tests/wp_plugin/unsigned.i.0.report.json'
-------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
-Lemma - - 1 100%
+Lemma - - (4..16) 1 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i.0.report.json b/src/plugins/wp/tests/wp_plugin/unsigned.i.0.report.json
index bcf9b8a1f6f..e786ec578ac 100644
--- a/src/plugins/wp/tests/wp_plugin/unsigned.i.0.report.json
+++ b/src/plugins/wp/tests/wp_plugin/unsigned.i.0.report.json
@@ -1,10 +1,13 @@
-{ "wp:global": { "script": { "total": 1, "valid": 1 },
- "wp:main": { "total": 1, "valid": 1 } },
- "wp:axiomatics": { "": { "lemma_U32": { "script": { "total": 1,
- "valid": 1 },
+{ "wp:global": { "script": { "total": 1, "valid": 1, "rank": 2 },
+ "wp:main": { "total": 1, "valid": 1, "rank": 2 } },
+ "wp:axiomatics": { "": { "lemma_U32": { "script": { "total": 1, "valid": 1,
+ "rank": 2 },
"wp:main": { "total": 1,
- "valid": 1 } },
+ "valid": 1,
+ "rank": 2 } },
"wp:section": { "script": { "total": 1,
- "valid": 1 },
+ "valid": 1,
+ "rank": 2 },
"wp:main": { "total": 1,
- "valid": 1 } } } } }
+ "valid": 1,
+ "rank": 2 } } } } }
--
GitLab