Commit 46dbc9a1 authored by Loïc Correnson's avatar Loïc Correnson
Browse files

[WP] full resolution in script

parent 6dd146c5
......@@ -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 ;
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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
......
......@@ -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)
......
......@@ -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)
......
/* 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
......
......@@ -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
......
......@@ -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
......
Supports Markdown
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment