# HG changeset patch # User paulson # Date 880710724 -3600 # Node ID 561242f8606b92db2b6630febb8249badf39826f # Parent 5f5df208b0e0ab6beccff4491a2eca0a6c09b613 Printing of statistics including time for search & reconstruction diff -r 5f5df208b0e0 -r 561242f8606b src/Provers/blast.ML --- a/src/Provers/blast.ML Fri Nov 28 10:36:08 1997 +0100 +++ b/src/Provers/blast.ML Fri Nov 28 10:52:04 1997 +0100 @@ -90,6 +90,7 @@ val Blast_tac : int -> tactic val overloaded : string * (Term.typ -> Term.typ) -> unit (*debugging tools*) + val stats : bool ref val trace : bool ref val fullTrace : branch list list ref val fromType : (indexname * term) list ref -> Term.typ -> term @@ -113,7 +114,8 @@ type claset = Data.claset; -val trace = ref false; +val trace = ref false +and stats = ref false; (*for runtime and search statistics*) datatype term = Const of string @@ -879,15 +881,25 @@ val nclosed = ref 0 and ntried = ref 1; +fun printStats (b, start) = + if b then + writeln (endTiming start ^ " for search. Closed: " + ^ Int.toString (!nclosed) ^ + " tried: " ^ Int.toString (!ntried)) + else (); + + (*Tableau prover based on leanTaP. Argument is a list of branches. Each branch contains a list of unexpanded formulae, a list of literals, and a bound on unsafe expansions.*) fun prove (sign, cs, brs, cont) = - let val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs + let val start = startTiming() + val {safe0_netpair, safep_netpair, haz_netpair, ...} = Data.rep_claset cs val safeList = [safe0_netpair, safep_netpair] and hazList = [haz_netpair] fun prv (tacs, trs, choices, []) = - cont (tacs, trs, choices) (*all branches closed!*) + (printStats (!trace orelse !stats, start); + cont (tacs, trs, choices)) (*all branches closed!*) | prv (tacs, trs, choices, brs0 as (((G,md)::br, haz)::pairs, lits, vars, lim) :: brs) = (*apply a safe rule only (possibly allowing instantiation); @@ -1172,31 +1184,29 @@ nclosed := 0; ntried := 1); -fun printStats b = - if b then - (writeln ("Branches closed: " ^ Int.toString (!nclosed)); - writeln ("Branches tried: " ^ Int.toString (!ntried))) - else (); - - (*Tactic using tableau engine and proof reconstruction. "lim" is depth limit.*) fun depth_tac cs lim i st = - (initialize(); - let val {sign,...} = rep_thm st - val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) - val hyps = strip_imp_prems skoprem - and concl = strip_imp_concl skoprem - fun cont (tacs,_,choices) = - (case Seq.pull(EVERY' (rev tacs) i st) of - None => (writeln ("PROOF FAILED for depth " ^ - Int.toString lim); - backtrack choices) - | cell => Seq.make(fn()=> cell)) - in #1 (prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont), - printStats (!trace)) - end - handle PROVE => Seq.empty); + (initialize(); + let val {sign,...} = rep_thm st + val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) + val hyps = strip_imp_prems skoprem + and concl = strip_imp_concl skoprem + fun cont (tacs,_,choices) = + let val start = startTiming() + in + case Seq.pull(EVERY' (rev tacs) i st) of + None => (writeln ("PROOF FAILED for depth " ^ + Int.toString lim); + backtrack choices) + | cell => (if (!trace orelse !stats) + then writeln (endTiming start ^ " for reconstruction") + else (); + Seq.make(fn()=> cell)) + end + in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont) + end + handle PROVE => Seq.empty); fun blast_tac cs i st = (DEEPEN (1,20) (depth_tac cs) 0) i st handle TRANS s => (warning ("Blast_tac: " ^ s); Seq.empty); @@ -1215,9 +1225,7 @@ val skoprem = fromSubgoal (List.nth(prems_of st, i-1)) val hyps = strip_imp_prems skoprem and concl = strip_imp_concl skoprem - in #1 (timeap prove - (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I), - printStats true) + in timeap prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I) end handle Subscript => error("There is no subgoal " ^ Int.toString i)); @@ -1229,11 +1237,10 @@ fun tryInThy thy lim s = (initialize(); - #1 (timeap prove (sign_of thy, - Data.claset(), - [initBranch ([readGoal (sign_of thy) s], lim)], - I), - printStats true)); + timeap prove (sign_of thy, + Data.claset(), + [initBranch ([readGoal (sign_of thy) s], lim)], + I)); end;