src/Pure/search.ML
changeset 38802 a925c0ee42f7
parent 35408 b48ab741683b
child 46492 bf96ed9e55c1
     1.1 --- a/src/Pure/search.ML	Fri Aug 27 15:46:08 2010 +0200
     1.2 +++ b/src/Pure/search.ML	Fri Aug 27 16:29:12 2010 +0200
     1.3 @@ -18,9 +18,8 @@
     1.4    val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic
     1.5    val DEPTH_SOLVE: tactic -> tactic
     1.6    val DEPTH_SOLVE_1: tactic -> tactic
     1.7 -  val iter_deepen_limit: int Unsynchronized.ref
     1.8 -  val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic
     1.9 -  val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic
    1.10 +  val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic
    1.11 +  val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic
    1.12    val trace_DEEPEN: bool Unsynchronized.ref
    1.13    val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic
    1.14    val trace_BEST_FIRST: bool Unsynchronized.ref
    1.15 @@ -117,21 +116,18 @@
    1.16      in  prune_aux (take (qs, []))  end;
    1.17  
    1.18  
    1.19 -(*No known example (on 1-5-2007) needs even thirty*)
    1.20 -val iter_deepen_limit = Unsynchronized.ref 50;
    1.21 -
    1.22  (*Depth-first iterative deepening search for a state that satisfies satp
    1.23    tactic tac0 sets up the initial goal queue, while tac1 searches it.
    1.24    The solution sequence is redundant: the cutoff heuristic makes it impossible
    1.25    to suppress solutions arising from earlier searches, as the accumulated cost
    1.26    (k) can be wrong.*)
    1.27 -fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st =>
    1.28 +fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st =>
    1.29   let val countr = Unsynchronized.ref 0
    1.30       and tf = tracify trace_DEPTH_FIRST (tac1 1)
    1.31       and qs0 = tac0 st
    1.32       (*bnd = depth bound; inc = estimate of increment required next*)
    1.33       fun depth (bnd,inc) [] =
    1.34 -          if bnd > !iter_deepen_limit then
    1.35 +          if bnd > lim then
    1.36               (tracing (string_of_int (!countr) ^
    1.37                         " inferences so far.  Giving up at " ^ string_of_int bnd);
    1.38                NONE)
    1.39 @@ -170,19 +166,19 @@
    1.40                 end
    1.41    in depth (0,5) [] end);
    1.42  
    1.43 -val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac;
    1.44 +fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac;
    1.45  
    1.46  
    1.47  (*Simple iterative deepening tactical.  It merely "deepens" any search tactic
    1.48    using increment "inc" up to limit "lim". *)
    1.49  val trace_DEEPEN = Unsynchronized.ref false;
    1.50  
    1.51 -fun DEEPEN (inc,lim) tacf m i =
    1.52 +fun DEEPEN (inc, lim) tacf m i =
    1.53    let
    1.54      fun dpn m st =
    1.55        st |>
    1.56         (if has_fewer_prems i st then no_tac
    1.57 -        else if m>lim then
    1.58 +        else if m > lim then
    1.59            (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else ();
    1.60              no_tac)
    1.61          else