# HG changeset patch
# User paulson
# Date 880559394 -3600
# Node ID 451ae21dca28150b6349d275417b2fec433a0a7e
# Parent  22596d62ce0b1c5d2c94b0fc9b4e751d5e8a08fb
Statistics

diff -r 22596d62ce0b -r 451ae21dca28 src/Provers/blast.ML
--- a/src/Provers/blast.ML	Wed Nov 26 16:49:07 1997 +0100
+++ b/src/Provers/blast.ML	Wed Nov 26 16:49:54 1997 +0100
@@ -874,6 +874,11 @@
   | match t               u   = false;
 
 
+(*Branches closed: number of branches closed during the search
+  Branches tried:  number of branches created by splitting (counting from 1)*)
+val nclosed = ref 0
+and ntried  = ref 1;
+
 (*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.*)
@@ -923,16 +928,18 @@
 		     in
 			 traceNew prems;  traceVars sign ntrl;
 			 (if null prems then (*closed the branch: prune!*)
-			    prv(tacs',  brs0::trs, 
-				prune (nbrs, nxtVars, choices'),
-				brs)
-			  else
+			    (nclosed := !nclosed + 1;
+			     prv(tacs',  brs0::trs, 
+				 prune (nbrs, nxtVars, choices'),
+				 brs))
+			  else (*prems non-null*)
 			  if lim'<0 (*faster to kill ALL the alternatives*)
 			  then (traceMsg"Excessive branching: KILLED\n";
 			        clearTo ntrl;  raise NEWBRANCHES)
 			  else
-			    prv(tacs',  brs0::trs, choices',
-				newBr (vars',lim') prems))
+			    (ntried := !ntried + length prems - 1;
+			     prv(tacs',  brs0::trs, choices',
+				 newBr (vars',lim') prems)))
                          handle PRV => 
 			   if ntrl < ntrl' (*Vars have been updated*)
 			   then
@@ -955,7 +962,8 @@
 				               else ();
 				     prune (nbrs, nxtVars, 
 					    (ntrl, nbrs, PRV) :: choices))
-			    in  prv (tac::tacs, brs0::trs, choices', brs)  
+			    in  nclosed := !nclosed + 1;
+				prv (tac::tacs, brs0::trs, choices', brs)  
 				handle PRV => 
 				    (*reset Vars and try another literal
 				      [this handler is pruned if possible!]*)
@@ -1058,6 +1066,8 @@
 			    clearTo ntrl;  raise NEWBRANCHES)
 		       else 
 			 traceNew prems;  traceVars sign ntrl;
+			 if null prems then nclosed := !nclosed + 1
+			 else ntried := !ntried + length prems - 1;
 			 prv(tac dup :: tacs, 
 			       (*FIXME: if recur then the tactic should not
 				 call rotate_tac: new formulae should be last*)
@@ -1157,10 +1167,22 @@
   in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
 
 
+fun initialize() = 
+    (fullTrace:=[];  trail := [];  ntrail := 0;
+     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 = 
-    (fullTrace:=[];  trail := [];  ntrail := 0;
+    (initialize();
      let val {sign,...} = rep_thm st
 	 val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
          val hyps  = strip_imp_prems skoprem
@@ -1171,7 +1193,8 @@
 				    Int.toString lim);
 			   backtrack choices)
 		| cell => Seq.make(fn()=> cell))
-     in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
+     in #1 (prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont),
+	    printStats (!trace))
      end
      handle PROVE     => Seq.empty);
 
@@ -1186,14 +1209,15 @@
 
 (*Translate subgoal i from a proof state*)
 fun trygl cs lim i = 
-    (fullTrace:=[];  trail := [];  ntrail := 0;
+    (initialize();
      let val st = topthm()
          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
-     in timeap prove
-	 (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I)
+     in #1 (timeap prove
+	    (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I),
+	    printStats true)
      end
      handle Subscript => error("There is no subgoal " ^ Int.toString i));
 
@@ -1204,11 +1228,12 @@
                       term_of |> fromTerm |> rand |> mkGoal;
 
 fun tryInThy thy lim s = 
-    (fullTrace:=[];  trail := [];  ntrail := 0;
-     timeap prove (sign_of thy, 
-		   Data.claset(), 
-		   [initBranch ([readGoal (sign_of thy) s], lim)], 
-		   I));
+    (initialize();
+     #1 (timeap prove (sign_of thy, 
+		       Data.claset(), 
+		       [initBranch ([readGoal (sign_of thy) s], lim)], 
+		       I),
+	    printStats true));
 
 
 end;