1(* ========================================================================= *) 2(* CLAUSE = ID + THEOREM + CONSTRAINTS *) 3(* Copyright (c) 2002-2004 Joe Hurd. *) 4(* ========================================================================= *) 5 6(* 7app load ["Moscow", "mlibTerm", "mlibSubst", "mlibThm", "mlibUnits", "mlibTermorder"]; 8*) 9 10(* 11*) 12structure mlibClause :> mlibClause = 13struct 14 15infix ## |->; 16 17open mlibUseful mlibTerm mlibMatch; 18 19structure S = Binaryset; local open Binaryset in end; 20structure T = mlibTermorder; local open mlibTermorder in end; 21 22type subst = mlibSubst.subst; 23type thm = mlibThm.thm; 24type units = mlibUnits.units; 25type termorder = T.termorder; 26 27val |<>| = mlibSubst.|<>|; 28val term_subst = mlibSubst.term_subst; 29val formula_subst = mlibSubst.formula_subst; 30 31(* ------------------------------------------------------------------------- *) 32(* Chatting *) 33(* ------------------------------------------------------------------------- *) 34 35val module = "mlibClause"; 36val _ = add_trace {module = module, alignment = I} 37fun chatting l = tracing {module = module, level = l}; 38fun chat s = (trace s; true) 39 40(* ------------------------------------------------------------------------- *) 41(* Parameters *) 42(* ------------------------------------------------------------------------- *) 43 44type parameters = 45 {term_order : bool, 46 literal_order : bool, 47 order_stickiness : int, 48 termorder_parm : mlibTermorder.parameters}; 49 50type 'a parmupdate = ('a -> 'a) -> parameters -> parameters; 51 52val defaults = 53 {term_order = true, 54 literal_order = false, 55 order_stickiness = 0, 56 termorder_parm = T.defaults}; 57 58fun update_term_order f (parm : parameters) : parameters = 59 let 60 val {term_order = t, literal_order = l, 61 order_stickiness = s, termorder_parm = x} = parm 62 in 63 {term_order = f t, literal_order = l, 64 order_stickiness = s, termorder_parm = x} 65 end; 66 67fun update_literal_order f (parm : parameters) : parameters = 68 let 69 val {term_order = t, literal_order = l, 70 order_stickiness = s, termorder_parm = x} = parm 71 in 72 {term_order = t, literal_order = f l, 73 order_stickiness = s, termorder_parm = x} 74 end; 75 76fun update_order_stickiness f (parm : parameters) : parameters = 77 let 78 val {term_order = t, literal_order = l, 79 order_stickiness = s, termorder_parm = x} = parm 80 in 81 {term_order = t, literal_order = l, 82 order_stickiness = f s, termorder_parm = x} 83 end; 84 85fun update_termorder_parm f (parm : parameters) : parameters = 86 let 87 val {term_order = t, literal_order = l, 88 order_stickiness = s, termorder_parm = x} = parm 89 in 90 {term_order = t, literal_order = l, 91 order_stickiness = s, termorder_parm = f x} 92 end; 93 94(* ------------------------------------------------------------------------- *) 95(* Helper functions *) 96(* ------------------------------------------------------------------------- *) 97 98fun ocons (SOME x) l = x :: l | ocons NONE l = l; 99 100val new_id = new_int; 101 102fun dest_refl lit = 103 let 104 val (x,y) = dest_eq lit 105 val () = assert (x = y) (Error "dest_refl") 106 in 107 x 108 end; 109 110val is_refl = can dest_refl; 111 112fun dest_peq lit = (I ## dest_eq) (dest_literal lit); 113fun mk_peq (s,xy) = mk_literal (s, mk_eq xy); 114 115fun psym lit = 116 let 117 val (s,(x,y)) = dest_peq lit 118 val () = assert (x <> y) (Error "psym: refl") 119 in 120 mk_peq (s,(y,x)) 121 end; 122 123(* ------------------------------------------------------------------------- *) 124(* Objects are either predicates or sides of (dis)equations *) 125(* ------------------------------------------------------------------------- *) 126 127datatype obj = Pred of term | Eq of term; 128 129fun obj_subst sub (Pred tm) = Pred (term_subst sub tm) 130 | obj_subst sub (Eq tm) = Eq (term_subst sub tm); 131 132fun dest_pred a = [Pred (dest_atom a)]; 133 134fun dest_eq_refl (x,y) = if x = y then [Eq x] else [Eq x, Eq y]; 135 136fun object_map f g l = 137 let val a = literal_atom l 138 in case total dest_eq a of NONE => f a | SOME x_y => g x_y 139 end; 140 141local val break = object_map dest_pred dest_eq_refl; 142in val objects = foldl (fn (h,t) => break h @ t) []; 143end; 144 145(* ------------------------------------------------------------------------- *) 146(* mlibTerm and literal ordering *) 147(* ------------------------------------------------------------------------- *) 148 149fun tm_order (parm : parameters) lrs c = 150 let val c' = T.add_leqs lrs c 151 in if #order_stickiness parm <= 0 then c else c' 152 end; 153 154fun term_order (parm : parameters) l r c = 155 if l = r then raise Error "term_order: refl" 156 else if #term_order parm then tm_order parm [(r,l)] c 157 else c; 158 159local 160 fun f (Eq x) (Eq y) = SOME (x,y) 161 | f (Eq x) (Pred y) = NONE 162 | f (Pred x) (Eq y) = raise Error "obj_order: Pred > Eq" 163 | f (Pred x) (Pred y) = SOME (x,y); 164in 165 fun obj_order {literal_order = false, ...} _ _ c = c 166 | obj_order p xs ys c = tm_order p (List.mapPartial I (cartwith f ys xs)) c; 167end; 168 169fun lit_order {literal_order = false, ...} _ _ c = c 170 | lit_order p l ls c = 171 let val xs = object_map dest_pred dest_eq_refl l 172 in obj_order p xs (objects ls) c 173 end; 174 175(* ------------------------------------------------------------------------- *) 176(* Generic constraint interface *) 177(* ------------------------------------------------------------------------- *) 178 179fun no_constraints ({termorder_parm = p, ...} : parameters) = T.empty p; 180 181fun constraint_vars to = T.vars to; 182 183fun constraint_subst sub to = T.subst sub to; 184 185fun merge_constraints sub to1 to2 = 186 (T.merge (T.subst sub to1) (T.subst sub to2), sub); 187 188fun constraint_consistent (p : parameters) to = 189 case T.consistent to of 190 SOME to => if #order_stickiness p <= 1 then no_constraints p else to 191 | NONE => 192 (chatting 1 andalso 193 chat ("merge_orderings: resulting termorder is inconsistent:\n" ^ 194 PP.pp_to_string (!LINE_LENGTH) T.pp_termorder to); 195 raise Error "consistent: inconsistent orderings"); 196 197fun constraint_subsumes sub to1 to2 = 198 case total (T.subst sub) to1 of NONE => false 199 | SOME to1 => T.subsumes to1 to2; 200 201fun pp_constraints to = T.pp_termorder to; 202 203(* ------------------------------------------------------------------------- *) 204(* mlibClauses *) 205(* ------------------------------------------------------------------------- *) 206 207type bits = {parm : parameters, id : int, thm : thm, order : termorder}; 208 209datatype clause = CL of parameters * int * thm * termorder * derivation 210and derivation = 211 Axiom 212| mlibResolution of clause * clause 213| Paramodulation of clause * clause 214| Factor of clause; 215 216fun mk_clause p th = CL (p, new_id (), th, no_constraints p, Axiom); 217 218fun dest_clause (CL (p,i,th,to,_)) = {parm = p, id = i, thm = th, order = to}; 219 220fun derivation (CL (_,_,_,_,d)) = d; 221 222val literals = mlibThm.clause o #thm o dest_clause; 223 224fun free_vars cl = 225 FVL (constraint_vars (#order (dest_clause cl))) (literals cl); 226 227val is_empty = null o literals; 228 229fun dest_rewr cl = 230 let 231 val {parm, thm, id, ...} = dest_clause cl 232 val () = assert (#term_order parm) (Error "dest_rewr: no rewrs") 233 val (x,y) = mlibThm.dest_unit_eq thm 234 val () = assert (x <> y) (Error "dest_rewr: refl") 235 in 236 (id,thm) 237 end; 238 239val is_rewr = can dest_rewr; 240 241fun rebrand parm (CL (p,i,th,_,d)) = CL (parm, i, th, no_constraints parm, d); 242 243(* ------------------------------------------------------------------------- *) 244(* Pretty-printing. *) 245(* ------------------------------------------------------------------------- *) 246 247val show_id = ref false; 248 249val show_constraint = ref false; 250 251local 252 val pp_it = pp_pair pp_int mlibThm.pp_thm; 253 val pp_tc = pp_pair mlibThm.pp_thm pp_constraints; 254 val pp_itc = pp_triple pp_int mlibThm.pp_thm pp_constraints; 255 fun f false false = pp_map (fn CL (_,_,th,_,_) => th) mlibThm.pp_thm 256 | f true false = pp_map (fn CL (_,i,th,_,_) => (i,th)) pp_it 257 | f false true = pp_map (fn CL (_,_,th,c,_) => (th,c)) pp_tc 258 | f true true = pp_map (fn CL (_,i,th,c,_) => (i,th,c)) pp_itc; 259in 260 fun pp_clause cl = f (!show_id) (!show_constraint) cl; 261end; 262 263(* ------------------------------------------------------------------------- *) 264(* Using ordering constraints to cut down the set of possible inferences *) 265(* ------------------------------------------------------------------------- *) 266 267local 268 fun fail _ = raise Error "gen_largest_lits: fail"; 269 270 fun gen_largest_lits f g (CL (p,i,th,c,d)) = 271 let 272 val lits = mlibThm.clause th 273 val objs = objects lits 274 fun collect (n,l) = 275 let val xs = object_map f g l 276 in (CL (p, i, th, obj_order p xs objs c, d), n) |-> l 277 end 278 in 279 List.mapPartial (total collect) (enumerate 0 lits) 280 end; 281in 282 val largest_noneq_lits = gen_largest_lits dest_pred fail; 283 val largest_refl_lits = gen_largest_lits fail dest_eq_refl; 284 val largest_lits = gen_largest_lits dest_pred dest_eq_refl; 285end; 286 287local 288 fun gen_largest_eqs dest (CL (p,i,th,c,d)) = 289 let 290 val lits = mlibThm.clause th 291 val objs = objects lits 292 fun f ((n,l),acc) = 293 case total dest l of 294 NONE => acc 295 | SOME (x,y) => 296 let 297 fun g b z = (CL (p,i,th,obj_order p [Eq z] objs c,d), n, b) |-> z 298 in 299 if x = y then acc 300 else ocons (total (g false) y) (ocons (total (g true) x) acc) 301 end 302 in 303 foldl f [] (enumerate 0 lits) 304 end; 305in 306 val largest_eqs = gen_largest_eqs dest_eq; 307 val largest_peqs = gen_largest_eqs (snd o dest_peq); 308end; 309 310local 311 fun harvest (c,i) = 312 let 313 fun f ((_ |-> Var _), acc) = acc 314 | f ((_ |-> (Fn (":", [Var _, _]))), acc) = acc 315 | f ((p |-> (t as Fn _)), acc) = ((c,i,p) |-> t) :: acc 316 in 317 C (foldl f) 318 end; 319in 320 fun largest_tms (CL (p,i,th,c,d)) = 321 let 322 val lits = mlibThm.clause th 323 val objs = objects lits 324 fun ok x = total (obj_order p x objs) c 325 fun collect ((n,l),acc) = 326 let 327 fun inc c = harvest (CL (p,i,th,c,d), n) 328 fun f a = 329 (case ok (dest_pred a) of NONE => acc 330 | SOME c => inc c (literal_subterms a) acc) 331 fun g (x,y) = 332 if x = y then acc else 333 let 334 val acc = 335 case ok [Eq y] of NONE => acc 336 | SOME c => inc c (subterms [1] y) acc 337 val acc = 338 case ok [Eq x] of NONE => acc 339 | SOME c => inc c (subterms [0] x) acc 340 in 341 acc 342 end 343 in 344 object_map f g l 345 end 346 in 347 foldl collect [] (enumerate 0 lits) 348 end; 349end; 350 351fun drop_order (cl as CL (p,i,th,c,d)) = 352 if T.null c then cl else CL (p, i, th, no_constraints p, d); 353 354(* ------------------------------------------------------------------------- *) 355(* Subsumption *) 356(* ------------------------------------------------------------------------- *) 357 358fun subsumes (cl as CL (_,_,th,c,_)) (cl' as CL (_,_,th',c',_)) = 359 let val subs = mlibSubsume.subsumes1' (mlibThm.clause th) (mlibThm.clause th') 360 in List.exists (fn sub => constraint_subsumes sub c c') subs 361 end; 362 363(* ------------------------------------------------------------------------- *) 364(* mlibClause rewriting *) 365(* ------------------------------------------------------------------------- *) 366 367datatype rewrs = REWR of parameters * mlibRewrite.rewrs; 368 369fun empty (parm as {termorder_parm = p, ...}) = 370 REWR (parm, mlibRewrite.empty (mlibTermorder.compare (mlibTermorder.empty p))); 371 372fun size (REWR (_,r)) = mlibRewrite.size r; 373 374fun peek (REWR (p,r)) i = 375 case mlibRewrite.peek r i of NONE => NONE 376 | SOME (th,ort) => SOME (mlibThm.dest_unit_eq th, ort); 377 378fun add cl rewrs = 379 let 380 val (i,th) = dest_rewr cl 381 val REWR (parm,rw) = rewrs 382 in 383 REWR (parm, mlibRewrite.add (i,th) rw) 384 end; 385 386fun reduce (REWR (p,r)) = 387 let val (r,l) = mlibRewrite.reduce' r in (REWR (p,r), l) end; 388 389fun reduced (REWR (_,r)) = mlibRewrite.reduced r; 390 391val pp_rewrs = pp_map (fn REWR (_,r) => r) mlibRewrite.pp_rewrs; 392 393(* ------------------------------------------------------------------------- *) 394(* Simplifying rules: these preserve the clause id *) 395(* ------------------------------------------------------------------------- *) 396 397fun INST sub (cl as CL (p,i,th,c,d)) = 398 if mlibSubst.null sub then cl 399 else CL (p, i, mlibThm.INST sub th, constraint_subst sub c, d); 400 401fun FRESH_VARS cl = 402 let 403 val fvs = free_vars cl 404 val gvs = new_vars (length fvs) 405 val sub = mlibSubst.from_maplets (zipwith (curry op|->) fvs gvs) 406 in 407 INST sub cl 408 end; 409 410local 411 fun match_occurs cl l r = 412 let 413 val v = 414 case l of Var v => v 415 | Fn (":", [Var v, _]) => v 416 | _ => raise Error "match_occurs: not a variable" 417 val () = assert (not (mem v (FVT r))) (Error "match_occurs") 418 val sub = match l r 419 in 420 INST sub cl 421 end; 422 423 fun dest_neq cl lit = 424 let 425 val (l,r) = dest_eq (dest_neg lit) 426 val () = assert (l <> r) (Error "dest_neq: reflexive") 427 in 428 case total (match_occurs cl l) r of SOME cl => cl 429 | NONE => match_occurs cl r l 430 end; 431 432 fun neq_simp1 cl = first (total (dest_neq cl)) (literals cl); 433 434 fun neq_simp cl = case neq_simp1 cl of NONE => cl | SOME cl => neq_simp cl; 435 436 fun eq_factor (CL (p,i,th,c,d)) = CL (p, i, mlibThm.EQ_FACTOR th, c, d); 437in 438 fun NEQ_VARS cl = 439 (case neq_simp1 cl of NONE => cl | SOME cl => eq_factor (neq_simp cl)) 440 handle Error _ => raise Bug "NEQ_VARS: shouldn't fail"; 441end; 442 443fun DEMODULATE units (cl as CL (p,i,th,c,d)) = 444 let 445 val lits = mlibThm.clause th 446 val th = mlibUnits.demod units th 447 in 448 if mlibThm.clause th = lits then cl else CL (p,i,th,c,d) 449 end; 450 451local 452 fun mk_ord true c = T.compare c | mk_ord false _ = K NONE; 453 454 fun rewr r ord th = mlibThm.EQ_FACTOR (mlibRewrite.rewrite r ord th) 455 456 fun rewrite0 ord r (CL (p,i,th,c,d)) = 457 case mlibRewrite.peek r i of SOME (th,_) => CL (p,i,th,c,d) 458 | NONE => CL (p, i, rewr r (mk_ord ord c) (i,th), c, d); 459 460 fun GEN_REWRITE _ (REWR ({term_order = false, ...}, _)) cl = cl 461 | GEN_REWRITE ord (REWR (_,rw)) cl = rewrite0 ord rw cl; 462in 463 fun REWRITE rws cl = 464 if not (chatting 1) then GEN_REWRITE true rws cl else 465 let 466 val res = GEN_REWRITE true rws cl 467 val _ = literals cl <> literals res andalso chat 468 ("\nREWRITE: " ^ PP.pp_to_string 60 pp_clause cl ^ 469 "\nto get: " ^ PP.pp_to_string 60 pp_clause res ^ "\n") 470 in 471 res 472 end 473 handle Error _ => raise Bug "mlibClause.REWRITE: shouldn't fail"; 474 475 fun QREWRITE rws cl = 476 if not (chatting 1) then GEN_REWRITE false rws cl else 477 let 478 val res = GEN_REWRITE false rws cl 479 val _ = literals cl <> literals res andalso chat 480 ("\nQREWRITE: " ^ PP.pp_to_string 60 pp_clause cl ^ 481 "\nto get: " ^ PP.pp_to_string 60 pp_clause res ^ "\n") 482 in 483 res 484 end 485 handle Error _ => raise Bug "mlibClause.QREWRITE: shouldn't fail"; 486end; 487 488(* ------------------------------------------------------------------------- *) 489(* Ordered resolution and paramodulation: these generate new clause ids *) 490(* ------------------------------------------------------------------------- *) 491 492(* 493Factoring. 494 495This implementation tries hard to keep the number of generated clauses 496to a minimum, because performing simplification and subsumption 497testing on each new clause is the bottleneck of the prover. 498 499For each largest literal l in the input clause, we iterate through the 500set of all substitutions s that unify l with at least one other 501literal. Next apply the substitution s to the clause, and mark all the 502literals that are now equal to l with a X, and the others with a -, 503eg. 504 505X - - X - - - X - 506 507This is the 'hit list' for the new clause generated by (l,s). If we 508ever see the same hit list for another new clause C generated by an 509alternative (l',s'), then we can safely discard C immediately (since 510(i) the substitution s' must be equal to s, and (ii) the ordering 511constraints generated by setting l' to be a largest literal will be 512identical to those generated by l). 513 514With equality the situation becomes slightly more complicated. Now we 515have two kinds of hits: one as before (called an Id hit); and one for 516when we get a hit by applying symmetry to the (dis)equality literal 517(called a Sym hit). So now we get a list like: 518 519Sym - - Id - - - Sym - 520 521But this gives the same new clause as the hit list 522 523Id - - Sym - - - Id - 524 525so we always normalize the hit list by flipping Ids and Syms (if 526necessary) to make the first hit an Id. 527 528Unfortunately, this quotient function loses too much information 529because of ordering constraints. A (dis)equality literal M = N becomes 530a largest literal because one of M or N is a largest object in the 531clause. If M was the largest, then keep the first hit an Id. If N was 532the largest, then make the first hit a Sym. If in the previous step we 533had to flip all the hits to make the first hit an Id, then flip this 534first hit too. 535*) 536 537local 538 datatype hit = Id | Sym | Miss; 539 fun hit_compare (Id,Id) = EQUAL | hit_compare (Id,_) = LESS 540 | hit_compare (_,Id) = GREATER | hit_compare (Sym,Sym) = EQUAL 541 | hit_compare (Sym,_) = LESS | hit_compare (_,Sym) = GREATER 542 | hit_compare (Miss,Miss) = EQUAL; 543 fun hit _ [] _ = Miss | hit a (h :: t) x = if h = x then a else hit Sym t x; 544 fun first_hit true = Id | first_hit false = Sym; 545 fun flip_hit Id = Sym | flip_hit Sym = Id | flip_hit Miss = Miss; 546 fun norm_hits _ [] = raise Bug "norm_hits" 547 | norm_hits lr (Miss :: rest) = norm_hits lr rest 548 | norm_hits lr (Id :: rest) = first_hit lr :: rest 549 | norm_hits lr (Sym :: rest) = map flip_hit (first_hit lr :: rest); 550 fun calc_hits lr targs lits = norm_hits lr (map (hit Id targs) lits); 551 552 val empty = (S.empty (lex_list_order hit_compare), []); 553 fun is_new h (s,_) = not (S.member (s,h)); 554 fun insert (h,c) (s,l) = (S.add (s,h), ocons c l); 555 fun finish (_,l) = l; 556 557 fun assimilate s l l' = 558 let 559 val s' = unify_literals s l l' 560 val () = assert (formula_subst s l <> formula_subst s l') 561 (Error "assimilate: already included") 562 in 563 s' 564 end; 565 566 fun FAC x lits sub cl = 567 let 568 val CL (p,_,th,c,_) = INST sub cl 569 val th = mlibThm.EQ_FACTOR th 570 val c = obj_order p [obj_subst sub x] (objects lits) c 571 val c = constraint_consistent p c 572 in 573 CL (p, new_id (), th, c, Factor cl) 574 end; 575 576 fun final cl sub lr x targs = 577 let 578 fun f acc = 579 let 580 val lits = map (formula_subst sub) (literals cl) 581 val () = assert (List.all (not o is_refl) lits) (Error "final: refl") 582 val hits = calc_hits lr (map (formula_subst sub) targs) lits 583 val () = assert (is_new hits acc) (Error "final: already seen") 584 in 585 (hits, total (FAC x lits sub) cl) 586 end 587 in 588 fn acc => 589 if mlibSubst.null sub then acc 590 else case total f acc of SOME x => insert x acc | NONE => acc 591 end; 592 593 fun factor ((cl,n) |-> lit) = 594 let 595 val x = object_map (Pred o dest_atom) (fn _ => raise Bug "factor") lit 596 fun f [] acc = acc 597 | f ((s,[]) :: paths) acc = f paths (final cl s true x [lit] acc) 598 | f ((s, l :: ls) :: paths) acc = 599 let 600 val paths = (s,ls) :: paths 601 val paths = 602 case total (assimilate s l) lit of NONE => paths 603 | SOME s' => (s',ls) :: paths 604 in 605 f paths acc 606 end 607 in 608 f [(|<>|, List.drop (literals cl, n + 1))] 609 end; 610 611 fun factor_eq ((cl,n,b) |-> x) = 612 let 613 val x = Eq x 614 val lit = List.nth (literals cl, n) 615 val lit' = psym lit 616 fun f [] acc = acc 617 | f ((s,[]) :: paths) acc = f paths (final cl s b x [lit,lit'] acc) 618 | f ((s, l :: ls) :: paths) acc = 619 let 620 val paths = (s,ls) :: paths 621 val paths = 622 case total (assimilate s l) lit of NONE => paths 623 | SOME s' => (s',ls) :: paths 624 val paths = 625 case total (assimilate s l) lit' of NONE => paths 626 | SOME s' => (s',ls) :: paths 627 in 628 f paths acc 629 end 630 in 631 f [(|<>|, List.drop (literals cl, n + 1))] 632 end; 633 634 fun FACTOR' cl = 635 let 636 fun fac acc = foldl (uncurry factor) acc (largest_noneq_lits cl) 637 fun fac_eq acc = foldl (uncurry factor_eq) acc (largest_peqs cl) 638 in 639 finish (fac (fac_eq empty)) 640 end 641 handle Error _ => raise Bug "mlibClause.FACTOR: shouldn't fail"; 642in 643 fun FACTOR cl = 644 if not (chatting 1) then FACTOR' cl else 645 let 646 val res = FACTOR' cl 647 val _ = not (null res) andalso chat 648 ("\nFACTOR: " ^ PP.pp_to_string 60 pp_clause cl ^ 649 "\nto get: " ^ PP.pp_to_string 60 (pp_list pp_clause) res ^ "\n") 650 in 651 res 652 end; 653end; 654 655local 656 fun RESOLVE' (cl1 as CL (p,_,th1,c1,_), n1) (cl2 as CL (_,_,th2,c2,_), n2) = 657 let 658 val lit1 = List.nth (mlibThm.clause th1, n1) 659 val lit2 = List.nth (mlibThm.clause th2, n2) 660 val env = unify_literals |<>| lit1 (negate lit2) 661 val (c,env) = merge_constraints env c1 c2 662 val lit = mlibSubst.formula_subst env lit1 663 val th1 = mlibThm.INST env th1 664 val th2 = mlibThm.INST env th2 665 val th = mlibThm.EQ_FACTOR (mlibThm.RESOLVE lit th1 th2) 666 val c = lit_order p lit (mlibThm.clause th) c 667 val c = constraint_consistent p c 668 in 669 CL (p, new_id (), th, c, mlibResolution (cl1,cl2)) 670 end; 671in 672 fun RESOLVE arg1 arg2 = 673 if not (chatting 1) then RESOLVE' arg1 arg2 else 674 let 675 fun p res = chat 676 ("\nRESOLVE:\n" ^ 677 PP.pp_to_string 70 (pp_pair pp_clause pp_int) arg1 ^ "\n" ^ 678 PP.pp_to_string 70 (pp_pair pp_clause pp_int) arg2 ^ "\n" ^ 679 PP.pp_to_string 70 (pp_sum pp_clause pp_string) res ^ "\n") 680 val res = 681 RESOLVE' arg1 arg2 682 handle e as Error _ => (p (INR (report e)); raise e) 683 in 684 (p (INL res); res) 685 end; 686end; 687 688local 689 fun pick (0 :: _) (x,_) = x 690 | pick (1 :: _) (_,y) = y 691 | pick _ _ = raise Bug "into_obj: bad path"; 692 693 fun into_obj p = object_map (Pred o dest_atom) (Eq o pick p); 694 695 fun PARAMODULATE' (cl1,n1,lr1) (cl2,n2,p2) = 696 let 697 val CL (p,_,th1,c1,_) = cl1 698 val CL (_,_,th2,c2,_) = cl2 699 val lit1 = List.nth (mlibThm.clause th1, n1) 700 val lit2 = List.nth (mlibThm.clause th2, n2) 701 val (l1,r1) = (if lr1 then I else swap) (dest_eq lit1) 702 val t2 = literal_subterm p2 lit2 703 val env = unify |<>| l1 t2 704 val (c,env) = merge_constraints env c1 c2 705 val (l1,r1) = Df (mlibSubst.term_subst env) (l1,r1) 706 val c = term_order p l1 r1 c 707 val (lit1,lit2) = Df (mlibSubst.formula_subst env) (lit1,lit2) 708 val (th1,th2) = Df (mlibThm.INST env) (th1,th2) 709 val c = obj_order p [Eq l1] (objects (mlibThm.clause th1)) c 710 val c = obj_order p [into_obj p2 lit2] (objects (mlibThm.clause th2)) c 711 val c = constraint_consistent p c 712 val th = 713 let val eq_th = mlibThm.EQUALITY lit2 p2 r1 lr1 th2 714 in mlibThm.EQ_FACTOR (mlibThm.RESOLVE lit1 th1 eq_th) 715 end 716 handle Error _ => raise Bug "PARAMODULATE (rule): shouldn't fail" 717 in 718 CL (p, new_id (), th, c, Paramodulation (cl1,cl2)) 719 end; 720in 721 fun PARAMODULATE arg1 arg2 = 722 if not (chatting 1) then PARAMODULATE' arg1 arg2 else 723 let 724 fun p res = chat 725 ("\nPARAMODULATE:\n" ^ 726 PP.pp_to_string 70 (pp_triple pp_clause pp_int pp_bool) arg1 ^ "\n"^ 727 PP.pp_to_string 70 (pp_triple pp_clause pp_int (pp_list pp_int))arg2^ 728 "\n" ^ PP.pp_to_string 70 (pp_sum pp_clause pp_string) res ^ "\n") 729 val res = 730 PARAMODULATE' arg1 arg2 731 handle e as Error _ => (p (INR (report e)); raise e) 732 in 733 (p (INL res); res) 734 end; 735end; 736 737end 738