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