Statistics
authorpaulson
Wed Nov 26 16:49:54 1997 +0100 (1997-11-26 ago)
changeset 4300451ae21dca28
parent 4299 22596d62ce0b
child 4301 ed343192de45
Statistics
src/Provers/blast.ML
     1.1 --- a/src/Provers/blast.ML	Wed Nov 26 16:49:07 1997 +0100
     1.2 +++ b/src/Provers/blast.ML	Wed Nov 26 16:49:54 1997 +0100
     1.3 @@ -874,6 +874,11 @@
     1.4    | match t               u   = false;
     1.5  
     1.6  
     1.7 +(*Branches closed: number of branches closed during the search
     1.8 +  Branches tried:  number of branches created by splitting (counting from 1)*)
     1.9 +val nclosed = ref 0
    1.10 +and ntried  = ref 1;
    1.11 +
    1.12  (*Tableau prover based on leanTaP.  Argument is a list of branches.  Each 
    1.13    branch contains a list of unexpanded formulae, a list of literals, and a 
    1.14    bound on unsafe expansions.*)
    1.15 @@ -923,16 +928,18 @@
    1.16  		     in
    1.17  			 traceNew prems;  traceVars sign ntrl;
    1.18  			 (if null prems then (*closed the branch: prune!*)
    1.19 -			    prv(tacs',  brs0::trs, 
    1.20 -				prune (nbrs, nxtVars, choices'),
    1.21 -				brs)
    1.22 -			  else
    1.23 +			    (nclosed := !nclosed + 1;
    1.24 +			     prv(tacs',  brs0::trs, 
    1.25 +				 prune (nbrs, nxtVars, choices'),
    1.26 +				 brs))
    1.27 +			  else (*prems non-null*)
    1.28  			  if lim'<0 (*faster to kill ALL the alternatives*)
    1.29  			  then (traceMsg"Excessive branching: KILLED\n";
    1.30  			        clearTo ntrl;  raise NEWBRANCHES)
    1.31  			  else
    1.32 -			    prv(tacs',  brs0::trs, choices',
    1.33 -				newBr (vars',lim') prems))
    1.34 +			    (ntried := !ntried + length prems - 1;
    1.35 +			     prv(tacs',  brs0::trs, choices',
    1.36 +				 newBr (vars',lim') prems)))
    1.37                           handle PRV => 
    1.38  			   if ntrl < ntrl' (*Vars have been updated*)
    1.39  			   then
    1.40 @@ -955,7 +962,8 @@
    1.41  				               else ();
    1.42  				     prune (nbrs, nxtVars, 
    1.43  					    (ntrl, nbrs, PRV) :: choices))
    1.44 -			    in  prv (tac::tacs, brs0::trs, choices', brs)  
    1.45 +			    in  nclosed := !nclosed + 1;
    1.46 +				prv (tac::tacs, brs0::trs, choices', brs)  
    1.47  				handle PRV => 
    1.48  				    (*reset Vars and try another literal
    1.49  				      [this handler is pruned if possible!]*)
    1.50 @@ -1058,6 +1066,8 @@
    1.51  			    clearTo ntrl;  raise NEWBRANCHES)
    1.52  		       else 
    1.53  			 traceNew prems;  traceVars sign ntrl;
    1.54 +			 if null prems then nclosed := !nclosed + 1
    1.55 +			 else ntried := !ntried + length prems - 1;
    1.56  			 prv(tac dup :: tacs, 
    1.57  			       (*FIXME: if recur then the tactic should not
    1.58  				 call rotate_tac: new formulae should be last*)
    1.59 @@ -1157,10 +1167,22 @@
    1.60    in  skoSubgoal 0 (from 0 (discard_foralls t))  end;
    1.61  
    1.62  
    1.63 +fun initialize() = 
    1.64 +    (fullTrace:=[];  trail := [];  ntrail := 0;
    1.65 +     nclosed := 0;  ntried := 1);
    1.66 +
    1.67 +
    1.68 +fun printStats b =
    1.69 +  if b then
    1.70 +    (writeln ("Branches closed: " ^ Int.toString (!nclosed));
    1.71 +     writeln ("Branches tried:  " ^ Int.toString (!ntried)))
    1.72 +  else ();
    1.73 +
    1.74 +
    1.75  (*Tactic using tableau engine and proof reconstruction.  
    1.76   "lim" is depth limit.*)
    1.77  fun depth_tac cs lim i st = 
    1.78 -    (fullTrace:=[];  trail := [];  ntrail := 0;
    1.79 +    (initialize();
    1.80       let val {sign,...} = rep_thm st
    1.81  	 val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
    1.82           val hyps  = strip_imp_prems skoprem
    1.83 @@ -1171,7 +1193,8 @@
    1.84  				    Int.toString lim);
    1.85  			   backtrack choices)
    1.86  		| cell => Seq.make(fn()=> cell))
    1.87 -     in prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont)
    1.88 +     in #1 (prove (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], cont),
    1.89 +	    printStats (!trace))
    1.90       end
    1.91       handle PROVE     => Seq.empty);
    1.92  
    1.93 @@ -1186,14 +1209,15 @@
    1.94  
    1.95  (*Translate subgoal i from a proof state*)
    1.96  fun trygl cs lim i = 
    1.97 -    (fullTrace:=[];  trail := [];  ntrail := 0;
    1.98 +    (initialize();
    1.99       let val st = topthm()
   1.100           val {sign,...} = rep_thm st
   1.101  	 val skoprem = fromSubgoal (List.nth(prems_of st, i-1))
   1.102           val hyps  = strip_imp_prems skoprem
   1.103           and concl = strip_imp_concl skoprem
   1.104 -     in timeap prove
   1.105 -	 (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I)
   1.106 +     in #1 (timeap prove
   1.107 +	    (sign, cs, [initBranch (mkGoal concl :: hyps, lim)], I),
   1.108 +	    printStats true)
   1.109       end
   1.110       handle Subscript => error("There is no subgoal " ^ Int.toString i));
   1.111  
   1.112 @@ -1204,11 +1228,12 @@
   1.113                        term_of |> fromTerm |> rand |> mkGoal;
   1.114  
   1.115  fun tryInThy thy lim s = 
   1.116 -    (fullTrace:=[];  trail := [];  ntrail := 0;
   1.117 -     timeap prove (sign_of thy, 
   1.118 -		   Data.claset(), 
   1.119 -		   [initBranch ([readGoal (sign_of thy) s], lim)], 
   1.120 -		   I));
   1.121 +    (initialize();
   1.122 +     #1 (timeap prove (sign_of thy, 
   1.123 +		       Data.claset(), 
   1.124 +		       [initBranch ([readGoal (sign_of thy) s], lim)], 
   1.125 +		       I),
   1.126 +	    printStats true));
   1.127  
   1.128  
   1.129  end;