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`