112 |
112 |
113 (*Counting of primitive inferences is APPROXIMATE, as the step tactic |
113 (*Counting of primitive inferences is APPROXIMATE, as the step tactic |
114 may perform >1 inference*) |
114 may perform >1 inference*) |
115 |
115 |
116 (*Pruning of rigid ancestor to prevent backtracking*) |
116 (*Pruning of rigid ancestor to prevent backtracking*) |
117 fun prune (new as (k', np':int, rgd', stq), qs) = |
117 fun prune (new as (k', np':int, rgd', stq), qs) = |
118 let fun prune_aux (qs, []) = new::qs |
118 let fun prune_aux (qs, []) = new::qs |
119 | prune_aux (qs, (k,np,rgd,q)::rqs) = |
119 | prune_aux (qs, (k,np,rgd,q)::rqs) = |
120 if np'+1 = np andalso rgd then |
120 if np'+1 = np andalso rgd then |
121 (if !trace_DEPTH_FIRST then |
121 (if !trace_DEPTH_FIRST then |
122 tracing ("Pruning " ^ |
122 tracing ("Pruning " ^ |
123 string_of_int (1+length rqs) ^ " levels") |
123 string_of_int (1+length rqs) ^ " levels") |
124 else (); |
124 else (); |
125 (*Use OLD k: zero-cost solution; see Stickel, p 365*) |
125 (*Use OLD k: zero-cost solution; see Stickel, p 365*) |
126 (k, np', rgd', stq) :: qs) |
126 (k, np', rgd', stq) :: qs) |
127 else prune_aux ((k,np,rgd,q)::qs, rqs) |
127 else prune_aux ((k,np,rgd,q)::qs, rqs) |
128 fun take ([], rqs) = ([], rqs) |
128 fun take ([], rqs) = ([], rqs) |
129 | take (arg as ((k,np,rgd,stq)::qs, rqs)) = |
129 | take (arg as ((k,np,rgd,stq)::qs, rqs)) = |
130 if np' < np then take (qs, (k,np,rgd,stq)::rqs) |
130 if np' < np then take (qs, (k,np,rgd,stq)::rqs) |
131 else arg |
131 else arg |
132 in prune_aux (take (qs, [])) end; |
132 in prune_aux (take (qs, [])) end; |
133 |
133 |
134 |
134 |
135 (*No known example (on 1-5-2007) needs even thirty*) |
135 (*No known example (on 1-5-2007) needs even thirty*) |
136 val iter_deepen_limit = ref 50; |
136 val iter_deepen_limit = ref 50; |
138 (*Depth-first iterative deepening search for a state that satisfies satp |
138 (*Depth-first iterative deepening search for a state that satisfies satp |
139 tactic tac0 sets up the initial goal queue, while tac1 searches it. |
139 tactic tac0 sets up the initial goal queue, while tac1 searches it. |
140 The solution sequence is redundant: the cutoff heuristic makes it impossible |
140 The solution sequence is redundant: the cutoff heuristic makes it impossible |
141 to suppress solutions arising from earlier searches, as the accumulated cost |
141 to suppress solutions arising from earlier searches, as the accumulated cost |
142 (k) can be wrong.*) |
142 (k) can be wrong.*) |
143 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => |
143 fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => |
144 let val countr = ref 0 |
144 let val countr = ref 0 |
145 and tf = tracify trace_DEPTH_FIRST (tac1 1) |
145 and tf = tracify trace_DEPTH_FIRST (tac1 1) |
146 and qs0 = tac0 st |
146 and qs0 = tac0 st |
147 (*bnd = depth bound; inc = estimate of increment required next*) |
147 (*bnd = depth bound; inc = estimate of increment required next*) |
148 fun depth (bnd,inc) [] = |
148 fun depth (bnd,inc) [] = |
149 if bnd > !iter_deepen_limit then |
149 if bnd > !iter_deepen_limit then |
150 (tracing (string_of_int (!countr) ^ |
150 (tracing (string_of_int (!countr) ^ |
151 " inferences so far. Giving up at " ^ string_of_int bnd); |
151 " inferences so far. Giving up at " ^ string_of_int bnd); |
152 NONE) |
152 NONE) |
153 else |
153 else |
154 (tracing (string_of_int (!countr) ^ |
154 (tracing (string_of_int (!countr) ^ |
155 " inferences so far. Searching to depth " ^ |
155 " inferences so far. Searching to depth " ^ |
156 string_of_int bnd); |
156 string_of_int bnd); |
157 (*larger increments make it run slower for the hard problems*) |
157 (*larger increments make it run slower for the hard problems*) |
158 depth (bnd+inc, 10)) [(0, 1, false, qs0)] |
158 depth (bnd+inc, 10)) [(0, 1, false, qs0)] |
159 | depth (bnd,inc) ((k,np,rgd,q)::qs) = |
159 | depth (bnd,inc) ((k,np,rgd,q)::qs) = |
160 if k>=bnd then depth (bnd,inc) qs |
160 if k>=bnd then depth (bnd,inc) qs |
161 else |
161 else |
162 case (countr := !countr+1; |
162 case (countr := !countr+1; |
163 if !trace_DEPTH_FIRST then |
163 if !trace_DEPTH_FIRST then |
164 tracing (string_of_int np ^ implode (map (fn _ => "*") qs)) |
164 tracing (string_of_int np ^ implode (map (fn _ => "*") qs)) |
165 else (); |
165 else (); |
166 Seq.pull q) of |
166 Seq.pull q) of |
167 NONE => depth (bnd,inc) qs |
167 NONE => depth (bnd,inc) qs |
168 | SOME(st,stq) => |
168 | SOME(st,stq) => |
169 if satp st (*solution!*) |
169 if satp st (*solution!*) |
170 then SOME(st, Seq.make |
170 then SOME(st, Seq.make |
171 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs))) |
171 (fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs))) |
172 |
172 |
173 else |
173 else |
174 let val np' = nprems_of st |
174 let val np' = nprems_of st |
175 (*rgd' calculation assumes tactic operates on subgoal 1*) |
175 (*rgd' calculation assumes tactic operates on subgoal 1*) |
176 val rgd' = not (has_vars (hd (prems_of st))) |
176 val rgd' = not (has_vars (hd (prems_of st))) |
177 val k' = k+np'-np+1 (*difference in # of subgoals, +1*) |
177 val k' = k+np'-np+1 (*difference in # of subgoals, +1*) |
178 in if k'+np' >= bnd |
178 in if k'+np' >= bnd |
179 then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs |
179 then depth (bnd, Int.min(inc, k'+np'+1-bnd)) qs |
180 else if np' < np (*solved a subgoal; prune rigid ancestors*) |
180 else if np' < np (*solved a subgoal; prune rigid ancestors*) |
181 then depth (bnd,inc) |
181 then depth (bnd,inc) |
182 (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs)) |
182 (prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs)) |
183 else depth (bnd,inc) ((k', np', rgd', tf st) :: |
183 else depth (bnd,inc) ((k', np', rgd', tf st) :: |
184 (k,np,rgd,stq) :: qs) |
184 (k,np,rgd,stq) :: qs) |
185 end |
185 end |
186 in depth (0,5) [] end); |
186 in depth (0,5) [] end); |
187 |
187 |
188 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; |
188 val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; |
189 |
189 |
190 |
190 |
191 (*Simple iterative deepening tactical. It merely "deepens" any search tactic |
191 (*Simple iterative deepening tactical. It merely "deepens" any search tactic |
192 using increment "inc" up to limit "lim". *) |
192 using increment "inc" up to limit "lim". *) |
193 fun DEEPEN (inc,lim) tacf m i = |
193 fun DEEPEN (inc,lim) tacf m i = |
194 let fun dpn m st = |
194 let fun dpn m st = |
195 st |> (if has_fewer_prems i st then no_tac |
195 st |> (if has_fewer_prems i st then no_tac |
196 else if m>lim then |
196 else if m>lim then |
197 (warning "Search depth limit exceeded: giving up"; |
197 (warning "Search depth limit exceeded: giving up"; |
198 no_tac) |
198 no_tac) |
199 else (warning ("Search depth = " ^ string_of_int m); |
199 else (warning ("Search depth = " ^ string_of_int m); |
200 tacf m i ORELSE dpn (m+inc))) |
200 tacf m i ORELSE dpn (m+inc))) |
201 in dpn m end; |
201 in dpn m end; |
202 |
202 |
203 (*** Best-first search ***) |
203 (*** Best-first search ***) |
204 |
204 |
205 val trace_BEST_FIRST = ref false; |
205 val trace_BEST_FIRST = ref false; |
206 |
206 |
207 (*For creating output sequence*) |
207 (*For creating output sequence*) |
208 fun some_of_list [] = NONE |
208 fun some_of_list [] = NONE |
209 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); |
209 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); |
210 |
210 |
211 (*Check for and delete duplicate proof states*) |
211 (*Check for and delete duplicate proof states*) |
212 fun deleteAllMin prf heap = |
212 fun deleteAllMin prf heap = |
213 if ThmHeap.is_empty heap then heap |
213 if ThmHeap.is_empty heap then heap |
214 else if Thm.eq_thm (prf, #2 (ThmHeap.min heap)) |
214 else if Thm.eq_thm (prf, #2 (ThmHeap.min heap)) |
215 then deleteAllMin prf (ThmHeap.delete_min heap) |
215 then deleteAllMin prf (ThmHeap.delete_min heap) |
216 else heap; |
216 else heap; |
217 |
217 |
218 (*Best-first search for a state that satisfies satp (incl initial state) |
218 (*Best-first search for a state that satisfies satp (incl initial state) |
219 Function sizef estimates size of problem remaining (smaller means better). |
219 Function sizef estimates size of problem remaining (smaller means better). |
220 tactic tac0 sets up the initial priority queue, while tac1 searches it. *) |
220 tactic tac0 sets up the initial priority queue, while tac1 searches it. *) |
221 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = |
221 fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = |
222 let val tac = tracify trace_BEST_FIRST tac1 |
222 let val tac = tracify trace_BEST_FIRST tac1 |
223 fun pairsize th = (sizef th, th); |
223 fun pairsize th = (sizef th, th); |
224 fun bfs (news,nprf_heap) = |
224 fun bfs (news,nprf_heap) = |
225 (case List.partition satp news of |
225 (case List.partition satp news of |
226 ([],nonsats) => next(foldr ThmHeap.insert |
226 ([],nonsats) => next(fold_rev ThmHeap.insert (map pairsize nonsats) nprf_heap) |
227 nprf_heap (map pairsize nonsats)) |
227 | (sats,_) => some_of_list sats) |
228 | (sats,_) => some_of_list sats) |
|
229 and next nprf_heap = |
228 and next nprf_heap = |
230 if ThmHeap.is_empty nprf_heap then NONE |
229 if ThmHeap.is_empty nprf_heap then NONE |
231 else |
230 else |
232 let val (n,prf) = ThmHeap.min nprf_heap |
231 let val (n,prf) = ThmHeap.min nprf_heap |
233 in if !trace_BEST_FIRST |
232 in if !trace_BEST_FIRST |
234 then tracing("state size = " ^ string_of_int n) |
233 then tracing("state size = " ^ string_of_int n) |
235 else (); |
234 else (); |
236 bfs (Seq.list_of (tac prf), |
235 bfs (Seq.list_of (tac prf), |
237 deleteAllMin prf (ThmHeap.delete_min nprf_heap)) |
236 deleteAllMin prf (ThmHeap.delete_min nprf_heap)) |
238 end |
237 end |
239 fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty) |
238 fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty) |
240 in traced_tac btac end; |
239 in traced_tac btac end; |
241 |
240 |
242 (*Ordinary best-first search, with no initial tactic*) |
241 (*Ordinary best-first search, with no initial tactic*) |
243 val BEST_FIRST = THEN_BEST_FIRST all_tac; |
242 val BEST_FIRST = THEN_BEST_FIRST all_tac; |
244 |
243 |
245 (*Breadth-first search to satisfy satpred (including initial state) |
244 (*Breadth-first search to satisfy satpred (including initial state) |
246 SLOW -- SHOULD NOT USE APPEND!*) |
245 SLOW -- SHOULD NOT USE APPEND!*) |
247 fun gen_BREADTH_FIRST message satpred (tac:tactic) = |
246 fun gen_BREADTH_FIRST message satpred (tac:tactic) = |
248 let val tacf = Seq.list_of o tac; |
247 let val tacf = Seq.list_of o tac; |
249 fun bfs prfs = |
248 fun bfs prfs = |
250 (case List.partition satpred prfs of |
249 (case List.partition satpred prfs of |
251 ([],[]) => [] |
250 ([],[]) => [] |
252 | ([],nonsats) => |
251 | ([],nonsats) => |
253 (message("breadth=" ^ string_of_int(length nonsats)); |
252 (message("breadth=" ^ string_of_int(length nonsats)); |
254 bfs (maps tacf nonsats)) |
253 bfs (maps tacf nonsats)) |
255 | (sats,_) => sats) |
254 | (sats,_) => sats) |
256 in (fn st => Seq.of_list (bfs [st])) end; |
255 in (fn st => Seq.of_list (bfs [st])) end; |
257 |
256 |
258 val BREADTH_FIRST = gen_BREADTH_FIRST tracing; |
257 val BREADTH_FIRST = gen_BREADTH_FIRST tracing; |
259 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); |
258 val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); |
260 |
259 |
261 |
260 |
262 (* Author: Norbert Voelker, FernUniversitaet Hagen |
261 (* Author: Norbert Voelker, FernUniversitaet Hagen |
263 Remarks: Implementation of A*-like proof procedure by modification |
262 Remarks: Implementation of A*-like proof procedure by modification |
264 of the existing code for BEST_FIRST and best_tac so that the |
263 of the existing code for BEST_FIRST and best_tac so that the |
265 current level of search is taken into account. |
264 current level of search is taken into account. |
266 *) |
265 *) |
267 |
266 |
268 (*Insertion into priority queue of states, marked with level *) |
267 (*Insertion into priority queue of states, marked with level *) |
269 fun insert_with_level (lnth: int*int*thm, []) = [lnth] |
268 fun insert_with_level (lnth: int*int*thm, []) = [lnth] |
270 | insert_with_level ((l,m,th), (l',n,th')::nths) = |
269 | insert_with_level ((l,m,th), (l',n,th')::nths) = |
271 if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths) |
270 if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths) |
272 else if n=m andalso Thm.eq_thm(th,th') |
271 else if n=m andalso Thm.eq_thm(th,th') |
273 then (l',n,th')::nths |
272 then (l',n,th')::nths |
274 else (l,m,th)::(l',n,th')::nths; |
273 else (l,m,th)::(l',n,th')::nths; |
275 |
274 |
276 (*For creating output sequence*) |
275 (*For creating output sequence*) |
277 fun some_of_list [] = NONE |
276 fun some_of_list [] = NONE |
278 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); |
277 | some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); |
279 |
278 |
280 val trace_ASTAR = ref false; |
279 val trace_ASTAR = ref false; |
281 |
280 |
282 fun THEN_ASTAR tac0 (satp, costf) tac1 = |
281 fun THEN_ASTAR tac0 (satp, costf) tac1 = |
283 let val tf = tracify trace_ASTAR tac1; |
282 let val tf = tracify trace_ASTAR tac1; |
284 fun bfs (news,nprfs,level) = |
283 fun bfs (news,nprfs,level) = |
285 let fun cost thm = (level, costf level thm, thm) |
284 let fun cost thm = (level, costf level thm, thm) |
286 in (case List.partition satp news of |
285 in (case List.partition satp news of |
287 ([],nonsats) |
286 ([],nonsats) |
288 => next (foldr insert_with_level nprfs (map cost nonsats)) |
287 => next (List.foldr insert_with_level nprfs (map cost nonsats)) |
289 | (sats,_) => some_of_list sats) |
288 | (sats,_) => some_of_list sats) |
290 end and |
289 end and |
291 next [] = NONE |
290 next [] = NONE |
292 | next ((level,n,prf)::nprfs) = |
291 | next ((level,n,prf)::nprfs) = |
293 (if !trace_ASTAR |
292 (if !trace_ASTAR |
294 then tracing("level = " ^ string_of_int level ^ |
293 then tracing("level = " ^ string_of_int level ^ |
295 " cost = " ^ string_of_int n ^ |
294 " cost = " ^ string_of_int n ^ |
296 " queue length =" ^ string_of_int (length nprfs)) |
295 " queue length =" ^ string_of_int (length nprfs)) |
297 else (); |
296 else (); |
298 bfs (Seq.list_of (tf prf), nprfs,level+1)) |
297 bfs (Seq.list_of (tf prf), nprfs,level+1)) |
299 fun tf st = bfs (Seq.list_of (tac0 st), [], 0) |
298 fun tf st = bfs (Seq.list_of (tac0 st), [], 0) |
300 in traced_tac tf end; |
299 in traced_tac tf end; |
301 |
300 |