diff --git a/src/plugins/wp/GuiGoal.ml b/src/plugins/wp/GuiGoal.ml
index a728026f5dcea8c5e71bd8d638c9f68a03688ecb..9ba3bf0cc946a7afb8a246f85e5c5817624d3900 100644
--- a/src/plugins/wp/GuiGoal.ml
+++ b/src/plugins/wp/GuiGoal.ml
@@ -551,7 +551,7 @@ class pane (proverpane : GuiConfig.provers) =
let n = Task.size pool in
if n = 0 then
begin
- ignore (ProofEngine.commit ~resolve:false fork) ;
+ ignore (ProofEngine.commit fork) ;
ProofEngine.validate proof ;
ProofEngine.forward proof ;
state <- Proof proof ;
diff --git a/src/plugins/wp/GuiNavigator.ml b/src/plugins/wp/GuiNavigator.ml
index 7da1c5d3d9f9a6dc365f93b24f5c4d18001792ee..0b97d0de9e790f28775d5e04d2d93fd736323ddd 100644
--- a/src/plugins/wp/GuiNavigator.ml
+++ b/src/plugins/wp/GuiNavigator.ml
@@ -123,7 +123,7 @@ class behavior
method reload () =
begin
list#reload ;
- let to_prove g = not (Wpo.is_proved g || Wpo.resolve g) in
+ let to_prove g = not (Wpo.is_proved g || Wpo.reduce g) in
let has_proof g =
match ProofEngine.get g with
| `None -> false
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index 8e8d7bcb37a8b03584196ef37cbb404717b86b4b..acc7f935ca2acbd308d663ba09ac3d3021ba8e5e 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -52,13 +52,15 @@ module PROOFS = Model.StaticGenerator(Wpo.S)
type key = Wpo.S.t
type data = tree
let name = "Wp.ProofEngine.Proofs"
- let compile main = {
- main ; gid = 0 ;
- pool = None ;
- head = None ;
- root = None ;
- saved = false ;
- }
+ let compile main =
+ ignore (Wpo.resolve main) ;
+ {
+ main ; gid = 0 ;
+ pool = None ;
+ head = None ;
+ root = None ;
+ saved = false ;
+ }
end)
let () = Wpo.on_remove PROOFS.remove
@@ -143,6 +145,8 @@ let iteri f tree =
(* --- Consolidating --- *)
(* -------------------------------------------------------------------------- *)
+let proved n = Wpo.is_proved n.goal
+
let pending n =
let k = ref 0 in
walk (fun _ -> incr k) n ; !k
@@ -212,7 +216,6 @@ let status t : status =
`Pending (pending root)
-let proved n = Wpo.is_proved n.goal
let opened n = not (Wpo.is_proved n.goal)
let state n =
@@ -387,14 +390,11 @@ let anchor tree ?node () =
| Some n -> n
| None -> mk_root tree
-let commit ~resolve fork =
- let resolved (_,wp) =
- Wpo.is_proved wp || ( resolve && Wpo.resolve wp ) in
- let resolved , residual = List.partition resolved fork.Fork.goals in
- iter_all Wpo.remove resolved ;
+let commit fork =
+ List.iter (fun (_,wp) -> ignore (Wpo.resolve wp)) fork.Fork.goals ;
let tree = fork.Fork.tree in
let anchor = fork.Fork.anchor in
- let children = map_all (mk_tree_node ~tree ~anchor) residual in
+ let children = map_all (mk_tree_node ~tree ~anchor) fork.Fork.goals in
tree.saved <- false ;
anchor.script <- Tactic( fork.Fork.tactic , children ) ;
anchor , children
diff --git a/src/plugins/wp/ProofEngine.mli b/src/plugins/wp/ProofEngine.mli
index 8d8078f18d59041ab10d8e51719f912da30e9c50..53299b7b63a39b8e710cc0ed309981adb6291dc0 100644
--- a/src/plugins/wp/ProofEngine.mli
+++ b/src/plugins/wp/ProofEngine.mli
@@ -71,7 +71,7 @@ type fork
val anchor : tree -> ?node:node -> unit -> node
val fork : tree -> anchor:node -> ProofScript.jtactic -> Tactical.process -> fork
val iter : (Wpo.t -> unit) -> fork -> unit
-val commit : resolve:bool -> fork -> node * (string * node) list
+val commit : fork -> node * (string * node) list
val pretty : Format.formatter -> fork -> unit
val script : tree -> ProofScript.jscript
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index ceb23c74de9701f305ae7d32bf9c0060d5ca4524..3ccf4f59b6873a055a172ced0622f3e5ae6cfbbf 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -299,7 +299,7 @@ and autosearch env ~depth node : bool Task.task =
| Some fork -> autofork env ~depth fork
and autofork env ~depth fork =
- let _,children = ProofEngine.commit ~resolve:true fork in
+ let _,children = ProofEngine.commit fork in
let pending = Env.pending env in
if pending > 0 then
begin
@@ -346,7 +346,7 @@ let rec crawl env on_child node = function
begin
match jfork (Env.tree env) ?node jtactic with
| None ->
- Wp_parameters.error
+ Wp_parameters.warning
"Script Error: can not apply '%s'@\n\
@[<hov 2>Params: %a@]@\n\
@[<hov 2>Select: %a@]@."
@@ -356,9 +356,12 @@ let rec crawl env on_child node = function
crawl env on_child node alternative
| Some fork ->
(*TODO: saveback forgiven script *)
- let _,children = ProofEngine.commit ~resolve:true fork in
+ let _,children = ProofEngine.commit fork in
reconcile children subscripts ;
- if children = [] then
+ let residual = List.filter
+ (fun (_,node) -> not (ProofEngine.proved node))
+ children in
+ if residual = [] then
Env.validate env
else
List.iter (fun (_,n) -> on_child n) children ;
@@ -375,8 +378,11 @@ let schedule job =
let rec process env node =
schedule
begin fun () ->
- let script = Priority.sort (ProofEngine.bound node) in
- crawl env (process env) (Some node) script
+ if ProofEngine.proved node then
+ ( Env.validate env ; Task.return () )
+ else
+ let script = Priority.sort (ProofEngine.bound node) in
+ crawl env (process env) (Some node) script
end
let task
diff --git a/src/plugins/wp/cfgWP.ml b/src/plugins/wp/cfgWP.ml
index e58d1977ed7cb42caad44cd5aabe3d81ea4e6ce2..7a9212ebaee5782462b178c33633f3b37741d27c 100644
--- a/src/plugins/wp/cfgWP.ml
+++ b/src/plugins/wp/cfgWP.ml
@@ -1466,7 +1466,7 @@ struct
begin
Wp_parameters.feedback ~ontty:`Transient "Collecting checks" ;
Bag.iter
- (fun w -> ignore (Wpo.resolve w))
+ (fun w -> ignore (Wpo.reduce w))
!collection ;
Lang.F.Check.iter (add_qed_check collection m) ;
end
diff --git a/src/plugins/wp/prover.ml b/src/plugins/wp/prover.ml
index 4de85cbcd9ab13a9ffdbc5ed2c8f883adcdd26d3..bc18054056ee79ce17a0b201df3c98f2e3c78cb5 100644
--- a/src/plugins/wp/prover.ml
+++ b/src/plugins/wp/prover.ml
@@ -76,7 +76,7 @@ let simplify ?start ?result wpo =
VCS.( r.verdict == Valid ) ||
begin
started ?start wpo ;
- if resolve wpo then
+ if Wpo.reduce wpo then
let time = qed_time wpo in
let res = VCS.result ~time VCS.Valid in
(update ?result wpo VCS.Qed res ; true)
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index ae5dcd02429cb933efa456d8861aebe6664703c3..dbb0bcfefa3cd1cc8b0ca355235d751a04ea682f 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -168,10 +168,6 @@ let pp_warnings fmt wpo =
| false , _ -> Format.fprintf fmt " (Stronger, %d warnings)" n
end
-let auto_check = function
- | { Wpo.po_formula = Wpo.GoalCheck _ } -> true
- | _ -> false
-
let launch task =
let server = ProverTask.server () in
(** Do on_server_stop save why3 session *)
@@ -359,7 +355,7 @@ let do_wpo_success goal s =
end
end
| Some prover ->
- if not (auto_check goal) then
+ if not (Wpo.is_check goal) then
Wp_parameters.feedback ~ontty:`Silent
"[%a] Goal %s : Valid" VCS.pp_prover prover (Wpo.get_gid goal)
diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i
index dd79473b668aa1805dba478d721bcfe5552c158e..5ac917b0ddb23b34e0df8188e75e75a800e4a895 100644
--- a/src/plugins/wp/tests/wp_plugin/unroll.i
+++ b/src/plugins/wp/tests/wp_plugin/unroll.i
@@ -1,5 +1,5 @@
/* run.config
- OPT: -ulevel=1 -wp -wp-prop=@ensures -wp-prover script -session tests/wp_plugin/unroll
+ OPT: -ulevel=1 -wp -wp-prop=@ensures -wp-prover script -session tests/wp_plugin/unroll -wp-msg-key no-time-info,no-step-info
*/
/* run.config_qualif
diff --git a/src/plugins/wp/wpo.ml b/src/plugins/wp/wpo.ml
index 8a20407e53338db5485ec741ba9092b980ec6bbe..b4ff5124a5c54d708891290a466c0566b4c08f0f 100644
--- a/src/plugins/wp/wpo.ml
+++ b/src/plugins/wp/wpo.ml
@@ -805,11 +805,19 @@ let is_trivial g =
| GoalAnnot vc -> VC_Annot.is_trivial vc
| GoalCheck _ -> false
-let resolve g =
+
+let reduce g =
match g.po_formula with
- | GoalAnnot vc -> Model.with_model g.po_model VC_Annot.resolve vc
- | GoalLemma vc -> Model.with_model g.po_model VC_Lemma.is_trivial vc
| GoalCheck _ -> false
+ | GoalLemma vc -> Model.with_model g.po_model VC_Lemma.is_trivial vc
+ | GoalAnnot vc -> Model.with_model g.po_model VC_Annot.resolve vc
+
+let resolve g =
+ let valid = reduce g in
+ if valid then
+ ( let solver = qed_time g in
+ set_result g VCS.Qed (VCS.result ~solver VCS.Valid) ) ;
+ valid
let compute g =
match g.po_formula with
diff --git a/src/plugins/wp/wpo.mli b/src/plugins/wp/wpo.mli
index 9413c844b02e32eb94e06c950d0af43196378001..ffe0871674f0f168c3d62bae4c5d4a78d1960e0b 100644
--- a/src/plugins/wp/wpo.mli
+++ b/src/plugins/wp/wpo.mli
@@ -157,7 +157,8 @@ val on_remove : (t -> unit) -> unit
val add : t -> unit
val age : t -> int (* generation *)
-val resolve : t -> bool (** tries simplification *)
+val reduce : t -> bool (** tries simplification *)
+val resolve : t -> bool (** tries simplification and set result if valid *)
val set_result : t -> prover -> result -> unit
val clear_results : t -> unit