1(* ========================================================================= *) 2(* PROCESSING SETS OF CLAUSES AT A TIME *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["mlibClause", "mlibUnits"]; 8*) 9 10(* 11*) 12structure mlibClauseset :> mlibClauseset = 13struct 14 15infix |-> ::> ##; 16 17open mlibUseful mlibTerm mlibClause; 18 19structure T = mlibTermnet; local open mlibTermnet in end; 20structure N = mlibLiteralnet; local open mlibLiteralnet in end; 21structure S = mlibSubsume; local open mlibSubsume in end; 22structure U = mlibUnits; local open mlibUnits in end; 23 24type 'a termnet = 'a T.termnet; 25type 'a literalnet = 'a N.literalnet; 26type 'a subsume = 'a S.subsume; 27 28val |<>| = mlibSubst.|<>|; 29val op ::> = mlibSubst.::>; 30val term_subst = mlibSubst.term_subst; 31val formula_subst = mlibSubst.formula_subst; 32 33(* ------------------------------------------------------------------------- *) 34(* Chatting. *) 35(* ------------------------------------------------------------------------- *) 36 37val module = "mlibClauseset"; 38val () = add_trace {module = module, alignment = I} 39fun chatting l = tracing {module = module, level = l}; 40fun chat s = (trace s; true) 41 42(* ------------------------------------------------------------------------- *) 43(* Parameters *) 44(* ------------------------------------------------------------------------- *) 45 46type filter = {subsumption : bool, simplification : int, splitting : bool} 47type parameters = {prefactoring : filter, postfactoring : filter} 48 49val defaults = 50 {prefactoring = {subsumption = true, simplification = 2, splitting = false}, 51 postfactoring = {subsumption = true, simplification = 2, splitting = false}}; 52 53fun update_subsumption f (parm : filter) : filter = 54 let val {subsumption = s, simplification = r, splitting = v} = parm 55 in {subsumption = f s, simplification = r, splitting = v} 56 end; 57 58fun update_simplification f (parm : filter) : filter = 59 let val {subsumption = s, simplification = r, splitting = v} = parm 60 in {subsumption = s, simplification = f r, splitting = v} 61 end; 62 63fun update_splitting f (parm : filter) : filter = 64 let val {subsumption = s, simplification = r, splitting = v} = parm 65 in {subsumption = s, simplification = r, splitting = f v} 66 end; 67 68fun update_prefactoring f (parm : parameters) : parameters = 69 let val {prefactoring = a, postfactoring = b} = parm 70 in {prefactoring = f a, postfactoring = b} 71 end; 72 73fun update_postfactoring f (parm : parameters) : parameters = 74 let val {prefactoring = a, postfactoring = b} = parm 75 in {prefactoring = a, postfactoring = f b} 76 end; 77 78(* ------------------------------------------------------------------------- *) 79(* Helper functions. *) 80(* ------------------------------------------------------------------------- *) 81 82fun ofilt _ NONE = NONE | ofilt p (s as SOME x) = if p x then s else NONE; 83 84fun olist NONE = [] | olist (SOME x) = [x]; 85 86val intset_to_string = to_string (pp_map Intset.listItems (pp_list pp_int)); 87 88fun psym lit = 89 let 90 val (s,(x,y)) = (I ## dest_eq) (dest_literal lit) 91 val () = assert (x <> y) (Error "psym: refl") 92 in 93 mk_literal (s, mk_eq (y,x)) 94 end; 95 96fun add_unit cl units = 97 let val {thm, ...} = dest_clause cl in U.add thm units end; 98 99fun add_subsum cl = S.add (literals cl |-> cl); 100 101fun clause_subterm c n p = literal_subterm p (List.nth (literals c, n)); 102 103val clause_to_string = to_string mlibClause.pp_clause; 104 105val rewrs_to_string = to_string mlibClause.pp_rewrs; 106 107val literals_to_string = to_string (N.pp_literalnet (pp_pair pp_clause pp_int)); 108 109(* ------------------------------------------------------------------------- *) 110(* mlibClause sets *) 111(* ------------------------------------------------------------------------- *) 112 113datatype clauseset = SET of 114 {parm : mlibClause.parameters * parameters, 115 size : int, 116 units : U.units, 117 rewrites : rewrs, 118 clauses : clause list, 119 subsumers : clause subsume, 120 literals : (clause * int) literalnet, 121 equalities : (clause * int * bool) termnet, 122 subterms : (clause * int * int list) termnet}; 123 124fun update_size n set = 125 let 126 val SET {parm = z, size = _, units = u, rewrites = r, clauses = c, 127 subsumers = s, literals = l, equalities = e, subterms = p} = set 128 in 129 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 130 subsumers = s, literals = l, equalities = e, subterms = p} 131 end; 132 133fun update_units u set = 134 let 135 val SET {parm = z, size = n, units = _, rewrites = r, clauses = c, 136 subsumers = s, literals = l, equalities = e, subterms = p} = set 137 in 138 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 139 subsumers = s, literals = l, equalities = e, subterms = p} 140 end; 141 142fun update_rewrites r set = 143 let 144 val SET {parm = z, size = n, units = u, rewrites = _, clauses = c, 145 subsumers = s, literals = l, equalities = e, subterms = p} = set 146 in 147 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 148 subsumers = s, literals = l, equalities = e, subterms = p} 149 end; 150 151fun update_clauses c set = 152 let 153 val SET {parm = z, size = n, units = u, rewrites = r, clauses = _, 154 subsumers = s, literals = l, equalities = e, subterms = p} = set 155 in 156 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 157 subsumers = s, literals = l, equalities = e, subterms = p} 158 end; 159 160fun update_subsumers s set = 161 let 162 val SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 163 subsumers = _, literals = l, equalities = e, subterms = p} = set 164 in 165 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 166 subsumers = s, literals = l, equalities = e, subterms = p} 167 end; 168 169fun update_literals l set = 170 let 171 val SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 172 subsumers = s, literals = _, equalities = e, subterms = p} = set 173 in 174 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 175 subsumers = s, literals = l, equalities = e, subterms = p} 176 end; 177 178fun update_equalities e set = 179 let 180 val SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 181 subsumers = s, literals = l, equalities = _, subterms = p} = set 182 in 183 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 184 subsumers = s, literals = l, equalities = e, subterms = p} 185 end; 186 187fun update_subterms p set = 188 let 189 val SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 190 subsumers = s, literals = l, equalities = e, subterms = _} = set 191 in 192 SET {parm = z, size = n, units = u, rewrites = r, clauses = c, 193 subsumers = s, literals = l, equalities = e, subterms = p} 194 end; 195 196(* ------------------------------------------------------------------------- *) 197(* Basic operations *) 198(* ------------------------------------------------------------------------- *) 199 200fun empty (cparm,parm) = 201 SET {parm = (cparm,parm), size = 0, units = U.empty, 202 rewrites = mlibClause.empty cparm, clauses = [], subsumers = S.empty (), 203 literals = N.empty {fifo = false}, equalities = T.empty {fifo = false}, 204 subterms = T.empty {fifo = false}}; 205 206fun parm (SET {parm, ...}) = parm; 207 208fun ssize (SET {size, ...}) = size; 209 210fun units (SET {units, ...}) = units; 211 212fun rewrites (SET {rewrites, ...}) = rewrites; 213 214fun clauses (SET {clauses, ...}) = clauses; 215 216fun new_units u set = update_units u set; 217 218(* ------------------------------------------------------------------------- *) 219(* Simplify and strengthen clauses *) 220(* ------------------------------------------------------------------------- *) 221 222fun qsimplify set = let val SET {rewrites = r, ...} = set in QREWRITE r end; 223 224fun simplify set = let val SET {rewrites = r, ...} = set in REWRITE r end; 225 226local 227 fun taut c = assert (not (mlibCanon.tautologous (literals c))) (Error "taut"); 228 fun beef_up (SET {units, ...}) cl = 229 let 230 val () = taut cl 231 val cl = NEQ_VARS cl 232 val () = taut cl 233 val cl = DEMODULATE units cl 234 in 235 cl 236 end; 237in 238 fun strengthen set = total (beef_up set); 239end; 240 241(* ------------------------------------------------------------------------- *) 242(* mlibClause splitting *) 243(* ------------------------------------------------------------------------- *) 244 245local 246 fun new_pred () = 247 case new_var () of Var v => Atom (Fn (v, [])) 248 | Fn _ => raise Bug "new_pred: new_var didn't return a var"; 249 250 fun AX cl lits = mk_clause (#parm (dest_clause cl)) (mlibThm.AXIOM lits); 251 252 fun new l = Binaryset.addList (Binaryset.empty String.compare, l); 253 fun disjoint s t = Binaryset.isEmpty (Binaryset.intersection (s,t)); 254 fun union s t = Binaryset.union (s,t); 255 256 fun add_lits lits shar = foldl (fn ((_,x),l) => x :: l) lits shar; 257 fun add_vars vars shar = foldl (fn ((v,_),s) => union v s) vars shar; 258 259 fun dfs acc lits vars vlits = 260 case List.partition (disjoint vars o fst) vlits of 261 (_,[]) => components (rev lits :: acc) vlits 262 | (disj,shar) => dfs acc (add_lits lits shar) (add_vars vars shar) disj 263 and components acc [] = acc 264 | components acc ((vs,lit) :: rest) = dfs acc [lit] vs rest; 265 266 fun spl _ _ [] = raise Bug "split: empty" 267 | spl cl acc [c] = rev (AX cl c :: acc) 268 | spl cl acc (c1 :: c2 :: cs) = 269 let val p = new_pred () 270 in spl cl (AX cl (c1 @ [p]) :: acc) ((Not p :: c2) :: cs) 271 end; 272 273 fun split_clause cl comps = 274 let 275 val _ = chatting 2 andalso chat "%" 276 val cls = spl cl [] comps 277 val _ = chatting 5 andalso chat 278 ("\nsplit: components of clause " ^ clause_to_string cl ^ ":\n" 279 ^ PP.pp_to_string (!LINE_LENGTH) (pp_list pp_clause) cls ^ "\n") 280 in 281 cls 282 end; 283in 284 fun split cl = 285 let 286 val lits = map (fn lit => (FV lit, lit)) (literals cl) 287 val (glits,vlits) = List.partition (null o fst) lits 288 val glits = map snd glits 289 val vlits = map (new ## I) vlits 290 in 291 case components [] vlits of [] => [cl] 292 | [_] => [cl] 293 | l => split_clause cl (rev (if null glits then l else glits :: l)) 294 end 295end; 296 297(* ------------------------------------------------------------------------- *) 298(* Forward subsumption checking *) 299(* ------------------------------------------------------------------------- *) 300 301fun subsum subs cl = 302 let 303 fun f (sub,c) = 304 case total (INST sub) c of NONE => false | SOME d => subsumes d cl 305 in 306 mlibStream.exists f (S.subsumes' subs (literals cl)) 307 end; 308 309fun subsumed (SET {subsumers, ...}) = subsum subsumers; 310 311(* ------------------------------------------------------------------------- *) 312(* Add a clause into the set *) 313(* ------------------------------------------------------------------------- *) 314 315fun add_rewr cl set = 316 if not (is_rewr cl) then (cl,set) else 317 let 318 val SET {rewrites = r, ...} = set 319 val cl = mlibClause.drop_order cl 320 val r = mlibClause.add cl r 321 val _ = chatting 5 andalso 322 chat ("\nrewrite set now:\n" ^ rewrs_to_string r ^ "\n") 323 val set = update_rewrites r set 324 in 325 (cl,set) 326 end; 327 328fun add cl set = 329 let 330 val SET {size = n, units = u, clauses = c, subsumers = s, literals = l, 331 equalities = e, subterms = p, ...} = set 332 fun f (x |-> l, net) = N.insert (l |-> x) net 333 fun g (x |-> t, net) = T.insert (t |-> x) net 334 val set = update_size (n + 1) set 335 val (cl,set) = add_rewr cl set 336 val set = update_units (add_unit cl u) set 337 val set = update_clauses (cl :: c) set 338 val set = update_subsumers (add_subsum cl s) set 339 val set = update_literals (foldl f l (largest_lits cl)) set 340 val set = update_equalities (foldl g e (largest_eqs cl)) set 341 val set = update_subterms (foldl g p (largest_tms cl)) set 342 val SET {size = n, units = u, clauses = c, subsumers = s, literals = l, 343 equalities = e, subterms = p, ...} = set 344 val _ = chatting 7 andalso 345 chat ("\nlargest_lits cl:\n" ^ 346 (PP.pp_to_string (!LINE_LENGTH) 347 (pp_list (pp_maplet (pp_pair pp_clause pp_int) pp_formula)) 348 (largest_lits cl)) ^ "\n") 349 val _ = chatting 6 andalso 350 chat ("\nliteral set now:\n" ^ literals_to_string l ^ "\n") 351 in 352 set 353 end; 354 355(* ------------------------------------------------------------------------- *) 356(* Derive consequences of a clause *) 357(* ------------------------------------------------------------------------- *) 358 359fun deduce set = 360 let 361 fun resolv ci (dj,acc) = 362 case total (RESOLVE ci) dj of NONE => acc | SOME l => l :: acc 363 364 fun resolvants r (ci |-> l, acc) = 365 foldl (resolv ci) acc (N.unify r (negate l)) 366 367 fun paramod cib djp acc = 368 case total (PARAMODULATE cib) djp of NONE => acc | SOME l => l :: acc 369 370 fun paramods_from p (cib |-> t, acc) = 371 foldl (uncurry (paramod cib)) acc (T.unify p t) 372 373 fun paramods_into e (cip |-> t, acc) = 374 foldl (uncurry (C paramod cip)) acc (T.unify e t) 375 in 376 fn cl => 377 let 378 val SET {literals = l, equalities = e, subterms = p, ...} = set 379 val res = [] 380 val res = foldl (resolvants l) res (largest_lits cl) 381 val res = foldl (paramods_from p) res (largest_eqs cl) 382 val res = foldl (paramods_into e) res (largest_tms cl) 383 in 384 rev res 385 end 386 handle Error _ => raise Bug "deduce: shouldn't fail" 387 end; 388 389(* ------------------------------------------------------------------------- *) 390(* Extract clauses that can be simplified *) 391(* ------------------------------------------------------------------------- *) 392 393local 394 fun clause_mem cl s = 395 let val {id, ...} = dest_clause cl in Intset.member (s,id) end; 396 397 fun clause_reducibles set = 398 let 399 val SET {rewrites = r, clauses = c, ...} = set 400 fun pred x = let val y = REWRITE r x in literals x <> literals y end 401 val d = List.filter pred c 402 in 403 Intset.addList (Intset.empty, map (#id o dest_clause) d) 404 end; 405 406 fun valid_rw l ro ord tm = 407 let 408 val sub = mlibMatch.match l tm 409 in 410 case ro of NONE => () | SOME r => 411 assert (mlibTermorder.compare ord (tm, term_subst sub r) = SOME GREATER) 412 (Error "rewr_reducibles: order violation") 413 end; 414 415 fun consider_rw l ro ((c,n,p),s) = 416 let 417 val {id, order, ...} = dest_clause c 418 in 419 if Intset.member (s,id) then s 420 else if not (can (valid_rw l ro order) (clause_subterm c n p)) then s 421 else Intset.add (s,id) 422 end; 423 424 fun rewr_reducibles set changed_redexes = 425 let 426 val SET {rewrites = r, clauses = c, subterms = p, ...} = set 427 428 fun pk i = 429 case peek r i of SOME x => x 430 | NONE => raise Bug "rewr_reducibles: vanishing rewrite" 431 432 fun red l ro s = foldl (consider_rw l ro) s (T.matched p l) 433 434 fun reds (i,s) = 435 case pk i of 436 ((l,r),mlibRewrite.LtoR) => red l NONE s 437 | ((l,r),mlibRewrite.RtoL) => red r NONE s 438 | ((l,r),mlibRewrite.Both) => red l (SOME r) (red r (SOME l) s) 439 440 fun unchanged i th = 441 case peek r i of NONE => false 442 | SOME (l_r,_) => l_r = mlibThm.dest_unit_eq th 443 444 fun mk_init_id (cl,(s,s')) = 445 case total dest_rewr cl of NONE => (s,s') 446 | SOME (i,th) => 447 (Intset.add (s,i), if unchanged i th then Intset.add (s',i) else s') 448 449 val (s_init,s_id) = foldl mk_init_id (Intset.empty,Intset.empty) c 450 451 fun quick i = snd (pk i) <> mlibRewrite.Both 452 453 val changed_redexes = op@ (List.partition quick changed_redexes) 454 in 455 Intset.difference (foldl reds s_init changed_redexes, s_id) 456 end; 457 458 fun reducibles set l = 459 if not (chatting 4) then 460 if ssize set <= length l then clause_reducibles set 461 else rewr_reducibles set l 462 else 463 let 464 val SET {clauses = c, rewrites = r, ...} = set 465 fun pk i = 466 case List.find (fn cl => #id (dest_clause cl) = i) c of SOME cl => cl 467 | NONE => raise Bug "reducibles: not a clause" 468 fun i_to_string f = 469 to_string (pp_list pp_clause) o map (f o pk) o Intset.listItems 470 val _ = chat "finding rewritable clauses in the clause set\n" 471 val clause_i = clause_reducibles set 472 val rewr_i = rewr_reducibles set l 473 val () = 474 if Intset.equal (clause_i,rewr_i) then () else 475 (print ("clause_reducibles = " ^ intset_to_string clause_i ^ "\n" ^ 476 i_to_string I clause_i ^ " -->\n" ^ 477 i_to_string (REWRITE r) clause_i ^ "\n" ^ 478 "rewr_reducibles = " ^ intset_to_string rewr_i ^ "\n" ^ 479 i_to_string I rewr_i ^ " -->\n" ^ 480 i_to_string (REWRITE r) rewr_i ^ "\n"); 481 raise Bug "purge_reducibles: rewr <> clause") 482 in 483 rewr_i 484 end; 485 486 fun purge ns set = 487 let 488 fun pred cl = not (clause_mem cl ns) 489 val SET {clauses = c, subsumers = s, literals = l, 490 equalities = e, subterms = p, ...} = set 491 val c = List.filter pred c 492 val set = update_clauses c set 493 val set = update_size (length c) set 494 val set = update_subsumers (S.filter pred s) set 495 val set = update_literals (N.filter (pred o fst) l) set 496 val set = update_equalities (T.filter (pred o #1) e) set 497 val set = update_subterms (T.filter (pred o #1) p) set 498 in 499 set 500 end; 501in 502 fun purge_reducibles (set as SET {rewrites = r, ...}) = 503 if reduced r then ([],set) else 504 let 505 val _ = chatting 2 andalso chat "=" 506 val _ = chatting 4 andalso chat "\ninter-reducing the clause set\n" 507 val (r,l) = mlibClause.reduce r 508 val set = update_rewrites r set 509 val i = reducibles set l 510 val _ = chatting 2 andalso chat (int_to_string (Intset.numItems i)) 511 in 512 if Intset.numItems i = 0 then ([],set) else 513 let 514 val SET {clauses = c, ...} = set 515 val cls = List.filter (fn cl => clause_mem cl i) c 516 val cls = map (REWRITE r) cls 517 val set = purge i set 518 in 519 (cls,set) 520 end 521 end 522 handle Error _ => raise Bug "purge_reducibles: shouldn't fail"; 523end; 524 525(* ------------------------------------------------------------------------- *) 526(* Initialize derived clauses *) 527(* ------------------------------------------------------------------------- *) 528 529local 530 fun utility cl = 531 case length (literals cl) of 0 => ~1 532 | 1 => if is_rewr cl then 0 else 1 533 | n => n; 534 535 val utilitywise = Int.compare; 536 537 fun is_subsumption (parm : parameters) = 538 #subsumption (#prefactoring parm) orelse #subsumption (#postfactoring parm); 539 540 fun ins (parm : parameters) cl (cls,set,subs) = 541 let 542 val (cl,set) = add_rewr cl set 543 val set = update_units (add_unit cl (units set)) set 544 val subs = if is_subsumption parm then add_subsum cl subs else subs 545 in 546 (cl :: cls, set, subs) 547 end; 548 549 fun quality (parm : parameters) post (_,s,x) = 550 let 551 val {subsumption, simplification, splitting} = 552 if post then #postfactoring parm else #prefactoring parm 553 val rw = 554 case simplification of 0 => I | 1 => qsimplify s | _ => simplify s 555 val sb = if subsumption then ofilt (not o subsum x) else I 556 val sp = if splitting then List.concat o map split else I 557 in 558 sp o olist o sb o strengthen s o rw 559 end; 560 561 fun fac1 parm (cl,acc) = 562 foldl (fn (cl,acc) => ins parm cl acc) acc (quality parm true acc cl); 563 564 fun facl parm (cl,acc) = 565 foldl (fn (cl,acc) => foldl (fac1 parm) (ins parm cl acc) (FACTOR cl)) acc 566 (quality parm false acc cl); 567 568 fun factor' acc set [] = (rev acc, set) 569 | factor' acc set cls = 570 let 571 val SET {parm = (_,z), subsumers = subs, ...} = set 572 val cls = sort_map utility utilitywise cls 573 val (cls,set,_) = foldl (facl z) ([],set,subs) cls 574 val (cls',set) = purge_reducibles set 575 in 576 factor' (cls @ acc) set cls' 577 end; 578in 579 fun factor cls set = 580 let 581 val _ = chatting 2 andalso chat ("-" ^ int_to_string (length cls)) 582 val res as (cls,_) = factor' [] set cls 583 val _ = chatting 1 andalso chat ("+" ^ int_to_string (length cls)) 584 in 585 res 586 end 587 handle Error _ => raise Bug "mlibClauseset.initialize: shouldn't fail"; 588end; 589 590(* ------------------------------------------------------------------------- *) 591(* Pretty-printing *) 592(* ------------------------------------------------------------------------- *) 593 594val pp_clauseset = pp_bracket "C<" ">" (pp_map ssize pp_int); 595 596(* ------------------------------------------------------------------------- *) 597(* Rebinding for signature *) 598(* ------------------------------------------------------------------------- *) 599 600val size = ssize; 601 602(* Quick testing 603quotation := true; (* OK *) 604installPP pp_formula; 605installPP pp_term; 606installPP pp_subst; 607installPP pp_thm; 608val th = AXIOM (map parse [`p(3,x,v)`, `q(x)`, `p(3,x,z)`]); 609val th' = AXIOM (map parse [`~p(3,f(y),w)`, `~q(y)`, `~p(3,f(y),4)`]); 610try (resolve_from (0,th)) (0,th'); 611try (resolve_from (2,th)) (0,th'); 612try (resolve_from (0,th)) (2,th'); 613try (resolve_from (2,th)) (2,th'); 614val r = add_literal th' empty_literals; 615map #res (find_resolvants r th); 616*) 617 618end 619