16 val DETERM_UNTIL_SOLVED: tactic -> tactic |
16 val DETERM_UNTIL_SOLVED: tactic -> tactic |
17 val THEN_MAYBE: tactic * tactic -> tactic |
17 val THEN_MAYBE: tactic * tactic -> tactic |
18 val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
18 val THEN_MAYBE': ('a -> tactic) * ('a -> tactic) -> 'a -> tactic |
19 val DEPTH_SOLVE: tactic -> tactic |
19 val DEPTH_SOLVE: tactic -> tactic |
20 val DEPTH_SOLVE_1: tactic -> tactic |
20 val DEPTH_SOLVE_1: tactic -> tactic |
21 val iter_deepen_limit: int Unsynchronized.ref |
21 val THEN_ITER_DEEPEN: int -> tactic -> (thm -> bool) -> (int -> tactic) -> tactic |
22 val THEN_ITER_DEEPEN: tactic -> (thm -> bool) -> (int -> tactic) -> tactic |
22 val ITER_DEEPEN: int -> (thm -> bool) -> (int -> tactic) -> tactic |
23 val ITER_DEEPEN: (thm -> bool) -> (int -> tactic) -> tactic |
|
24 val trace_DEEPEN: bool Unsynchronized.ref |
23 val trace_DEEPEN: bool Unsynchronized.ref |
25 val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic |
24 val DEEPEN: int * int -> (int -> int -> tactic) -> int -> int -> tactic |
26 val trace_BEST_FIRST: bool Unsynchronized.ref |
25 val trace_BEST_FIRST: bool Unsynchronized.ref |
27 val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic |
26 val THEN_BEST_FIRST: tactic -> (thm -> bool) * (thm -> int) -> tactic -> tactic |
28 val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic |
27 val BEST_FIRST: (thm -> bool) * (thm -> int) -> tactic -> tactic |
115 if np' < np then take (qs, (k,np,rgd,stq)::rqs) |
114 if np' < np then take (qs, (k,np,rgd,stq)::rqs) |
116 else arg |
115 else arg |
117 in prune_aux (take (qs, [])) end; |
116 in prune_aux (take (qs, [])) end; |
118 |
117 |
119 |
118 |
120 (*No known example (on 1-5-2007) needs even thirty*) |
|
121 val iter_deepen_limit = Unsynchronized.ref 50; |
|
122 |
|
123 (*Depth-first iterative deepening search for a state that satisfies satp |
119 (*Depth-first iterative deepening search for a state that satisfies satp |
124 tactic tac0 sets up the initial goal queue, while tac1 searches it. |
120 tactic tac0 sets up the initial goal queue, while tac1 searches it. |
125 The solution sequence is redundant: the cutoff heuristic makes it impossible |
121 The solution sequence is redundant: the cutoff heuristic makes it impossible |
126 to suppress solutions arising from earlier searches, as the accumulated cost |
122 to suppress solutions arising from earlier searches, as the accumulated cost |
127 (k) can be wrong.*) |
123 (k) can be wrong.*) |
128 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => |
124 fun THEN_ITER_DEEPEN lim tac0 satp tac1 = traced_tac (fn st => |
129 let val countr = Unsynchronized.ref 0 |
125 let val countr = Unsynchronized.ref 0 |
130 and tf = tracify trace_DEPTH_FIRST (tac1 1) |
126 and tf = tracify trace_DEPTH_FIRST (tac1 1) |
131 and qs0 = tac0 st |
127 and qs0 = tac0 st |
132 (*bnd = depth bound; inc = estimate of increment required next*) |
128 (*bnd = depth bound; inc = estimate of increment required next*) |
133 fun depth (bnd,inc) [] = |
129 fun depth (bnd,inc) [] = |
134 if bnd > !iter_deepen_limit then |
130 if bnd > lim then |
135 (tracing (string_of_int (!countr) ^ |
131 (tracing (string_of_int (!countr) ^ |
136 " inferences so far. Giving up at " ^ string_of_int bnd); |
132 " inferences so far. Giving up at " ^ string_of_int bnd); |
137 NONE) |
133 NONE) |
138 else |
134 else |
139 (tracing (string_of_int (!countr) ^ |
135 (tracing (string_of_int (!countr) ^ |
168 else depth (bnd,inc) ((k', np', rgd', tf st) :: |
164 else depth (bnd,inc) ((k', np', rgd', tf st) :: |
169 (k,np,rgd,stq) :: qs) |
165 (k,np,rgd,stq) :: qs) |
170 end |
166 end |
171 in depth (0,5) [] end); |
167 in depth (0,5) [] end); |
172 |
168 |
173 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; |
169 fun ITER_DEEPEN lim = THEN_ITER_DEEPEN lim all_tac; |
174 |
170 |
175 |
171 |
176 (*Simple iterative deepening tactical. It merely "deepens" any search tactic |
172 (*Simple iterative deepening tactical. It merely "deepens" any search tactic |
177 using increment "inc" up to limit "lim". *) |
173 using increment "inc" up to limit "lim". *) |
178 val trace_DEEPEN = Unsynchronized.ref false; |
174 val trace_DEEPEN = Unsynchronized.ref false; |
179 |
175 |
180 fun DEEPEN (inc,lim) tacf m i = |
176 fun DEEPEN (inc, lim) tacf m i = |
181 let |
177 let |
182 fun dpn m st = |
178 fun dpn m st = |
183 st |> |
179 st |> |
184 (if has_fewer_prems i st then no_tac |
180 (if has_fewer_prems i st then no_tac |
185 else if m>lim then |
181 else if m > lim then |
186 (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else (); |
182 (if !trace_DEEPEN then tracing "Search depth limit exceeded: giving up" else (); |
187 no_tac) |
183 no_tac) |
188 else |
184 else |
189 (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else (); |
185 (if !trace_DEEPEN then tracing ("Search depth = " ^ string_of_int m) else (); |
190 tacf m i ORELSE dpn (m+inc))) |
186 tacf m i ORELSE dpn (m+inc))) |