Commit c3ee29ac authored by Loïc Correnson's avatar Loïc Correnson Committed by Allan Blanchard
Browse files

[wp] improved consolidation for smoke tests

parent 0806835d
...@@ -29,6 +29,7 @@ type node = { ...@@ -29,6 +29,7 @@ type node = {
goal : Wpo.t ; (* only GoalAnnot of a sequent *) goal : Wpo.t ; (* only GoalAnnot of a sequent *)
parent : node option ; parent : node option ;
mutable script : script ; mutable script : script ;
mutable stats : Stats.stats ;
mutable search_index : int ; mutable search_index : int ;
mutable search_space : Strategy.t array ; (* sorted by priority *) mutable search_space : Strategy.t array ; (* sorted by priority *)
} }
...@@ -128,13 +129,6 @@ let rec walk f node = ...@@ -128,13 +129,6 @@ let rec walk f node =
| Tactic (_,children) -> iter_all (walk f) children | Tactic (_,children) -> iter_all (walk f) children
| Opened | Script _ -> f node | Opened | Script _ -> f node
let rec witer f node =
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
| Opened | Script _ -> f ~proved node
let iteri f tree = let iteri f tree =
match tree.root with match tree.root with
| None -> () | None -> ()
...@@ -152,30 +146,37 @@ let pending n = ...@@ -152,30 +146,37 @@ let pending n =
let k = ref 0 in let k = ref 0 in
walk (fun _ -> incr k) n ; !k walk (fun _ -> incr k) n ; !k
let has_pending n = let rec consolidate n =
try walk (fun _ -> raise Exit) n ; false let s =
with Exit -> true if Wpo.is_valid n.goal then
Stats.results ~smoke:false (Wpo.get_results n.goal)
let consolidate root = else
let result = ref VCS.valid in match n.script with
witer | Opened | Script _ -> Stats.empty
(fun ~proved:_ node -> | Tactic(_,children) ->
let rs = List.map snd (Wpo.get_results node.goal) in let qed = Wpo.qed_time n.goal in
result := VCS.merge !result (VCS.best rs) ; let results = List.map (fun (_,n) -> consolidate n) children in
) root ; Stats.tactical ~qed results
!result in n.stats <- s ; s
let validate ?(incomplete=false) tree = let validate tree =
match tree.root with match tree.root with
| None -> () | None -> ()
| Some root -> | Some root ->
if not (Wpo.is_valid tree.main) then if not (Wpo.is_valid tree.main) then
if incomplete then let stats = consolidate root in
let result = consolidate root in Wpo.set_result tree.main Tactical (Stats.script stats)
Wpo.set_result tree.main VCS.Tactical result
else let consolidated wpo =
if not (has_pending root) then let smoke = Wpo.is_smoke_test wpo in
Wpo.set_result tree.main VCS.Tactical VCS.valid let prs = Wpo.get_results wpo in
try
if Wpo.is_smoke_test wpo || not (PROOFS.mem wpo) then raise Not_found ;
match PROOFS.get wpo with
| { root = Some { stats ; script = Tactic _ } } -> stats
| _ -> raise Not_found
with Not_found ->
Stats.results ~smoke prs
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Accessors --- *) (* --- Accessors --- *)
...@@ -186,6 +187,7 @@ let head t = match t.head with ...@@ -186,6 +187,7 @@ let head t = match t.head with
| None -> t.main | None -> t.main
| Some n -> n.goal | Some n -> n.goal
let goal n = n.goal let goal n = n.goal
let stats n = n.stats
let tree_context t = Wpo.get_context t.main let tree_context t = Wpo.get_context t.main
let node_context n = Wpo.get_context n.goal let node_context n = Wpo.get_context n.goal
let parent n = n.parent let parent n = n.parent
...@@ -320,6 +322,7 @@ let mk_tree_node ~tree ~anchor goal = { ...@@ -320,6 +322,7 @@ let mk_tree_node ~tree ~anchor goal = {
tree = tree.main ; goal ; tree = tree.main ; goal ;
parent = Some anchor ; parent = Some anchor ;
script = Opened ; script = Opened ;
stats = Stats.empty ;
search_index = 0 ; search_index = 0 ;
search_space = [| |] ; search_space = [| |] ;
} }
...@@ -328,6 +331,7 @@ let mk_root_node goal = { ...@@ -328,6 +331,7 @@ let mk_root_node goal = {
tree = goal ; goal ; tree = goal ; goal ;
parent = None ; parent = None ;
script = Opened ; script = Opened ;
stats = Stats.empty ;
search_index = 0 ; search_index = 0 ;
search_space = [| |] ; search_space = [| |] ;
} }
......
...@@ -34,10 +34,14 @@ val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ] ...@@ -34,10 +34,14 @@ val get : Wpo.t -> [ `Script | `Proof | `Saved | `None ]
val proof : main:Wpo.t -> tree val proof : main:Wpo.t -> tree
val reset : tree -> unit val reset : tree -> unit
val remove : Wpo.t -> unit val remove : Wpo.t -> unit
val validate : ?incomplete:bool -> tree -> unit
(** Leaves are numbered from 0 to n-1 *) (** Re-compute stats & set status of the entire script *)
val validate : tree -> unit
(** Consolidate statistics wrt current script or prover results *)
val consolidated : Wpo.t -> Stats.stats
(** Leaves are numbered from 0 to n-1 *)
type status = [ type status = [
| `Unproved (** proof obligation not proved *) | `Unproved (** proof obligation not proved *)
...@@ -67,6 +71,7 @@ val node_context : node -> WpContext.t ...@@ -67,6 +71,7 @@ val node_context : node -> WpContext.t
val title : node -> string val title : node -> string
val proved : node -> bool val proved : node -> bool
val pending : node -> int val pending : node -> int
val stats : node -> Stats.stats
val parent : node -> node option val parent : node -> node option
val children : node -> (string * node) list val children : node -> (string * node) list
val tactical : node -> ProofScript.jtactic option val tactical : node -> ProofScript.jtactic option
......
...@@ -141,13 +141,13 @@ struct ...@@ -141,13 +141,13 @@ struct
let stuck env = let stuck env =
if not env.signaled then if not env.signaled then
begin begin
ProofEngine.validate ~incomplete:true env.tree ; ProofEngine.validate env.tree ;
env.success (ProofEngine.main env.tree) None ; env.success (ProofEngine.main env.tree) None ;
env.signaled <- true ; env.signaled <- true ;
end end
let validate ?(finalize=false) env = let validate ?(finalize=false) env =
ProofEngine.validate ~incomplete:true env.tree ; ProofEngine.validate env.tree ;
if not env.signaled then if not env.signaled then
let wpo = ProofEngine.main env.tree in let wpo = ProofEngine.main env.tree in
let proved = Wpo.is_valid wpo in let proved = Wpo.is_valid wpo in
......
...@@ -36,6 +36,7 @@ type pstats = { ...@@ -36,6 +36,7 @@ type pstats = {
} }
type stats = { type stats = {
verdict : VCS.verdict ;
provers : (VCS.prover * pstats) list ; provers : (VCS.prover * pstats) list ;
tactics : int ; tactics : int ;
proved : int ; proved : int ;
...@@ -84,11 +85,6 @@ let ptime t valid = ...@@ -84,11 +85,6 @@ let ptime t valid =
{ tmin = t ; tval = t ; tmax = t ; time = t ; tnbr = 1.0 ; { tmin = t ; tval = t ; tmax = t ; time = t ; tnbr = 1.0 ;
success = if valid then 1.0 else 0.0 } success = if valid then 1.0 else 0.0 }
let psmoke r =
{ pzero with
time = r.prover_time ;
success = if VCS.is_valid valid then 1.0 else 0.0 }
let pqed r = ptime r.solver_time (VCS.is_valid r) let pqed r = ptime r.solver_time (VCS.is_valid r)
let presult r = ptime r.prover_time (VCS.is_valid r) let presult r = ptime r.prover_time (VCS.is_valid r)
let psolver r = ptime r.solver_time false let psolver r = ptime r.solver_time false
...@@ -97,7 +93,8 @@ let psolver r = ptime r.solver_time false ...@@ -97,7 +93,8 @@ let psolver r = ptime r.solver_time false
(* --- Global Stats --- *) (* --- Global Stats --- *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
let zero = { let empty = {
verdict = NoResult;
provers = []; provers = [];
tactics = 0; tactics = 0;
proved = 0; proved = 0;
...@@ -108,46 +105,75 @@ let zero = { ...@@ -108,46 +105,75 @@ let zero = {
cached = 0 ; cached = 0 ;
} }
let choose (p,rp) (q,rq) = let choose_best a b =
if VCS.leq rp rq then (p,rp) else (q,rq) if VCS.leq (snd a) (snd b) then a else b
let choose_worst a b =
if VCS.leq (snd b) (snd a) then a else b
let consolidated ~smoke = function let consolidated_valid = function
| [] -> NoResult, 0, [] | [] -> NoResult, 0, []
| u::w as results -> | u::w as results ->
let p,r = List.fold_left choose u w in let p,r = List.fold_left choose_best u w in
let cached = let cached =
p = Qed || p = Qed ||
if VCS.is_valid r then r.cached else if VCS.is_valid r then r.cached else
List.for_all List.for_all
(fun (_,r) -> r.VCS.cached || not (VCS.is_verdict r)) (fun (_,r) -> r.VCS.cached || not (VCS.is_verdict r))
results in results in
r.verdict, r.VCS.verdict,
(if cached then 1 else 0), (if cached then 1 else 0),
if p = Qed then [Qed,pqed r] if p = Qed then [Qed,pqed r]
else pmerge [Qed,psolver r] [p,if smoke then psmoke r else presult r] else pmerge [Qed,psolver r] [p,presult r]
let smoked_result (p,r) = p, { r with verdict = VCS.smoked r.verdict }
let results ~smoke prs = let valid_stats prs =
let prs = if smoke then List.map smoked_result prs else prs in let verdict, cached, provers = consolidated_valid prs in
let verdict, cached, provers = consolidated ~smoke prs in
verdict,
match verdict with match verdict with
| Valid -> | Valid ->
{ zero with provers ; cached ; proved = 1 } { empty with verdict ; provers ; cached ; proved = 1 }
| Timeout | Stepout -> | Timeout | Stepout ->
{ zero with provers ; cached ; timeout = 1 } { empty with verdict ; provers ; cached ; timeout = 1 }
| Unknown -> | Unknown ->
{ zero with provers ; cached ; unknown = 1 } { empty with verdict ; provers ; cached ; unknown = 1 }
| NoResult | Computing _ -> | NoResult | Computing _ ->
{ zero with provers ; cached ; noresult = 1 } { empty with verdict ; provers ; cached ; noresult = 1 }
| Failed | Invalid -> | Failed | Invalid ->
{ zero with provers ; cached ; failed = 1 } { empty with verdict ; provers ; cached ; failed = 1 }
let results ~smoke prs =
if not smoke then valid_stats prs
else
let verdict, missing =
List.partition (fun (_,r) -> VCS.is_verdict r) prs in
let doomed, passed =
List.partition (fun (_,r) -> VCS.is_valid r) verdict in
if doomed <> [] then
valid_stats doomed
else
let cached = List.fold_left
(fun c (_,r) -> if r.VCS.cached then succ c else c)
0 doomed in
let stucked = List.map
(fun (p,r) -> p, ptime r.prover_time true)
doomed in
let solver = List.fold_left
(fun t (_,r) -> t +. r.solver_time)
0.0 doomed in
let provers = pmerge [Qed,ptime solver false] stucked in
let verdict =
if missing <> [] then NoResult else
match passed with
| [] -> NoResult
| u::w -> (snd @@ List.fold_left choose_worst u w).verdict in
let proved = List.length passed in
let failed = List.length missing + List.length doomed in
{ empty with verdict ; provers ; cached ; proved ; failed }
let add a b = let add a b =
if a == zero then b else if a == empty then b else
if b == zero then a else if b == empty then a else
{ {
verdict = VCS.combine a.verdict b.verdict ;
provers = pmerge a.provers b.provers ; provers = pmerge a.provers b.provers ;
tactics = a.tactics + b.tactics ; tactics = a.tactics + b.tactics ;
proved = a.proved + b.proved ; proved = a.proved + b.proved ;
...@@ -159,9 +185,19 @@ let add a b = ...@@ -159,9 +185,19 @@ let add a b =
} }
let tactical ~qed children = let tactical ~qed children =
let valid = children = [] in let valid = List.for_all (fun c -> c.verdict = Valid) children in
let provers = [Qed,ptime qed valid] in let qed_only = children = [] in
List.fold_left add { zero with provers ; tactics = 1 } children let verdict = if valid then Valid else Unknown in
let provers = [Qed,ptime qed qed_only] in
List.fold_left add { empty with verdict ; provers ; tactics = 1 } children
let script stats =
let cached = stats.cached = stats.proved in
let solver = List.fold_left
(fun t (p,s) -> if p = Qed then t +. s.time else t) 0.0 stats.provers in
let time = List.fold_left
(fun t (p,s) -> if p <> Qed then t +. s.time else t) 0.0 stats.provers in
VCS.result ~cached ~solver ~time stats.verdict
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Utils --- *) (* --- Utils --- *)
...@@ -195,20 +231,20 @@ let pp_pstats fmt p = ...@@ -195,20 +231,20 @@ let pp_pstats fmt p =
let pp_stats ~shell ~updating fmt s = let pp_stats ~shell ~updating fmt s =
let vp = s.proved in let vp = s.proved in
let np = proofs s in let np = proofs s in
if vp < np && np > 1 then
Format.fprintf fmt " (Proofs %d/%d)" vp np ;
if s.tactics > 1 then if s.tactics > 1 then
Format.fprintf fmt " (Tactics %d)" s.tactics Format.fprintf fmt " (Script %d)" s.tactics
else if np <= 1 && s.tactics = 1 then else if s.tactics = 1 then
Format.fprintf fmt " (Tactic)" ; Format.fprintf fmt " (Script)" ;
let perfo = not shell || (not updating && s.cached < vp) in let perfo = not shell || (not updating && s.cached < vp) in
let only_qed = match s.provers with [Qed,_] -> true | _ -> false in let qed_only =
match s.provers with [Qed,_] -> vp = np | _ -> false in
List.iter List.iter
(fun (p,pr) -> (fun (p,pr) ->
let success = truncate pr.success in let success = truncate pr.success in
let print_perfo = perfo && pr.time > Rformat.epsilon in let print_perfo = perfo && pr.time > Rformat.epsilon in
let print_proofs = success > 0 && np > 1 in let print_proofs = success > 0 && np > 1 in
if p != Qed || only_qed || print_perfo || print_proofs then let print_qed = qed_only && s.verdict = Valid && vp = np in
if p != Qed || print_qed || print_perfo || print_proofs then
begin begin
let title = VCS.title_of_prover ~version:false p in let title = VCS.title_of_prover ~version:false p in
Format.fprintf fmt " (%s" title ; Format.fprintf fmt " (%s" title ;
...@@ -229,6 +265,8 @@ let pp_stats ~shell ~updating fmt s = ...@@ -229,6 +265,8 @@ let pp_stats ~shell ~updating fmt s =
else else
Format.fprintf fmt " (Cached %d/%d)" s.cached np Format.fprintf fmt " (Cached %d/%d)" s.cached np
let pretty = pp_stats ~shell:false ~updating:false
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
(* --- Yojson --- *) (* --- Yojson --- *)
(* -------------------------------------------------------------------------- *) (* -------------------------------------------------------------------------- *)
......
...@@ -36,6 +36,7 @@ type pstats = { ...@@ -36,6 +36,7 @@ type pstats = {
(** Cumulated Stats *) (** Cumulated Stats *)
type stats = { type stats = {
verdict : VCS.verdict ;
provers : (VCS.prover * pstats) list ; provers : (VCS.prover * pstats) list ;
tactics : int ; tactics : int ;
proved : int ; proved : int ;
...@@ -48,9 +49,12 @@ type stats = { ...@@ -48,9 +49,12 @@ type stats = {
val pp_pstats : Format.formatter -> pstats -> unit val pp_pstats : Format.formatter -> pstats -> unit
val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit val pp_stats : shell:bool -> updating:bool -> Format.formatter -> stats -> unit
val pretty : Format.formatter -> stats -> unit
val results : smoke:bool -> (VCS.prover * VCS.result) list -> VCS.verdict * stats val empty : stats
val results : smoke:bool -> (VCS.prover * VCS.result) list -> stats
val tactical : qed:float -> stats list -> stats val tactical : qed:float -> stats list -> stats
val script : stats -> VCS.result
val proofs : stats -> int val proofs : stats -> int
val complete : stats -> bool val complete : stats -> bool
......
...@@ -41,8 +41,8 @@ let get_logout = Wpo.get_file_logout ...@@ -41,8 +41,8 @@ let get_logout = Wpo.get_file_logout
let get_logerr = Wpo.get_file_logerr let get_logerr = Wpo.get_file_logerr
let is_trivial = Wpo.is_trivial let is_trivial = Wpo.is_trivial
let is_valid = Wpo.is_valid let is_valid = Wpo.is_valid
let is_unknown = Wpo.is_unknown
let is_passed = Wpo.is_passed let is_passed = Wpo.is_passed
let has_unknown = Wpo.has_unknown
let get_formula po = let get_formula po =
match po.po_formula with match po.po_formula with
......
...@@ -48,11 +48,11 @@ val get_sequent : t -> Conditions.sequent ...@@ -48,11 +48,11 @@ val get_sequent : t -> Conditions.sequent
val get_formula: t -> Lang.F.pred val get_formula: t -> Lang.F.pred
val is_trivial : t -> bool val is_trivial : t -> bool
(** One prover at least returns Valid verdict. *) (** One prover at least returns a valid verdict. *)
val is_valid : t -> bool val is_valid : t -> bool
(** No prover with Valid verdict, and at least one non-Valid verdict. *) (** At least one non-valid verdict. *)
val is_unknown : t -> bool val has_unknown : t -> bool
(** Same as [is_valid] for non-smoke tests. For smoke-tests, (** Same as [is_valid] for non-smoke tests. For smoke-tests,
same as [is_unknown]. *) same as [is_unknown]. *)
......
...@@ -209,6 +209,7 @@ let is_result = function ...@@ -209,6 +209,7 @@ let is_result = function
let is_verdict r = is_result r.verdict let is_verdict r = is_result r.verdict
let is_valid = function { verdict = Valid } -> true | _ -> false let is_valid = function { verdict = Valid } -> true | _ -> false
let is_not_valid r = is_verdict r && not (is_valid r)
let is_computing = function { verdict=Computing _ } -> true | _ -> false let is_computing = function { verdict=Computing _ } -> true | _ -> false
let smoked = function let smoked = function
...@@ -349,16 +350,16 @@ let pp_result_qualif ?(updating=true) prover result fmt = ...@@ -349,16 +350,16 @@ let pp_result_qualif ?(updating=true) prover result fmt =
else else
pp_result fmt result pp_result fmt result
let vrank = function
| NoResult | Computing _ -> 0
| Failed -> 1
| Unknown -> 2
| Timeout | Stepout -> 3
| Valid -> 4
| Invalid -> 5
let compare p q = let compare p q =
let rank = function let r = vrank q.verdict - vrank p.verdict in
| NoResult | Computing _ -> 0
| Failed -> 1
| Unknown -> 2
| Timeout | Stepout -> 3
| Valid -> 4
| Invalid -> 5
in
let r = rank q.verdict - rank p.verdict in
if r <> 0 then r else if r <> 0 then r else
let s = Stdlib.compare p.prover_steps q.prover_steps in let s = Stdlib.compare p.prover_steps q.prover_steps in
if s <> 0 then s else if s <> 0 then s else
...@@ -394,5 +395,4 @@ let leq r1 r2 = ...@@ -394,5 +395,4 @@ let leq r1 r2 =
| _ -> compare r1 r2 <= 0 | _ -> compare r1 r2 <= 0
let choose r1 r2 = if leq r1 r2 then r1 else r2 let choose r1 r2 = if leq r1 r2 then r1 else r2
let best = List.fold_left choose no_result let best = List.fold_left choose no_result
...@@ -114,6 +114,7 @@ val is_auto : prover -> bool ...@@ -114,6 +114,7 @@ val is_auto : prover -> bool
val is_result : verdict -> bool val is_result : verdict -> bool
val is_verdict : result -> bool val is_verdict : result -> bool
val is_valid: result -> bool val is_valid: result -> bool
val is_not_valid: result -> bool
val is_computing: result -> bool val is_computing: result -> bool
val is_proved: smoke:bool -> result -> bool val is_proved: smoke:bool -> result -> bool
...@@ -129,6 +130,7 @@ val pp_result_qualif : ?updating:bool -> prover -> result -> ...@@ -129,6 +130,7 @@ val pp_result_qualif : ?updating:bool -> prover -> result ->
val compare : result -> result -> int (* best is minimal *) val compare : result -> result -> int (* best is minimal *)
val combine : verdict -> verdict -> verdict
val merge : result -> result -> result val merge : result -> result -> result
val leq : result -> result -> bool val leq : result -> result -> bool
val choose : result -> result -> result val choose : result -> result -> result
......
...@@ -139,7 +139,7 @@ class behavior ...@@ -139,7 +139,7 @@ class behavior
| `All -> true | `All -> true
| `Smoke -> Wpo.is_smoke_test g | `Smoke -> Wpo.is_smoke_test g
| `Scripts -> has_proof g | `Scripts -> has_proof g
| `ToProve -> to_prove g && (Wpo.is_unknown g || has_proof g) | `ToProve -> to_prove g && (Wpo.has_unknown g || has_proof g)
in if ok then list#add g in if ok then list#add g
in in