diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 84c3aa22696a3e6eb4d64eb5f05ad3bae353017e..4d7794474d2f920f9dd6c27e89524573862cd13b 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -122,13 +122,13 @@ let set_saved t s = t.saved <- s
(* -------------------------------------------------------------------------- *)
let rec walk f node =
- if not (Wpo.is_proved node.goal) then
+ if not (Wpo.is_valid node.goal) then
match node.script with
| Tactic (_,children) -> iter_all (walk f) children
| Opened | Script _ -> f node
let rec witer f node =
- let proved = Wpo.is_proved node.goal in
+ let proved = Wpo.is_valid node.goal in
if proved then f ~proved node else
match node.script with
| Tactic (_,children) -> iter_all (witer f) children
@@ -145,7 +145,7 @@ let iteri f tree =
(* --- Consolidating --- *)
(* -------------------------------------------------------------------------- *)
-let proved n = Wpo.is_proved n.goal
+let proved n = Wpo.is_valid n.goal
let pending n =
let k = ref 0 in
@@ -168,7 +168,7 @@ let validate ?(incomplete=false) tree =
match tree.root with
| None -> ()
| Some root ->
- if not (Wpo.is_proved tree.main) then
+ if not (Wpo.is_valid tree.main) then
if incomplete then
let result = consolidate root in
Wpo.set_result tree.main VCS.Tactical result
@@ -217,7 +217,7 @@ type status = [
let status t : status =
match t.root with
| None ->
- if Wpo.is_proved t.main
+ if Wpo.is_valid t.main
then if Wpo.is_smoke_test t.main then `Invalid else `Proved
else if Wpo.is_smoke_test t.main then `Passed else `Unproved
| Some root ->
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index 879fa822652884e147de9e388a7282b088515d57..652b0220a8881bcf08bbc3795cec6c4b7aed4b14 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -150,7 +150,7 @@ struct
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
+ let proved = Wpo.is_valid wpo in
if proved || finalize then
begin
env.signaled <- true ;
diff --git a/src/plugins/wp/VC.ml b/src/plugins/wp/VC.ml
index 5909360a0e0e06cb2f3875d758db88e64207e8e0..cf8ebc3518c2b63037d4adcccbc1855f0dbc320f 100644
--- a/src/plugins/wp/VC.ml
+++ b/src/plugins/wp/VC.ml
@@ -40,7 +40,9 @@ let get_results = Wpo.get_results
let get_logout = Wpo.get_file_logout
let get_logerr = Wpo.get_file_logerr
let is_trivial = Wpo.is_trivial
-let is_proved = Wpo.is_proved
+let is_valid = Wpo.is_valid
+let is_unknown = Wpo.is_unknown
+let is_passed = Wpo.is_passed
let get_formula po =
match po.po_formula with
diff --git a/src/plugins/wp/VC.mli b/src/plugins/wp/VC.mli
index 60140062de2e61534c7560dcdd97c83f66f38bd7..ac4abf38e2ab22013499372240ac1a6bb6a39365 100644
--- a/src/plugins/wp/VC.mli
+++ b/src/plugins/wp/VC.mli
@@ -47,7 +47,16 @@ val get_logerr : t -> prover -> string
val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred
val is_trivial : t -> bool
-val is_proved : t -> bool
+
+(** One prover at least returns Valid verdict. *)
+val is_valid : t -> bool
+
+(** No prover with Valid verdict, and at least one non-Valid verdict. *)
+val is_unknown : t -> bool
+
+(** Same as [is_valid] for non-smoke tests. For smoke-tests,
+ same as [is_unknown]. *)
+val is_passed : t -> bool
(** {2 Database}
Notice that a property or a function have no proof obligation until you
diff --git a/src/plugins/wp/gui/GuiNavigator.ml b/src/plugins/wp/gui/GuiNavigator.ml
index e39380a3381dd45a5217b3267096eeeaf31fb888..c99c230f6472feecdc4e2427d1ae43aa2c79bd72 100644
--- a/src/plugins/wp/gui/GuiNavigator.ml
+++ b/src/plugins/wp/gui/GuiNavigator.ml
@@ -128,7 +128,7 @@ class behavior
list#reload ;
let to_prove g =
not (Wpo.is_smoke_test g) &&
- not (Wpo.is_proved g || Wpo.reduce g) in
+ not (Wpo.is_valid g || Wpo.reduce g) in
let has_proof g =
match ProofEngine.get g with
| `None -> false
diff --git a/src/plugins/wp/gui/GuiProof.ml b/src/plugins/wp/gui/GuiProof.ml
index b258d11f1e5c0f3cc4b1104717525b5e4e3c6779..267456cd06c0a4580f5d26c725457e8a1a81a277 100644
--- a/src/plugins/wp/gui/GuiProof.ml
+++ b/src/plugins/wp/gui/GuiProof.ml
@@ -193,7 +193,7 @@ class printer (text : Wtext.text) =
| `Internal here | `Leaf(_,here) ->
begin
let root,path = rootchain here [here] in
- let qed = if Wpo.is_proved (ProofEngine.main tree) then "Qed" else "End"
+ let qed = if Wpo.is_valid (ProofEngine.main tree) then "Qed" else "End"
in text#printf "@[<hv 0>@{<bf>Proof@}:%a@\n@{<bf>%s@}.@]@."
(self#proofstep ~prefix:" " ~direct:" " ~path ~here) root qed ;
end
diff --git a/src/plugins/wp/wpReport.ml b/src/plugins/wp/wpReport.ml
index bf3d4d0832752d07c36b59bbf04109e1b3a5f551..e6f676b11d719c300f3ec6391fd087b2d5a19e7d 100644
--- a/src/plugins/wp/wpReport.ml
+++ b/src/plugins/wp/wpReport.ml
@@ -215,8 +215,8 @@ let add_results ~status (plist:pstats list) (wpo:Wpo.t) =
List.iter
(fun (p,r) ->
let re = result ~status ~smoke r in
- let st = Wpo.get_steps r in
- let tc = Wpo.get_time r in
+ let st = r.VCS.prover_steps in
+ let tc = r.VCS.prover_time in
let ts = r.VCS.solver_time in
if re <> NORESULT then
begin
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 9d50a7ad9f4a4d2982aea40ca6a65d596b1a2b55..d21eb22095cfe5e1361c2a8a4ecd77d567de4ccd 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -693,8 +693,6 @@ let warnings = function
| { po_formula = GoalAnnot vcq } -> vcq.VC_Annot.warn
| { po_formula = GoalLemma _ } -> []
-let get_time = function { prover_time=t } -> t
-let get_steps= function { prover_steps=n } -> n
let get_target g = WpPropId.property_of_id g.po_pid
let get_proof g =
@@ -813,27 +811,20 @@ let compute g =
Some( lemma.l_cluster , depends ) ,
WpContext.on_context ctxt VC_Lemma.sequent w
-let is_proved g =
+let is_valid g =
is_trivial g || List.exists (fun (_,r) -> VCS.is_valid r) (get_results g)
-let is_unknown g = List.exists
+let is_unknown g =
+ not (is_valid g) &&
+ List.exists
(fun (_,r) -> VCS.is_verdict r && not (VCS.is_valid r))
- ( get_results g )
+ (get_results g)
let is_passed g =
if is_smoke_test g then
- not (is_proved g)
+ is_unknown g
else
- is_proved g
-
-let get_result =
- Dynamic.register ~plugin:"Wp" "Wpo.get_result"
- (Datatype.func2 WpoType.ty ProverType.ty ResultType.ty)
- get_result
-
-let is_valid =
- Dynamic.register ~plugin:"Wp" "Wpo.is_valid"
- (Datatype.func ResultType.ty Datatype.bool) VCS.is_valid
+ is_valid g
(* -------------------------------------------------------------------------- *)
(* --- Proof Obligations : Pretty-printing --- *)
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 93ddc06982ba7dff8a5fa43395173c4c86f13676..2cc7c59e74cbcb6db40d230dd56947588af1c254 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -158,33 +158,43 @@ val clear_results : t -> unit
val compute : t -> Definitions.axioms option * Conditions.sequent
+(** Warning: Prover results are stored as they are from prover output,
+ without taking into consideration that validity is inverted
+ for smoke tests.
+
+ On the contrary, proof validity is computed with respect to
+ smoke test/non-smoke test.
+*)
+
+(** Definite result for this prover (not computing) *)
val has_verdict : t -> prover -> bool
+
+(** Raw prover result (without any respect to smoke tests) *)
val get_result : t -> prover -> result
+
+(** All raw prover results (without any respect to smoke tests) *)
val get_results : t -> (prover * result) list
+
+(** Consolidated wrt to associated property and smoke test. *)
val get_proof : t -> [`Passed|`Failed|`Unknown] * Property.t
+
+(** Associated property. *)
val get_target : t -> Property.t
+
val is_trivial : t -> bool
-(** do not tries simplification, do not check prover results *)
+(** Currently trivial sequent (no forced simplification) *)
-val is_proved : t -> bool
-(** do not tries simplification, check prover results *)
+val is_valid : t -> bool
+(** Checks for some prover with valid verdict (no forced simplification) *)
val is_unknown : t -> bool
-(** at least one prover returns « Unknown » *)
+(** Checks that all provers has a non-valid verdict *)
val is_passed : t -> bool
-(** proved, or unknown for smoke tests *)
+(** valid, or unknown for smoke tests *)
val warnings : t -> Warning.t list
-(** [true] if the result is valid. Dynamically exported.
- @since Nitrogen-20111001
-*)
-val is_valid: result -> bool
-
-val get_time: result -> float
-val get_steps: result -> int
-
val is_tactic : t -> bool
val is_smoke_test : t -> bool