diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index af909388a75859ce192afc8e84976e67c7c22711..8e8d7bcb37a8b03584196ef37cbb404717b86b4b 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 78174d15cdf221a002c5b32a22ed8da79435290d..8d8078f18d59041ab10d8e51719f912da30e9c50 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 6893ddb27814038b4a1516ab4657ce25218d71d4..ceb23c74de9701f305ae7d32bf9c0060d5ca4524 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 b343e24d20cc2adf85d9ac0559431dece966b38b..4be16e756bda25b1418b3aef15f9967490f62397 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 31bf3423feb10d9348c935eec2ebb1da760a911a..ef6079503fca60854d404d895996ca21489bd285 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 4f621599bac38e47ca39ce0880501e65167c7dd6..8a4e9399f451a852b7e1338479604b6bf9f45d7a 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 bcf9b8a1f6f09696d76168b9fc53d18ad5bc52e1..e786ec578aca591188dffba000253a94180ce50d 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 } } } } }