author  wenzelm 
Fri, 21 Nov 1997 15:27:43 +0100  
changeset 4270  957c887b89b5 
parent 3538  ed9de44032e0 
child 5693  998af7667fa3 
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 

35 
end; 

36 

37 
structure Search : SEARCH = 

38 
struct 

39 

40 
(**** Depthfirst search ****) 

41 

42 
val trace_DEPTH_FIRST = ref false; 

43 

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

45 
Suppresses duplicate solutions to minimize search space.*) 

46 
fun DEPTH_FIRST satp tac = 

47 
let val tac = tracify trace_DEPTH_FIRST tac 

48 
fun depth used [] = None 

49 
 depth used (q::qs) = 

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

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

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

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

59 

60 

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

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

63 

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

65 
val IF_UNSOLVED = COND (has_fewer_prems 1) all_tac; 

66 

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

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

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

71 

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

72 
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

73 

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

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

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

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

82 
val DEPTH_SOLVE = DEPTH_FIRST (has_fewer_prems 1); 

83 

84 

85 

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

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

88 
fun has_vars (Var _) = true 

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

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

91 
 has_vars _ = false; 

92 

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

94 
may perform >1 inference*) 

95 

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

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

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

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

100 
if np'+1 = np andalso rgd then 

101 
(if !trace_DEPTH_FIRST then 

102 
writeln ("Pruning " ^ 

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

104 
else (); 

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

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

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

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

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

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

111 
else arg 

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

113 

114 

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

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

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

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

119 
(k) can be wrong.*) 

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

121 
let val countr = ref 0 

122 
and tf = tracify trace_DEPTH_FIRST (tac1 1) 

123 
and qs0 = tac0 st 

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

125 
fun depth (bnd,inc) [] = 

126 
(writeln (string_of_int (!countr) ^ 

127 
" inferences so far. Searching to depth " ^ 

128 
string_of_int bnd); 

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

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

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

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

133 
else 

134 
case (countr := !countr+1; 

135 
if !trace_DEPTH_FIRST then 

136 
writeln (string_of_int np ^ 

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

138 
else (); 

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

142 
if satp st (*solution!*) 

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

146 
else 

147 
let val np' = nprems_of st 

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

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

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

151 
in if k'+np' >= bnd 

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

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

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

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

158 
end 

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

160 

161 
val ITER_DEEPEN = THEN_ITER_DEEPEN all_tac; 

162 

163 

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

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

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

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

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

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

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

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

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

173 

1588  174 
(*** Bestfirst search ***) 
175 

176 
val trace_BEST_FIRST = ref false; 

177 

178 
(*Insertion into priority queue of states *) 

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

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

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

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

183 
then (n,th')::nths 

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

185 

186 
(*For creating output sequence*) 

187 
fun some_of_list [] = None 

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

190 

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

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

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

194 
fun THEN_BEST_FIRST tac0 (satp, sizef) tac1 = 

195 
let val tac = tracify trace_BEST_FIRST tac1 

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

197 
fun bfs (news,nprfs) = 

198 
(case partition satp news of 

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

200 
(map pairsize nonsats, nprfs)) 

201 
 (sats,_) => some_of_list sats) 

202 
and next [] = None 

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

204 
(if !trace_BEST_FIRST 

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

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

207 
else (); 

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

1588  210 
in traced_tac btac end; 
211 

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

213 
val BEST_FIRST = THEN_BEST_FIRST all_tac; 

214 

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

216 
SLOW  SHOULD NOT USE APPEND!*) 

217 
fun BREADTH_FIRST satpred tac = 

4270  218 
let val tacf = Seq.list_of o tac; 
1588  219 
fun bfs prfs = 
220 
(case partition satpred prfs of 

221 
([],[]) => [] 

222 
 ([],nonsats) => 

223 
(prs("breadth=" ^ string_of_int(length nonsats) ^ "\n"); 

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

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

228 

229 
(* Author: Norbert Voelker, FernUniversitaet Hagen 

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

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

232 
current level of search is taken into account. 

233 
*) 

234 

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

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

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

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

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

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

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

242 

243 
(*For creating output sequence*) 

244 
fun some_of_list [] = None 

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

247 
val trace_ASTAR = ref false; 

248 

249 
fun THEN_ASTAR tac0 (satp, costf) tac1 = 

250 
let val tf = tracify trace_ASTAR tac1; 

251 
fun bfs (news,nprfs,level) = 

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

253 
in (case partition satp news of 

254 
([],nonsats) 

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

256 
 (sats,_) => some_of_list sats) 

257 
end and 

258 
next [] = None 

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

260 
(if !trace_ASTAR 

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

262 
" cost = " ^ string_of_int n ^ 

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

264 
else (); 

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

1588  267 
in traced_tac tf end; 
268 

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

270 
val ASTAR = THEN_ASTAR all_tac; 

271 

272 
end; 

273 

274 
open Search; 