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

[wp] better consolidation of scripts

parent ceb9a93e
......@@ -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 --- *)
......
......@@ -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 *)
......
......@@ -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
......
......@@ -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
......@@ -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
......
......@@ -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%
-------------------------------------------------------------
{ "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 } } } } }
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