author  wenzelm 
Tue, 20 Oct 1998 16:33:47 +0200  
changeset 5693  998af7667fa3 
parent 4270  957c887b89b5 
child 5754  98744e38ded1 
permissions  rwrr 
1588  1 
(* Title: search 
2 
ID: $Id$ 

3 
Author: Lawrence C Paulson and Norbert Voelker 

4 

5 
Search tacticals 

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 

26 
val trace_BEST_FIRST : bool ref 

27 
val BEST_FIRST : (thm > bool) * (thm > int) > tactic > tactic 

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

29 
> tactic 

30 
val trace_ASTAR : bool ref 

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

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

33 
> tactic 

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

5693  35 
val QUIET_BREADTH_FIRST : (thm > bool) > tactic > tactic 
1588  36 
end; 
37 

38 
structure Search : SEARCH = 

39 
struct 

40 

41 
(**** Depthfirst search ****) 

42 

43 
val trace_DEPTH_FIRST = ref false; 

44 

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

46 
Suppresses duplicate solutions to minimize search space.*) 

47 
fun DEPTH_FIRST satp tac = 

48 
let val tac = tracify trace_DEPTH_FIRST tac 

49 
fun depth used [] = None 

50 
 depth used (q::qs) = 

4270  51 
case Seq.pull q of 
1588  52 
None => depth used qs 
53 
 Some(st,stq) => 

54 
if satp st andalso not (gen_mem eq_thm (st, used)) 

4270  55 
then Some(st, Seq.make 
1588  56 
(fn()=> depth (st::used) (stq::qs))) 
57 
else depth used (tac st :: stq :: qs) 

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

60 

61 

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

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

64 

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

66 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

67 

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

68 
(*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

69 
as before. This ensures that tac2 is only applied to an outcome of tac1.*) 
3538  70 
fun (tac1 THEN_MAYBE tac2) st = 
71 
(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

72 

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

73 
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

74 

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

3538  77 
fun DEPTH_SOLVE_1 tac st = st > 
1588  78 
(case nprems_of st of 
79 
0 => no_tac 

3538  80 
 n => DEPTH_FIRST (has_fewer_prems n) tac); 
1588  81 

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

83 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

84 

85 

86 

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

87 
(**** Iterative deepening with pruning ****) 
1588  88 

89 
fun has_vars (Var _) = true 

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

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

92 
 has_vars _ = false; 

93 

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

95 
may perform >1 inference*) 

96 

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

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

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

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

101 
if np'+1 = np andalso rgd then 

102 
(if !trace_DEPTH_FIRST then 

103 
writeln ("Pruning " ^ 

104 
string_of_int (1+length rqs) ^ " levels") 

105 
else (); 

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

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

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

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

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

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

112 
else arg 

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

114 

115 

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

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

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

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

120 
(k) can be wrong.*) 

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

122 
let val countr = ref 0 

123 
and tf = tracify trace_DEPTH_FIRST (tac1 1) 

124 
and qs0 = tac0 st 

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

126 
fun depth (bnd,inc) [] = 

127 
(writeln (string_of_int (!countr) ^ 

128 
" inferences so far. Searching to depth " ^ 

129 
string_of_int bnd); 

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

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

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

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

134 
else 

135 
case (countr := !countr+1; 

136 
if !trace_DEPTH_FIRST then 

137 
writeln (string_of_int np ^ 

138 
implode (map (fn _ => "*") qs)) 

139 
else (); 

4270  140 
Seq.pull q) of 
1588  141 
None => depth (bnd,inc) qs 
142 
 Some(st,stq) => 

143 
if satp st (*solution!*) 

4270  144 
then Some(st, Seq.make 
1588  145 
(fn()=> depth (bnd,inc) ((k,np,rgd,stq)::qs))) 
146 

147 
else 

148 
let val np' = nprems_of st 

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

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

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

152 
in if k'+np' >= bnd 

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

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

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

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

159 
end 

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

161 

162 
val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; 

163 

164 

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

165 
(*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

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

167 
fun DEEPEN (inc,lim) tacf m i = 
3538  168 
let fun dpn m st = st > (if has_fewer_prems i st then no_tac 
169 
else if m>lim then 

170 
(writeln "Giving up..."; no_tac) 

171 
else (writeln ("Depth = " ^ string_of_int m); 

172 
tacf m i ORELSE dpn (m+inc))) 

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

173 
in dpn m end; 
acee08856cc9
DEEPEN now takes an upper bound for terminating searches
paulson
parents:
2672
diff
changeset

174 

1588  175 
(*** Bestfirst search ***) 
176 

177 
val trace_BEST_FIRST = ref false; 

178 

179 
(*Insertion into priority queue of states *) 

180 
fun insert (nth: int*thm, []) = [nth] 

181 
 insert ((m,th), (n,th')::nths) = 

182 
if n<m then (n,th') :: insert ((m,th), nths) 

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

184 
then (n,th')::nths 

185 
else (m,th)::(n,th')::nths; 

186 

187 
(*For creating output sequence*) 

188 
fun some_of_list [] = None 

4270  189 
 some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l)); 
1588  190 

191 

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

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

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

195 
fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 

196 
let val tac = tracify trace_BEST_FIRST tac1 

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

198 
fun bfs (news,nprfs) = 

199 
(case partition satp news of 

200 
([],nonsats) => next(foldr insert 

201 
(map pairsize nonsats, nprfs)) 

202 
 (sats,_) => some_of_list sats) 

203 
and next [] = None 

204 
 next ((n,prf)::nprfs) = 

205 
(if !trace_BEST_FIRST 

206 
then writeln("state size = " ^ string_of_int n ^ 

207 
" queue length =" ^ string_of_int (length nprfs)) 

208 
else (); 

4270  209 
bfs (Seq.list_of (tac prf), nprfs)) 
210 
fun btac st = bfs (Seq.list_of (tac0 st), []) 

1588  211 
in traced_tac btac end; 
212 

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

214 
val BEST_FIRST = THEN_BEST_FIRST all_tac; 

215 

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

217 
SLOW  SHOULD NOT USE APPEND!*) 

5693  218 
fun gen_BREADTH_FIRST message satpred (tac:tactic) = 
4270  219 
let val tacf = Seq.list_of o tac; 
1588  220 
fun bfs prfs = 
221 
(case partition satpred prfs of 

222 
([],[]) => [] 

223 
 ([],nonsats) => 

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

225 
bfs (List.concat (map tacf nonsats))) 
1588  226 
 (sats,_) => sats) 
4270  227 
in (fn st => Seq.of_list (bfs [st])) end; 
1588  228 

5693  229 
val BREADTH_FIRST = gen_BREADTH_FIRST prs; 
230 
val QUIET_BREADTH_FIRST = gen_BREADTH_FIRST (K ()); 

231 

1588  232 

233 
(* Author: Norbert Voelker, FernUniversitaet Hagen 

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

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

236 
current level of search is taken into account. 

237 
*) 

238 

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

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

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

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

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

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

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

246 

247 
(*For creating output sequence*) 

248 
fun some_of_list [] = None 

4270  249 
 some_of_list (x::l) = Some (x, Seq.make (fn () => some_of_list l)); 
1588  250 

251 
val trace_ASTAR = ref false; 

252 

253 
fun THEN_ASTAR tac0 (satp, costf) tac1 = 

254 
let val tf = tracify trace_ASTAR tac1; 

255 
fun bfs (news,nprfs,level) = 

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

257 
in (case partition satp news of 

258 
([],nonsats) 

259 
=> next (foldr insert_with_level (map cost nonsats, nprfs)) 

260 
 (sats,_) => some_of_list sats) 

261 
end and 

262 
next [] = None 

263 
 next ((level,n,prf)::nprfs) = 

264 
(if !trace_ASTAR 

265 
then writeln("level = " ^ string_of_int level ^ 

266 
" cost = " ^ string_of_int n ^ 

267 
" queue length =" ^ string_of_int (length nprfs)) 

268 
else (); 

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

1588  271 
in traced_tac tf end; 
272 

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

274 
val ASTAR = THEN_ASTAR all_tac; 

275 

276 
end; 

277 

278 
open Search; 