src/Pure/search.ML
changeset 22025 7c5896919eb8
parent 20852 edc3147ab164
child 22360 26ead7ed4f4b
     1.1 --- a/src/Pure/search.ML	Fri Jan 05 15:33:05 2007 +0100
     1.2 +++ b/src/Pure/search.ML	Fri Jan 05 17:38:05 2007 +0100
     1.3 @@ -20,6 +20,7 @@
     1.4    val DEPTH_SOLVE_1	: tactic -> tactic
     1.5    val ITER_DEEPEN	: (thm->bool) -> (int->tactic) -> tactic
     1.6    val THEN_ITER_DEEPEN	: tactic -> (thm->bool) -> (int->tactic) -> tactic
     1.7 +  val iter_deepen_limit : int ref
     1.8  
     1.9    val has_fewer_prems	: int -> thm -> bool   
    1.10    val IF_UNSOLVED	: tactic -> tactic
    1.11 @@ -131,6 +132,9 @@
    1.12      in  prune_aux (take (qs, []))  end;
    1.13  
    1.14  
    1.15 +(*No known example (on 1-5-2007) needs even thirty*)
    1.16 +val iter_deepen_limit = ref 50;
    1.17 +
    1.18  (*Depth-first iterative deepening search for a state that satisfies satp
    1.19    tactic tac0 sets up the initial goal queue, while tac1 searches it.
    1.20    The solution sequence is redundant: the cutoff heuristic makes it impossible
    1.21 @@ -142,6 +146,11 @@
    1.22       and qs0 = tac0 st
    1.23       (*bnd = depth bound; inc = estimate of increment required next*)
    1.24       fun depth (bnd,inc) [] = 
    1.25 +          if bnd > !iter_deepen_limit then
    1.26 +	     (tracing (string_of_int (!countr) ^ 
    1.27 +		       " inferences so far.  Giving up at " ^ string_of_int bnd);
    1.28 +	      NONE)
    1.29 +          else
    1.30  	     (tracing (string_of_int (!countr) ^ 
    1.31  		       " inferences so far.  Searching to depth " ^ 
    1.32  		       string_of_int bnd);
    1.33 @@ -152,8 +161,7 @@
    1.34            else
    1.35  	  case (countr := !countr+1;
    1.36  		if !trace_DEPTH_FIRST then
    1.37 -		    tracing (string_of_int np ^ 
    1.38 -			     implode (map (fn _ => "*") qs))
    1.39 +		    tracing (string_of_int np ^ implode (map (fn _ => "*") qs))
    1.40  		else ();
    1.41  		Seq.pull q) of
    1.42  	     NONE         => depth (bnd,inc) qs