author  wenzelm 
Sat, 21 Jan 2006 23:02:14 +0100  
changeset 18728  6790126ab5f6 
parent 16179  fa7e70be26b0 
child 18921  f47c46d7d654 
permissions  rwrr 
16179  1 
(* Title: Pure/search.ML 
1588  2 
ID: $Id$ 
3 
Author: Lawrence C Paulson and Norbert Voelker 

4 

16179  5 
Search tacticals. 
1588  6 
*) 
7 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

8 
infix 1 THEN_MAYBE THEN_MAYBE'; 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

9 

1588  10 
signature SEARCH = 
11 
sig 

2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

12 
val DEEPEN : int*int > (int>int>tactic) > int > int > tactic 
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

13 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

14 
val THEN_MAYBE : tactic * tactic > tactic 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

15 
val THEN_MAYBE' : ('a > tactic) * ('a > tactic) > ('a > tactic) 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

16 

1588  17 
val trace_DEPTH_FIRST : bool ref 
18 
val DEPTH_FIRST : (thm > bool) > tactic > tactic 

19 
val DEPTH_SOLVE : tactic > tactic 

20 
val DEPTH_SOLVE_1 : tactic > tactic 

21 
val ITER_DEEPEN : (thm>bool) > (int>tactic) > tactic 

22 
val THEN_ITER_DEEPEN : tactic > (thm>bool) > (int>tactic) > tactic 

23 

24 
val has_fewer_prems : int > thm > bool 

25 
val IF_UNSOLVED : tactic > tactic 

5754  26 
val SOLVE : tactic > tactic 
8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
5956
diff
changeset

27 
val DETERM_UNTIL_SOLVED: tactic > tactic 
1588  28 
val trace_BEST_FIRST : bool ref 
29 
val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 

30 
val THEN_BEST_FIRST : tactic > (thm>bool) * (thm>int) > tactic 

31 
> tactic 

32 
val trace_ASTAR : bool ref 

33 
val ASTAR : (thm > bool) * (int>thm>int) > tactic > tactic 

34 
val THEN_ASTAR : tactic > (thm>bool) * (int>thm>int) > tactic 

35 
> tactic 

36 
val BREADTH_FIRST : (thm > bool) > tactic > tactic 

5693  37 
val QUIET_BREADTH_FIRST : (thm > bool) > tactic > tactic 
1588  38 
end; 
39 

9094  40 

9411  41 
(** Instantiation of heaps for bestfirst search **) 
9094  42 

9411  43 
(*total ordering on theorems, allowing duplicates to be found*) 
44 
structure ThmHeap = 

45 
HeapFun (type elem = int * thm 

46 
val ord = Library.prod_ord Library.int_ord 

47 
(Term.term_ord o Library.pairself (#prop o Thm.rep_thm))); 

9094  48 

49 

1588  50 
structure Search : SEARCH = 
51 
struct 

52 

53 
(**** Depthfirst search ****) 

54 

55 
val trace_DEPTH_FIRST = ref false; 

56 

57 
(*Searches until "satp" reports proof tree as satisfied. 

58 
Suppresses duplicate solutions to minimize search space.*) 

59 
fun DEPTH_FIRST satp tac = 

60 
let val tac = tracify trace_DEPTH_FIRST tac 

15531  61 
fun depth used [] = NONE 
1588  62 
 depth used (q::qs) = 
4270  63 
case Seq.pull q of 
15531  64 
NONE => depth used qs 
65 
 SOME(st,stq) => 

1588  66 
if satp st andalso not (gen_mem eq_thm (st, used)) 
15531  67 
then SOME(st, Seq.make 
1588  68 
(fn()=> depth (st::used) (stq::qs))) 
69 
else depth used (tac st :: stq :: qs) 

4270  70 
in traced_tac (fn st => depth [] ([Seq.single st])) end; 
1588  71 

72 

73 

74 
(*Predicate: Does the rule have fewer than n premises?*) 

75 
fun has_fewer_prems n rule = (nprems_of rule < n); 

76 

77 
(*Apply a tactic if subgoals remain, else do nothing.*) 

78 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

79 

5754  80 
(*Force a tactic to solve its goal completely, otherwise fail *) 
81 
fun SOLVE tac = tac THEN COND (has_fewer_prems 1) all_tac no_tac; 

82 

8149
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
5956
diff
changeset

83 
(*Force repeated application of tactic until goal is solved completely *) 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
5956
diff
changeset

84 
val DETERM_UNTIL_SOLVED = DETERM_UNTIL (has_fewer_prems 1); 
941afb897532
added tacticals DETERM_UNTIL and DETERM_UNTIL_SOLVED
oheimb
parents:
5956
diff
changeset

85 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

86 
(*Execute tac1, but only execute tac2 if there are at least as many subgoals 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

87 
as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
3538  88 
fun (tac1 THEN_MAYBE tac2) st = 
89 
(tac1 THEN COND (has_fewer_prems (nprems_of st)) all_tac tac2) st; 

2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

90 

85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

91 
fun (tac1 THEN_MAYBE' tac2) x = tac1 x THEN_MAYBE tac2 x; 
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

92 

1588  93 
(*Tactical to reduce the number of premises by 1. 
94 
If no subgoals then it must fail! *) 

3538  95 
fun DEPTH_SOLVE_1 tac st = st > 
1588  96 
(case nprems_of st of 
97 
0 => no_tac 

3538  98 
 n => DEPTH_FIRST (has_fewer_prems n) tac); 
1588  99 

100 
(*Uses depthfirst search to solve ALL subgoals*) 

101 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

102 

103 

104 

2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

105 
(**** Iterative deepening with pruning ****) 
1588  106 

107 
fun has_vars (Var _) = true 

108 
 has_vars (Abs (_,_,t)) = has_vars t 

109 
 has_vars (f$t) = has_vars f orelse has_vars t 

110 
 has_vars _ = false; 

111 

112 
(*Counting of primitive inferences is APPROXIMATE, as the step tactic 

113 
may perform >1 inference*) 

114 

115 
(*Pruning of rigid ancestor to prevent backtracking*) 

116 
fun prune (new as (k', np':int, rgd', stq), qs) = 

117 
let fun prune_aux (qs, []) = new::qs 

118 
 prune_aux (qs, (k,np,rgd,q)::rqs) = 

119 
if np'+1 = np andalso rgd then 

120 
(if !trace_DEPTH_FIRST then 

12262  121 
tracing ("Pruning " ^ 
1588  122 
string_of_int (1+length rqs) ^ " levels") 
123 
else (); 

124 
(*Use OLD k: zerocost solution; see Stickel, p 365*) 

125 
(k, np', rgd', stq) :: qs) 

126 
else prune_aux ((k,np,rgd,q)::qs, rqs) 

127 
fun take ([], rqs) = ([], rqs) 

128 
 take (arg as ((k,np,rgd,stq)::qs, rqs)) = 

129 
if np' < np then take (qs, (k,np,rgd,stq)::rqs) 

130 
else arg 

131 
in prune_aux (take (qs, [])) end; 

132 

133 

134 
(*Depthfirst iterative deepening search for a state that satisfies satp 

135 
tactic tac0 sets up the initial goal queue, while tac1 searches it. 

136 
The solution sequence is redundant: the cutoff heuristic makes it impossible 

137 
to suppress solutions arising from earlier searches, as the accumulated cost 

138 
(k) can be wrong.*) 

139 
fun THEN_ITER_DEEPEN tac0 satp tac1 = traced_tac (fn st => 

140 
let val countr = ref 0 

141 
and tf = tracify trace_DEPTH_FIRST (tac1 1) 

142 
and qs0 = tac0 st 

143 
(*bnd = depth bound; inc = estimate of increment required next*) 

144 
fun depth (bnd,inc) [] = 

12262  145 
(tracing (string_of_int (!countr) ^ 
1588  146 
" inferences so far. Searching to depth " ^ 
147 
string_of_int bnd); 

148 
(*larger increments make it run slower for the hard problems*) 

149 
depth (bnd+inc, 10)) [(0, 1, false, qs0)] 

150 
 depth (bnd,inc) ((k,np,rgd,q)::qs) = 

151 
if k>=bnd then depth (bnd,inc) qs 

152 
else 

153 
case (countr := !countr+1; 

154 
if !trace_DEPTH_FIRST then 

12262  155 
tracing (string_of_int np ^ 
1588  156 
implode (map (fn _ => "*") qs)) 
157 
else (); 

4270  158 
Seq.pull q) of 
15531  159 
NONE => depth (bnd,inc) qs 
160 
 SOME(st,stq) => 

1588  161 
if satp st (*solution!*) 
15531  162 
then SOME(st, Seq.make 
1588  163 
(fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs))) 
164 

165 
else 

166 
let val np' = nprems_of st 

167 
(*rgd' calculation assumes tactic operates on subgoal 1*) 

168 
val rgd' = not (has_vars (hd (prems_of st))) 

169 
val k' = k+np'np+1 (*difference in # of subgoals, +1*) 

170 
in if k'+np' >= bnd 

2143  171 
then depth (bnd, Int.min(inc, k'+np'+1bnd)) qs 
1588  172 
else if np' < np (*solved a subgoal; prune rigid ancestors*) 
173 
then depth (bnd,inc) 

174 
(prune ((k', np', rgd', tf st), (k,np,rgd,stq) :: qs)) 

175 
else depth (bnd,inc) ((k', np', rgd', tf st) :: 

176 
(k,np,rgd,stq) :: qs) 

177 
end 

178 
in depth (0,5) [] end); 

179 

180 
val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; 

181 

182 

2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

183 
(*Simple iterative deepening tactical. It merely "deepens" any search tactic 
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

184 
using increment "inc" up to limit "lim". *) 
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

185 
fun DEEPEN (inc,lim) tacf m i = 
14160
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

186 
let fun dpn m st = 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

187 
st > (if has_fewer_prems i st then no_tac 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

188 
else if m>lim then 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

189 
(warning "Search depth limit exceeded: giving up"; 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

190 
no_tac) 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

191 
else (warning ("Search depth = " ^ string_of_int m); 
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

192 
tacf m i ORELSE dpn (m+inc))) 
2869
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

193 
in dpn m end; 
14160
6750ff1dfc32
Change from "tracing" to "warning", as requested by David Aspinall
paulson
parents:
12262
diff
changeset

194 

1588  195 
(*** Bestfirst search ***) 
196 

197 
val trace_BEST_FIRST = ref false; 

198 

199 
(*For creating output sequence*) 

15531  200 
fun some_of_list [] = NONE 
201 
 some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); 

1588  202 

9094  203 
(*Check for and delete duplicate proof states*) 
204 
fun deleteAllMin prf heap = 

9411  205 
if ThmHeap.is_empty heap then heap 
206 
else if eq_thm (prf, #2 (ThmHeap.min heap)) 

207 
then deleteAllMin prf (ThmHeap.delete_min heap) 

9094  208 
else heap; 
1588  209 

210 
(*Bestfirst search for a state that satisfies satp (incl initial state) 

211 
Function sizef estimates size of problem remaining (smaller means better). 

212 
tactic tac0 sets up the initial priority queue, while tac1 searches it. *) 

213 
fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 

214 
let val tac = tracify trace_BEST_FIRST tac1 

215 
fun pairsize th = (sizef th, th); 

9094  216 
fun bfs (news,nprf_heap) = 
15570  217 
(case List.partition satp news of 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

218 
([],nonsats) => next(foldr ThmHeap.insert 
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

219 
nprf_heap (map pairsize nonsats)) 
1588  220 
 (sats,_) => some_of_list sats) 
9094  221 
and next nprf_heap = 
15531  222 
if ThmHeap.is_empty nprf_heap then NONE 
9094  223 
else 
9411  224 
let val (n,prf) = ThmHeap.min nprf_heap 
9094  225 
in if !trace_BEST_FIRST 
12262  226 
then tracing("state size = " ^ string_of_int n) 
1588  227 
else (); 
9094  228 
bfs (Seq.list_of (tac prf), 
9411  229 
deleteAllMin prf (ThmHeap.delete_min nprf_heap)) 
9094  230 
end 
9411  231 
fun btac st = bfs (Seq.list_of (tac0 st), ThmHeap.empty) 
1588  232 
in traced_tac btac end; 
233 

234 
(*Ordinary bestfirst search, with no initial tactic*) 

235 
val BEST_FIRST = THEN_BEST_FIRST all_tac; 

236 

237 
(*Breadthfirst search to satisfy satpred (including initial state) 

238 
SLOW  SHOULD NOT USE APPEND!*) 

5693  239 
fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
4270  240 
let val tacf = Seq.list_of o tac; 
1588  241 
fun bfs prfs = 
15570  242 
(case List.partition satpred prfs of 
1588  243 
([],[]) => [] 
244 
 ([],nonsats) => 

5956  245 
(message("breadth=" ^ string_of_int(length nonsats)); 
2672
85d7e800d754
Replaced "flat" by the Basis Library function List.concat
paulson
parents:
2143
diff
changeset

246 
bfs (List.concat (map tacf nonsats))) 
1588  247 
 (sats,_) => sats) 
4270  248 
in (fn st => Seq.of_list (bfs [st])) end; 
1588  249 

12262  250 
val BREADTH_FIRST = gen_BREADTH_FIRST tracing; 
5693  251 
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); 
252 

1588  253 

254 
(* Author: Norbert Voelker, FernUniversitaet Hagen 

255 
Remarks: Implementation of A*like proof procedure by modification 

256 
of the existing code for BEST_FIRST and best_tac so that the 

257 
current level of search is taken into account. 

258 
*) 

259 

260 
(*Insertion into priority queue of states, marked with level *) 

261 
fun insert_with_level (lnth: int*int*thm, []) = [lnth] 

262 
 insert_with_level ((l,m,th), (l',n,th')::nths) = 

263 
if n<m then (l',n,th') :: insert_with_level ((l,m,th), nths) 

264 
else if n=m andalso eq_thm(th,th') 

265 
then (l',n,th')::nths 

266 
else (l,m,th)::(l',n,th')::nths; 

267 

268 
(*For creating output sequence*) 

15531  269 
fun some_of_list [] = NONE 
270 
 some_of_list (x::l) = SOME (x, Seq.make (fn () => some_of_list l)); 

1588  271 

272 
val trace_ASTAR = ref false; 

273 

274 
fun THEN_ASTAR tac0 (satp, costf) tac1 = 

275 
let val tf = tracify trace_ASTAR tac1; 

276 
fun bfs (news,nprfs,level) = 

277 
let fun cost thm = (level, costf level thm, thm) 

15570  278 
in (case List.partition satp news of 
1588  279 
([],nonsats) 
15574
b1d1b5bfc464
Removed practically all references to Library.foldr.
skalberg
parents:
15570
diff
changeset

280 
=> next (foldr insert_with_level nprfs (map cost nonsats)) 
1588  281 
 (sats,_) => some_of_list sats) 
282 
end and 

15531  283 
next [] = NONE 
1588  284 
 next ((level,n,prf)::nprfs) = 
285 
(if !trace_ASTAR 

12262  286 
then tracing("level = " ^ string_of_int level ^ 
1588  287 
" cost = " ^ string_of_int n ^ 
288 
" queue length =" ^ string_of_int (length nprfs)) 

289 
else (); 

4270  290 
bfs (Seq.list_of (tf prf), nprfs,level+1)) 
291 
fun tf st = bfs (Seq.list_of (tac0 st), [], 0) 

1588  292 
in traced_tac tf end; 
293 

294 
(*Ordinary ASTAR, with no initial tactic*) 

295 
val ASTAR = THEN_ASTAR all_tac; 

296 

297 
end; 

298 

299 
open Search; 