1 (* ========================================================================= *) |
|
2 (* THE ACTIVE SET OF CLAUSES *) |
|
3 (* Copyright (c) 2002-2006 Joe Hurd, distributed under the BSD License *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure Active :> Active = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Helper functions. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 local |
|
16 fun allFactors red = |
|
17 let |
|
18 fun allClause cl = List.all red (cl :: Clause.factor cl) |
|
19 in |
|
20 List.all allClause |
|
21 end; |
|
22 |
|
23 fun allResolutions red = |
|
24 let |
|
25 fun allClause2 cl_lit cl = |
|
26 let |
|
27 fun allLiteral2 lit = |
|
28 case total (Clause.resolve cl_lit) (cl,lit) of |
|
29 NONE => true |
|
30 | SOME cl => allFactors red [cl] |
|
31 in |
|
32 LiteralSet.all allLiteral2 (Clause.literals cl) |
|
33 end |
|
34 |
|
35 fun allClause1 allCls cl = |
|
36 let |
|
37 val cl = Clause.freshVars cl |
|
38 |
|
39 fun allLiteral1 lit = List.all (allClause2 (cl,lit)) allCls |
|
40 in |
|
41 LiteralSet.all allLiteral1 (Clause.literals cl) |
|
42 end |
|
43 in |
|
44 fn [] => true |
|
45 | allCls as cl :: cls => |
|
46 allClause1 allCls cl andalso allResolutions red cls |
|
47 end; |
|
48 |
|
49 fun allParamodulations red cls = |
|
50 let |
|
51 fun allClause2 cl_lit_ort_tm cl = |
|
52 let |
|
53 fun allLiteral2 lit = |
|
54 let |
|
55 val para = Clause.paramodulate cl_lit_ort_tm |
|
56 |
|
57 fun allSubterms (path,tm) = |
|
58 case total para (cl,lit,path,tm) of |
|
59 NONE => true |
|
60 | SOME cl => allFactors red [cl] |
|
61 in |
|
62 List.all allSubterms (Literal.nonVarTypedSubterms lit) |
|
63 end |
|
64 in |
|
65 LiteralSet.all allLiteral2 (Clause.literals cl) |
|
66 end |
|
67 |
|
68 fun allClause1 cl = |
|
69 let |
|
70 val cl = Clause.freshVars cl |
|
71 |
|
72 fun allLiteral1 lit = |
|
73 let |
|
74 fun allCl2 x = List.all (allClause2 x) cls |
|
75 in |
|
76 case total Literal.destEq lit of |
|
77 NONE => true |
|
78 | SOME (l,r) => |
|
79 allCl2 (cl,lit,Rewrite.LeftToRight,l) andalso |
|
80 allCl2 (cl,lit,Rewrite.RightToLeft,r) |
|
81 end |
|
82 in |
|
83 LiteralSet.all allLiteral1 (Clause.literals cl) |
|
84 end |
|
85 in |
|
86 List.all allClause1 cls |
|
87 end; |
|
88 |
|
89 fun redundant {subsume,reduce,rewrite} = |
|
90 let |
|
91 fun simp cl = |
|
92 case Clause.simplify cl of |
|
93 NONE => true |
|
94 | SOME cl => |
|
95 Subsume.isStrictlySubsumed subsume (Clause.literals cl) orelse |
|
96 let |
|
97 val cl' = cl |
|
98 val cl' = Clause.reduce reduce cl' |
|
99 val cl' = Clause.rewrite rewrite cl' |
|
100 in |
|
101 not (Clause.equalThms cl cl') andalso simp cl' |
|
102 end |
|
103 in |
|
104 simp |
|
105 end; |
|
106 in |
|
107 fun isSaturated ordering subs cls = |
|
108 let |
|
109 (*TRACE2 |
|
110 val ppCls = Parser.ppList Clause.pp |
|
111 val () = Parser.ppTrace ppCls "Active.checkSaturated: clauses" cls |
|
112 *) |
|
113 val red = Units.empty |
|
114 val rw = Rewrite.new (KnuthBendixOrder.compare ordering) |
|
115 val red = redundant {subsume = subs, reduce = red, rewrite = rw} |
|
116 in |
|
117 allFactors red cls andalso |
|
118 allResolutions red cls andalso |
|
119 allParamodulations red cls |
|
120 end; |
|
121 |
|
122 fun checkSaturated ordering subs cls = |
|
123 if isSaturated ordering subs cls then () else raise Bug "unsaturated"; |
|
124 end; |
|
125 |
|
126 (* ------------------------------------------------------------------------- *) |
|
127 (* A type of active clause sets. *) |
|
128 (* ------------------------------------------------------------------------- *) |
|
129 |
|
130 type simplify = {subsume : bool, reduce : bool, rewrite : bool}; |
|
131 |
|
132 type parameters = |
|
133 {clause : Clause.parameters, |
|
134 prefactor : simplify, |
|
135 postfactor : simplify}; |
|
136 |
|
137 datatype active = |
|
138 Active of |
|
139 {parameters : parameters, |
|
140 clauses : Clause.clause IntMap.map, |
|
141 units : Units.units, |
|
142 rewrite : Rewrite.rewrite, |
|
143 subsume : Clause.clause Subsume.subsume, |
|
144 literals : (Clause.clause * Literal.literal) LiteralNet.literalNet, |
|
145 equations : |
|
146 (Clause.clause * Literal.literal * Rewrite.orient * Term.term) |
|
147 TermNet.termNet, |
|
148 subterms : |
|
149 (Clause.clause * Literal.literal * Term.path * Term.term) |
|
150 TermNet.termNet, |
|
151 allSubterms : (Clause.clause * Term.term) TermNet.termNet}; |
|
152 |
|
153 fun getSubsume (Active {subsume = s, ...}) = s; |
|
154 |
|
155 fun setRewrite active rewrite = |
|
156 let |
|
157 val Active |
|
158 {parameters,clauses,units,subsume,literals,equations, |
|
159 subterms,allSubterms,...} = active |
|
160 in |
|
161 Active |
|
162 {parameters = parameters, clauses = clauses, units = units, |
|
163 rewrite = rewrite, subsume = subsume, literals = literals, |
|
164 equations = equations, subterms = subterms, allSubterms = allSubterms} |
|
165 end; |
|
166 |
|
167 (* ------------------------------------------------------------------------- *) |
|
168 (* Basic operations. *) |
|
169 (* ------------------------------------------------------------------------- *) |
|
170 |
|
171 val maxSimplify : simplify = {subsume = true, reduce = true, rewrite = true}; |
|
172 |
|
173 val default : parameters = |
|
174 {clause = Clause.default, |
|
175 prefactor = maxSimplify, |
|
176 postfactor = maxSimplify}; |
|
177 |
|
178 fun empty parameters = |
|
179 let |
|
180 val {clause,...} = parameters |
|
181 val {ordering,...} = clause |
|
182 in |
|
183 Active |
|
184 {parameters = parameters, |
|
185 clauses = IntMap.new (), |
|
186 units = Units.empty, |
|
187 rewrite = Rewrite.new (KnuthBendixOrder.compare ordering), |
|
188 subsume = Subsume.new (), |
|
189 literals = LiteralNet.new {fifo = false}, |
|
190 equations = TermNet.new {fifo = false}, |
|
191 subterms = TermNet.new {fifo = false}, |
|
192 allSubterms = TermNet.new {fifo = false}} |
|
193 end; |
|
194 |
|
195 fun size (Active {clauses,...}) = IntMap.size clauses; |
|
196 |
|
197 fun clauses (Active {clauses = cls, ...}) = |
|
198 let |
|
199 fun add (_,cl,acc) = cl :: acc |
|
200 in |
|
201 IntMap.foldr add [] cls |
|
202 end; |
|
203 |
|
204 fun saturated active = |
|
205 let |
|
206 fun remove (cl,(cls,subs)) = |
|
207 let |
|
208 val lits = Clause.literals cl |
|
209 in |
|
210 if Subsume.isStrictlySubsumed subs lits then (cls,subs) |
|
211 else (cl :: cls, Subsume.insert subs (lits,())) |
|
212 end |
|
213 |
|
214 val cls = clauses active |
|
215 val (cls,_) = foldl remove ([], Subsume.new ()) cls |
|
216 val (cls,subs) = foldl remove ([], Subsume.new ()) cls |
|
217 |
|
218 (*DEBUG |
|
219 val Active {parameters,...} = active |
|
220 val {clause,...} = parameters |
|
221 val {ordering,...} = clause |
|
222 val () = checkSaturated ordering subs cls |
|
223 *) |
|
224 in |
|
225 cls |
|
226 end; |
|
227 |
|
228 (* ------------------------------------------------------------------------- *) |
|
229 (* Pretty printing. *) |
|
230 (* ------------------------------------------------------------------------- *) |
|
231 |
|
232 val pp = |
|
233 let |
|
234 fun toStr active = "Active{" ^ Int.toString (size active) ^ "}" |
|
235 in |
|
236 Parser.ppMap toStr Parser.ppString |
|
237 end; |
|
238 |
|
239 (*DEBUG |
|
240 local |
|
241 open Parser; |
|
242 |
|
243 fun ppField f ppA p a = |
|
244 (beginBlock p Inconsistent 2; |
|
245 addString p (f ^ " ="); |
|
246 addBreak p (1,0); |
|
247 ppA p a; |
|
248 endBlock p); |
|
249 |
|
250 val ppClauses = |
|
251 ppField "clauses" |
|
252 (Parser.ppMap IntMap.toList |
|
253 (Parser.ppList (Parser.ppPair Parser.ppInt Clause.pp))); |
|
254 |
|
255 val ppRewrite = ppField "rewrite" Rewrite.pp; |
|
256 |
|
257 val ppSubterms = |
|
258 ppField "subterms" |
|
259 (TermNet.pp |
|
260 (Parser.ppMap (fn (c,l,p,t) => ((Clause.id c, l, p), t)) |
|
261 (Parser.ppPair |
|
262 (Parser.ppTriple Parser.ppInt Literal.pp Term.ppPath) |
|
263 Term.pp))); |
|
264 in |
|
265 fun pp p (Active {clauses,rewrite,subterms,...}) = |
|
266 (beginBlock p Inconsistent 2; |
|
267 addString p "Active"; |
|
268 addBreak p (1,0); |
|
269 beginBlock p Inconsistent 1; |
|
270 addString p "{"; |
|
271 ppClauses p clauses; |
|
272 addString p ","; |
|
273 addBreak p (1,0); |
|
274 ppRewrite p rewrite; |
|
275 (*TRACE5 |
|
276 addString p ","; |
|
277 addBreak p (1,0); |
|
278 ppSubterms p subterms; |
|
279 *) |
|
280 endBlock p; |
|
281 addString p "}"; |
|
282 endBlock p); |
|
283 end; |
|
284 *) |
|
285 |
|
286 val toString = Parser.toString pp; |
|
287 |
|
288 (* ------------------------------------------------------------------------- *) |
|
289 (* Simplify clauses. *) |
|
290 (* ------------------------------------------------------------------------- *) |
|
291 |
|
292 fun simplify simp units rewr subs = |
|
293 let |
|
294 val {subsume = s, reduce = r, rewrite = w} = simp |
|
295 |
|
296 fun rewrite cl = |
|
297 let |
|
298 val cl' = Clause.rewrite rewr cl |
|
299 in |
|
300 if Clause.equalThms cl cl' then SOME cl else Clause.simplify cl' |
|
301 end |
|
302 in |
|
303 fn cl => |
|
304 case Clause.simplify cl of |
|
305 NONE => NONE |
|
306 | SOME cl => |
|
307 case (if w then rewrite cl else SOME cl) of |
|
308 NONE => NONE |
|
309 | SOME cl => |
|
310 let |
|
311 val cl = if r then Clause.reduce units cl else cl |
|
312 in |
|
313 if s andalso Clause.subsumes subs cl then NONE else SOME cl |
|
314 end |
|
315 end; |
|
316 |
|
317 (*DEBUG |
|
318 val simplify = fn simp => fn units => fn rewr => fn subs => fn cl => |
|
319 let |
|
320 fun traceCl s = Parser.ppTrace Clause.pp ("Active.simplify: " ^ s) |
|
321 (*TRACE4 |
|
322 val ppClOpt = Parser.ppOption Clause.pp |
|
323 val () = traceCl "cl" cl |
|
324 *) |
|
325 val cl' = simplify simp units rewr subs cl |
|
326 (*TRACE4 |
|
327 val () = Parser.ppTrace ppClOpt "Active.simplify: cl'" cl' |
|
328 *) |
|
329 val () = |
|
330 case cl' of |
|
331 NONE => () |
|
332 | SOME cl' => |
|
333 case |
|
334 (case simplify simp units rewr subs cl' of |
|
335 NONE => SOME ("away", K ()) |
|
336 | SOME cl'' => |
|
337 if Clause.equalThms cl' cl'' then NONE |
|
338 else SOME ("further", fn () => traceCl "cl''" cl'')) of |
|
339 NONE => () |
|
340 | SOME (e,f) => |
|
341 let |
|
342 val () = traceCl "cl" cl |
|
343 val () = traceCl "cl'" cl' |
|
344 val () = f () |
|
345 in |
|
346 raise |
|
347 Bug |
|
348 ("Active.simplify: clause should have been simplified "^e) |
|
349 end |
|
350 in |
|
351 cl' |
|
352 end; |
|
353 *) |
|
354 |
|
355 fun simplifyActive simp active = |
|
356 let |
|
357 val Active {units,rewrite,subsume,...} = active |
|
358 in |
|
359 simplify simp units rewrite subsume |
|
360 end; |
|
361 |
|
362 (* ------------------------------------------------------------------------- *) |
|
363 (* Add a clause into the active set. *) |
|
364 (* ------------------------------------------------------------------------- *) |
|
365 |
|
366 fun addUnit units cl = |
|
367 let |
|
368 val th = Clause.thm cl |
|
369 in |
|
370 case total Thm.destUnit th of |
|
371 SOME lit => Units.add units (lit,th) |
|
372 | NONE => units |
|
373 end; |
|
374 |
|
375 fun addRewrite rewrite cl = |
|
376 let |
|
377 val th = Clause.thm cl |
|
378 in |
|
379 case total Thm.destUnitEq th of |
|
380 SOME l_r => Rewrite.add rewrite (Clause.id cl, (l_r,th)) |
|
381 | NONE => rewrite |
|
382 end; |
|
383 |
|
384 fun addSubsume subsume cl = Subsume.insert subsume (Clause.literals cl, cl); |
|
385 |
|
386 fun addLiterals literals cl = |
|
387 let |
|
388 fun add (lit as (_,atm), literals) = |
|
389 if Atom.isEq atm then literals |
|
390 else LiteralNet.insert literals (lit,(cl,lit)) |
|
391 in |
|
392 LiteralSet.foldl add literals (Clause.largestLiterals cl) |
|
393 end; |
|
394 |
|
395 fun addEquations equations cl = |
|
396 let |
|
397 fun add ((lit,ort,tm),equations) = |
|
398 TermNet.insert equations (tm,(cl,lit,ort,tm)) |
|
399 in |
|
400 foldl add equations (Clause.largestEquations cl) |
|
401 end; |
|
402 |
|
403 fun addSubterms subterms cl = |
|
404 let |
|
405 fun add ((lit,path,tm),subterms) = |
|
406 TermNet.insert subterms (tm,(cl,lit,path,tm)) |
|
407 in |
|
408 foldl add subterms (Clause.largestSubterms cl) |
|
409 end; |
|
410 |
|
411 fun addAllSubterms allSubterms cl = |
|
412 let |
|
413 fun add ((_,_,tm),allSubterms) = |
|
414 TermNet.insert allSubterms (tm,(cl,tm)) |
|
415 in |
|
416 foldl add allSubterms (Clause.allSubterms cl) |
|
417 end; |
|
418 |
|
419 fun addClause active cl = |
|
420 let |
|
421 val Active |
|
422 {parameters,clauses,units,rewrite,subsume,literals, |
|
423 equations,subterms,allSubterms} = active |
|
424 val clauses = IntMap.insert clauses (Clause.id cl, cl) |
|
425 and subsume = addSubsume subsume cl |
|
426 and literals = addLiterals literals cl |
|
427 and equations = addEquations equations cl |
|
428 and subterms = addSubterms subterms cl |
|
429 and allSubterms = addAllSubterms allSubterms cl |
|
430 in |
|
431 Active |
|
432 {parameters = parameters, clauses = clauses, units = units, |
|
433 rewrite = rewrite, subsume = subsume, literals = literals, |
|
434 equations = equations, subterms = subterms, |
|
435 allSubterms = allSubterms} |
|
436 end; |
|
437 |
|
438 fun addFactorClause active cl = |
|
439 let |
|
440 val Active |
|
441 {parameters,clauses,units,rewrite,subsume,literals, |
|
442 equations,subterms,allSubterms} = active |
|
443 val units = addUnit units cl |
|
444 and rewrite = addRewrite rewrite cl |
|
445 in |
|
446 Active |
|
447 {parameters = parameters, clauses = clauses, units = units, |
|
448 rewrite = rewrite, subsume = subsume, literals = literals, |
|
449 equations = equations, subterms = subterms, allSubterms = allSubterms} |
|
450 end; |
|
451 |
|
452 (* ------------------------------------------------------------------------- *) |
|
453 (* Derive (unfactored) consequences of a clause. *) |
|
454 (* ------------------------------------------------------------------------- *) |
|
455 |
|
456 fun deduceResolution literals cl (lit as (_,atm), acc) = |
|
457 let |
|
458 fun resolve (cl_lit,acc) = |
|
459 case total (Clause.resolve cl_lit) (cl,lit) of |
|
460 SOME cl' => cl' :: acc |
|
461 | NONE => acc |
|
462 (*TRACE4 |
|
463 val () = Parser.ppTrace Literal.pp "Active.deduceResolution: lit" lit |
|
464 *) |
|
465 in |
|
466 if Atom.isEq atm then acc |
|
467 else foldl resolve acc (LiteralNet.unify literals (Literal.negate lit)) |
|
468 end; |
|
469 |
|
470 fun deduceParamodulationWith subterms cl ((lit,ort,tm),acc) = |
|
471 let |
|
472 fun para (cl_lit_path_tm,acc) = |
|
473 case total (Clause.paramodulate (cl,lit,ort,tm)) cl_lit_path_tm of |
|
474 SOME cl' => cl' :: acc |
|
475 | NONE => acc |
|
476 in |
|
477 foldl para acc (TermNet.unify subterms tm) |
|
478 end; |
|
479 |
|
480 fun deduceParamodulationInto equations cl ((lit,path,tm),acc) = |
|
481 let |
|
482 fun para (cl_lit_ort_tm,acc) = |
|
483 case total (Clause.paramodulate cl_lit_ort_tm) (cl,lit,path,tm) of |
|
484 SOME cl' => cl' :: acc |
|
485 | NONE => acc |
|
486 in |
|
487 foldl para acc (TermNet.unify equations tm) |
|
488 end; |
|
489 |
|
490 fun deduce active cl = |
|
491 let |
|
492 val Active {parameters,literals,equations,subterms,...} = active |
|
493 |
|
494 val lits = Clause.largestLiterals cl |
|
495 val eqns = Clause.largestEquations cl |
|
496 val subtms = |
|
497 if TermNet.null equations then [] else Clause.largestSubterms cl |
|
498 |
|
499 val acc = [] |
|
500 val acc = LiteralSet.foldl (deduceResolution literals cl) acc lits |
|
501 val acc = foldl (deduceParamodulationWith subterms cl) acc eqns |
|
502 val acc = foldl (deduceParamodulationInto equations cl) acc subtms |
|
503 in |
|
504 rev acc |
|
505 end; |
|
506 |
|
507 (* ------------------------------------------------------------------------- *) |
|
508 (* Extract clauses from the active set that can be simplified. *) |
|
509 (* ------------------------------------------------------------------------- *) |
|
510 |
|
511 local |
|
512 fun clause_rewritables active = |
|
513 let |
|
514 val Active {clauses,rewrite,...} = active |
|
515 |
|
516 fun rewr (id,cl,ids) = |
|
517 let |
|
518 val cl' = Clause.rewrite rewrite cl |
|
519 in |
|
520 if Clause.equalThms cl cl' then ids else IntSet.add ids id |
|
521 end |
|
522 in |
|
523 IntMap.foldr rewr IntSet.empty clauses |
|
524 end; |
|
525 |
|
526 fun orderedRedexResidues (((l,r),_),ort) = |
|
527 case ort of |
|
528 NONE => [] |
|
529 | SOME Rewrite.LeftToRight => [(l,r,true)] |
|
530 | SOME Rewrite.RightToLeft => [(r,l,true)]; |
|
531 |
|
532 fun unorderedRedexResidues (((l,r),_),ort) = |
|
533 case ort of |
|
534 NONE => [(l,r,false),(r,l,false)] |
|
535 | SOME _ => []; |
|
536 |
|
537 fun rewrite_rewritables active rewr_ids = |
|
538 let |
|
539 val Active {parameters,rewrite,clauses,allSubterms,...} = active |
|
540 val {clause = {ordering,...}, ...} = parameters |
|
541 val order = KnuthBendixOrder.compare ordering |
|
542 |
|
543 fun addRewr (id,acc) = |
|
544 if IntMap.inDomain id clauses then IntSet.add acc id else acc |
|
545 |
|
546 fun addReduce ((l,r,ord),acc) = |
|
547 let |
|
548 fun isValidRewr tm = |
|
549 case total (Subst.match Subst.empty l) tm of |
|
550 NONE => false |
|
551 | SOME sub => |
|
552 ord orelse |
|
553 let |
|
554 val tm' = Subst.subst (Subst.normalize sub) r |
|
555 in |
|
556 order (tm,tm') = SOME GREATER |
|
557 end |
|
558 |
|
559 fun addRed ((cl,tm),acc) = |
|
560 let |
|
561 (*TRACE5 |
|
562 val () = Parser.ppTrace Clause.pp "Active.addRed: cl" cl |
|
563 val () = Parser.ppTrace Term.pp "Active.addRed: tm" tm |
|
564 *) |
|
565 val id = Clause.id cl |
|
566 in |
|
567 if IntSet.member id acc then acc |
|
568 else if not (isValidRewr tm) then acc |
|
569 else IntSet.add acc id |
|
570 end |
|
571 |
|
572 (*TRACE5 |
|
573 val () = Parser.ppTrace Term.pp "Active.addReduce: l" l |
|
574 val () = Parser.ppTrace Term.pp "Active.addReduce: r" r |
|
575 val () = Parser.ppTrace Parser.ppBool "Active.addReduce: ord" ord |
|
576 *) |
|
577 in |
|
578 List.foldl addRed acc (TermNet.matched allSubterms l) |
|
579 end |
|
580 |
|
581 fun addEquation redexResidues (id,acc) = |
|
582 case Rewrite.peek rewrite id of |
|
583 NONE => acc |
|
584 | SOME eqn_ort => List.foldl addReduce acc (redexResidues eqn_ort) |
|
585 |
|
586 val addOrdered = addEquation orderedRedexResidues |
|
587 |
|
588 val addUnordered = addEquation unorderedRedexResidues |
|
589 |
|
590 val ids = IntSet.empty |
|
591 val ids = List.foldl addRewr ids rewr_ids |
|
592 val ids = List.foldl addOrdered ids rewr_ids |
|
593 val ids = List.foldl addUnordered ids rewr_ids |
|
594 in |
|
595 ids |
|
596 end; |
|
597 |
|
598 fun choose_clause_rewritables active ids = size active <= length ids |
|
599 |
|
600 fun rewritables active ids = |
|
601 if choose_clause_rewritables active ids then clause_rewritables active |
|
602 else rewrite_rewritables active ids; |
|
603 |
|
604 (*DEBUG |
|
605 val rewritables = fn active => fn ids => |
|
606 let |
|
607 val clause_ids = clause_rewritables active |
|
608 val rewrite_ids = rewrite_rewritables active ids |
|
609 |
|
610 val () = |
|
611 if IntSet.equal rewrite_ids clause_ids then () |
|
612 else |
|
613 let |
|
614 val ppIdl = Parser.ppList Parser.ppInt |
|
615 val ppIds = Parser.ppMap IntSet.toList ppIdl |
|
616 val () = Parser.ppTrace pp "Active.rewritables: active" active |
|
617 val () = Parser.ppTrace ppIdl "Active.rewritables: ids" ids |
|
618 val () = Parser.ppTrace ppIds |
|
619 "Active.rewritables: clause_ids" clause_ids |
|
620 val () = Parser.ppTrace ppIds |
|
621 "Active.rewritables: rewrite_ids" rewrite_ids |
|
622 in |
|
623 raise Bug "Active.rewritables: ~(rewrite_ids SUBSET clause_ids)" |
|
624 end |
|
625 in |
|
626 if choose_clause_rewritables active ids then clause_ids else rewrite_ids |
|
627 end; |
|
628 *) |
|
629 |
|
630 fun delete active ids = |
|
631 if IntSet.null ids then active |
|
632 else |
|
633 let |
|
634 fun idPred id = not (IntSet.member id ids) |
|
635 |
|
636 fun clausePred cl = idPred (Clause.id cl) |
|
637 |
|
638 val Active |
|
639 {parameters,clauses,units,rewrite,subsume,literals, |
|
640 equations,subterms,allSubterms} = active |
|
641 |
|
642 val clauses = IntMap.filter (idPred o fst) clauses |
|
643 and subsume = Subsume.filter clausePred subsume |
|
644 and literals = LiteralNet.filter (clausePred o #1) literals |
|
645 and equations = TermNet.filter (clausePred o #1) equations |
|
646 and subterms = TermNet.filter (clausePred o #1) subterms |
|
647 and allSubterms = TermNet.filter (clausePred o fst) allSubterms |
|
648 in |
|
649 Active |
|
650 {parameters = parameters, clauses = clauses, units = units, |
|
651 rewrite = rewrite, subsume = subsume, literals = literals, |
|
652 equations = equations, subterms = subterms, |
|
653 allSubterms = allSubterms} |
|
654 end; |
|
655 in |
|
656 fun extract_rewritables (active as Active {clauses,rewrite,...}) = |
|
657 if Rewrite.isReduced rewrite then (active,[]) |
|
658 else |
|
659 let |
|
660 (*TRACE3 |
|
661 val () = trace "Active.extract_rewritables: inter-reducing\n" |
|
662 *) |
|
663 val (rewrite,ids) = Rewrite.reduce' rewrite |
|
664 val active = setRewrite active rewrite |
|
665 val ids = rewritables active ids |
|
666 val cls = IntSet.transform (IntMap.get clauses) ids |
|
667 (*TRACE3 |
|
668 val ppCls = Parser.ppList Clause.pp |
|
669 val () = Parser.ppTrace ppCls "Active.extract_rewritables: cls" cls |
|
670 *) |
|
671 in |
|
672 (delete active ids, cls) |
|
673 end |
|
674 (*DEBUG |
|
675 handle Error err => |
|
676 raise Bug ("Active.extract_rewritables: shouldn't fail\n" ^ err); |
|
677 *) |
|
678 end; |
|
679 |
|
680 (* ------------------------------------------------------------------------- *) |
|
681 (* Factor clauses. *) |
|
682 (* ------------------------------------------------------------------------- *) |
|
683 |
|
684 local |
|
685 fun prefactor_simplify active subsume = |
|
686 let |
|
687 val Active {parameters,units,rewrite,...} = active |
|
688 val {prefactor,...} = parameters |
|
689 in |
|
690 simplify prefactor units rewrite subsume |
|
691 end; |
|
692 |
|
693 fun postfactor_simplify active subsume = |
|
694 let |
|
695 val Active {parameters,units,rewrite,...} = active |
|
696 val {postfactor,...} = parameters |
|
697 in |
|
698 simplify postfactor units rewrite subsume |
|
699 end; |
|
700 |
|
701 val sort_utilitywise = |
|
702 let |
|
703 fun utility cl = |
|
704 case LiteralSet.size (Clause.literals cl) of |
|
705 0 => ~1 |
|
706 | 1 => if Thm.isUnitEq (Clause.thm cl) then 0 else 1 |
|
707 | n => n |
|
708 in |
|
709 sortMap utility Int.compare |
|
710 end; |
|
711 |
|
712 fun factor_add (cl, active_subsume_acc as (active,subsume,acc)) = |
|
713 case postfactor_simplify active subsume cl of |
|
714 NONE => active_subsume_acc |
|
715 | SOME cl => |
|
716 let |
|
717 val active = addFactorClause active cl |
|
718 and subsume = addSubsume subsume cl |
|
719 and acc = cl :: acc |
|
720 in |
|
721 (active,subsume,acc) |
|
722 end; |
|
723 |
|
724 fun factor1 (cl, active_subsume_acc as (active,subsume,_)) = |
|
725 case prefactor_simplify active subsume cl of |
|
726 NONE => active_subsume_acc |
|
727 | SOME cl => |
|
728 let |
|
729 val cls = sort_utilitywise (cl :: Clause.factor cl) |
|
730 in |
|
731 foldl factor_add active_subsume_acc cls |
|
732 end; |
|
733 |
|
734 fun factor' active acc [] = (active, rev acc) |
|
735 | factor' active acc cls = |
|
736 let |
|
737 val cls = sort_utilitywise cls |
|
738 val subsume = getSubsume active |
|
739 val (active,_,acc) = foldl factor1 (active,subsume,acc) cls |
|
740 val (active,cls) = extract_rewritables active |
|
741 in |
|
742 factor' active acc cls |
|
743 end; |
|
744 in |
|
745 fun factor active cls = factor' active [] cls; |
|
746 end; |
|
747 |
|
748 (*TRACE4 |
|
749 val factor = fn active => fn cls => |
|
750 let |
|
751 val ppCls = Parser.ppList Clause.pp |
|
752 val () = Parser.ppTrace ppCls "Active.factor: cls" cls |
|
753 val (active,cls') = factor active cls |
|
754 val () = Parser.ppTrace ppCls "Active.factor: cls'" cls' |
|
755 in |
|
756 (active,cls') |
|
757 end; |
|
758 *) |
|
759 |
|
760 (* ------------------------------------------------------------------------- *) |
|
761 (* Create a new active clause set and initialize clauses. *) |
|
762 (* ------------------------------------------------------------------------- *) |
|
763 |
|
764 fun new parameters ths = |
|
765 let |
|
766 val {clause,...} = parameters |
|
767 |
|
768 fun mk_clause th = |
|
769 Clause.mk {parameters = clause, id = Clause.newId (), thm = th} |
|
770 |
|
771 val cls = map mk_clause ths |
|
772 in |
|
773 factor (empty parameters) cls |
|
774 end; |
|
775 |
|
776 (* ------------------------------------------------------------------------- *) |
|
777 (* Add a clause into the active set and deduce all consequences. *) |
|
778 (* ------------------------------------------------------------------------- *) |
|
779 |
|
780 fun add active cl = |
|
781 case simplifyActive maxSimplify active cl of |
|
782 NONE => (active,[]) |
|
783 | SOME cl' => |
|
784 if Clause.isContradiction cl' then (active,[cl']) |
|
785 else if not (Clause.equalThms cl cl') then factor active [cl'] |
|
786 else |
|
787 let |
|
788 (*TRACE3 |
|
789 val () = Parser.ppTrace Clause.pp "Active.add: cl" cl |
|
790 *) |
|
791 val active = addClause active cl |
|
792 val cl = Clause.freshVars cl |
|
793 val cls = deduce active cl |
|
794 val (active,cls) = factor active cls |
|
795 (*TRACE2 |
|
796 val ppCls = Parser.ppList Clause.pp |
|
797 val () = Parser.ppTrace ppCls "Active.add: cls" cls |
|
798 *) |
|
799 in |
|
800 (active,cls) |
|
801 end; |
|
802 |
|
803 end |
|