src/Pure/search.ML
 changeset 62919 9eb0359d6a77 parent 62916 621afc4607ec
equal inserted replaced
62918:2fcbd4abc021 62919:9eb0359d6a77
106   The solution sequence is redundant: the cutoff heuristic makes it impossible
106   The solution sequence is redundant: the cutoff heuristic makes it impossible
107   to suppress solutions arising from earlier searches, as the accumulated cost
107   to suppress solutions arising from earlier searches, as the accumulated cost
108   (k) can be wrong.*)
108   (k) can be wrong.*)
109 fun THEN_ITER_DEEPEN lim tac0 satp tac1 st =
109 fun THEN_ITER_DEEPEN lim tac0 satp tac1 st =
110   let
110   let
111     val countr = Unsynchronized.ref 0
111     val counter = Unsynchronized.ref 0
112     and tf = tac1 1
112     and tf = tac1 1
113     and qs0 = tac0 st
113     and qs0 = tac0 st
114      (*bnd = depth bound; inc = estimate of increment required next*)
114      (*bnd = depth bound; inc = estimate of increment required next*)
115     fun depth (bnd, inc) [] =
115     fun depth (bnd, inc) [] =
116           if bnd > lim then NONE
116           if bnd > lim then NONE
118             (*larger increments make it run slower for the hard problems*)
118             (*larger increments make it run slower for the hard problems*)
119             depth (bnd + inc, 10) [(0, 1, false, qs0)]
119             depth (bnd + inc, 10) [(0, 1, false, qs0)]
120       | depth (bnd, inc) ((k, np, rgd, q) :: qs) =
120       | depth (bnd, inc) ((k, np, rgd, q) :: qs) =
121           if k >= bnd then depth (bnd, inc) qs
121           if k >= bnd then depth (bnd, inc) qs
122           else
122           else
123            (case (Unsynchronized.inc countr; Seq.pull q) of
123            (case (Unsynchronized.inc counter; Seq.pull q) of
124              NONE => depth (bnd, inc) qs
124              NONE => depth (bnd, inc) qs
125            | SOME (st, stq) =>
125            | SOME (st, stq) =>
126               if satp st then (*solution!*)
126               if satp st then (*solution!*)
127                 SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs)))
127                 SOME(st, Seq.make (fn() => depth (bnd, inc) ((k, np, rgd, stq) :: qs)))
128               else
128               else