1(* ========================================================================= *) 2(* NORMALIZING FORMULAS *) 3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6structure Normalize :> Normalize = 7struct 8 9open Useful; 10 11(* ------------------------------------------------------------------------- *) 12(* Constants. *) 13(* ------------------------------------------------------------------------- *) 14 15val prefix = "FOFtoCNF"; 16 17val skolemPrefix = "skolem" ^ prefix; 18 19val definitionPrefix = "definition" ^ prefix; 20 21(* ------------------------------------------------------------------------- *) 22(* Storing huge real numbers as their log. *) 23(* ------------------------------------------------------------------------- *) 24 25datatype logReal = LogReal of real; 26 27fun compareLogReal (LogReal logX, LogReal logY) = 28 Real.compare (logX,logY); 29 30val zeroLogReal = LogReal ~1.0; 31 32val oneLogReal = LogReal 0.0; 33 34local 35 fun isZero logX = logX < 0.0; 36 37 (* Assume logX >= logY >= 0.0 *) 38 fun add logX logY = logX + Math.ln (1.0 + Math.exp (logY - logX)); 39in 40 fun isZeroLogReal (LogReal logX) = isZero logX; 41 42 fun multiplyLogReal (LogReal logX) (LogReal logY) = 43 if isZero logX orelse isZero logY then zeroLogReal 44 else LogReal (logX + logY); 45 46 fun addLogReal (lx as LogReal logX) (ly as LogReal logY) = 47 if isZero logX then ly 48 else if isZero logY then lx 49 else if logX < logY then LogReal (add logY logX) 50 else LogReal (add logX logY); 51 52 fun withinRelativeLogReal logDelta (LogReal logX) (LogReal logY) = 53 isZero logX orelse 54 (not (isZero logY) andalso logX < logY + logDelta); 55end; 56 57fun toStringLogReal (LogReal logX) = Real.toString logX; 58 59(* ------------------------------------------------------------------------- *) 60(* Counting the clauses that would be generated by conjunctive normal form. *) 61(* ------------------------------------------------------------------------- *) 62 63val countLogDelta = 0.01; 64 65datatype count = Count of {positive : logReal, negative : logReal}; 66 67fun countCompare (count1,count2) = 68 let 69 val Count {positive = p1, negative = _} = count1 70 and Count {positive = p2, negative = _} = count2 71 in 72 compareLogReal (p1,p2) 73 end; 74 75fun countNegate (Count {positive = p, negative = n}) = 76 Count {positive = n, negative = p}; 77 78fun countLeqish count1 count2 = 79 let 80 val Count {positive = p1, negative = _} = count1 81 and Count {positive = p2, negative = _} = count2 82 in 83 withinRelativeLogReal countLogDelta p1 p2 84 end; 85 86(*MetisDebug 87fun countEqualish count1 count2 = 88 countLeqish count1 count2 andalso 89 countLeqish count2 count1; 90 91fun countEquivish count1 count2 = 92 countEqualish count1 count2 andalso 93 countEqualish (countNegate count1) (countNegate count2); 94*) 95 96val countTrue = Count {positive = zeroLogReal, negative = oneLogReal}; 97 98val countFalse = Count {positive = oneLogReal, negative = zeroLogReal}; 99 100val countLiteral = Count {positive = oneLogReal, negative = oneLogReal}; 101 102fun countAnd2 (count1,count2) = 103 let 104 val Count {positive = p1, negative = n1} = count1 105 and Count {positive = p2, negative = n2} = count2 106 val p = addLogReal p1 p2 107 and n = multiplyLogReal n1 n2 108 in 109 Count {positive = p, negative = n} 110 end; 111 112fun countOr2 (count1,count2) = 113 let 114 val Count {positive = p1, negative = n1} = count1 115 and Count {positive = p2, negative = n2} = count2 116 val p = multiplyLogReal p1 p2 117 and n = addLogReal n1 n2 118 in 119 Count {positive = p, negative = n} 120 end; 121 122(* Whether countXor2 is associative or not is an open question. *) 123 124fun countXor2 (count1,count2) = 125 let 126 val Count {positive = p1, negative = n1} = count1 127 and Count {positive = p2, negative = n2} = count2 128 val p = addLogReal (multiplyLogReal p1 p2) (multiplyLogReal n1 n2) 129 and n = addLogReal (multiplyLogReal p1 n2) (multiplyLogReal n1 p2) 130 in 131 Count {positive = p, negative = n} 132 end; 133 134fun countDefinition body_count = countXor2 (countLiteral,body_count); 135 136val countToString = 137 let 138 val rToS = toStringLogReal 139 in 140 fn Count {positive = p, negative = n} => 141 "(+" ^ rToS p ^ ",-" ^ rToS n ^ ")" 142 end; 143 144val ppCount = Print.ppMap countToString Print.ppString; 145 146(* ------------------------------------------------------------------------- *) 147(* A type of normalized formula. *) 148(* ------------------------------------------------------------------------- *) 149 150datatype formula = 151 True 152 | False 153 | Literal of NameSet.set * Literal.literal 154 | And of NameSet.set * count * formula Set.set 155 | Or of NameSet.set * count * formula Set.set 156 | Xor of NameSet.set * count * bool * formula Set.set 157 | Exists of NameSet.set * count * NameSet.set * formula 158 | Forall of NameSet.set * count * NameSet.set * formula; 159 160fun compare f1_f2 = 161 if Portable.pointerEqual f1_f2 then EQUAL 162 else 163 case f1_f2 of 164 (True,True) => EQUAL 165 | (True,_) => LESS 166 | (_,True) => GREATER 167 | (False,False) => EQUAL 168 | (False,_) => LESS 169 | (_,False) => GREATER 170 | (Literal (_,l1), Literal (_,l2)) => Literal.compare (l1,l2) 171 | (Literal _, _) => LESS 172 | (_, Literal _) => GREATER 173 | (And (_,_,s1), And (_,_,s2)) => Set.compare (s1,s2) 174 | (And _, _) => LESS 175 | (_, And _) => GREATER 176 | (Or (_,_,s1), Or (_,_,s2)) => Set.compare (s1,s2) 177 | (Or _, _) => LESS 178 | (_, Or _) => GREATER 179 | (Xor (_,_,p1,s1), Xor (_,_,p2,s2)) => 180 (case boolCompare (p1,p2) of 181 LESS => LESS 182 | EQUAL => Set.compare (s1,s2) 183 | GREATER => GREATER) 184 | (Xor _, _) => LESS 185 | (_, Xor _) => GREATER 186 | (Exists (_,_,n1,f1), Exists (_,_,n2,f2)) => 187 (case NameSet.compare (n1,n2) of 188 LESS => LESS 189 | EQUAL => compare (f1,f2) 190 | GREATER => GREATER) 191 | (Exists _, _) => LESS 192 | (_, Exists _) => GREATER 193 | (Forall (_,_,n1,f1), Forall (_,_,n2,f2)) => 194 (case NameSet.compare (n1,n2) of 195 LESS => LESS 196 | EQUAL => compare (f1,f2) 197 | GREATER => GREATER); 198 199val empty = Set.empty compare; 200 201val singleton = Set.singleton compare; 202 203local 204 fun neg True = False 205 | neg False = True 206 | neg (Literal (fv,lit)) = Literal (fv, Literal.negate lit) 207 | neg (And (fv,c,s)) = Or (fv, countNegate c, neg_set s) 208 | neg (Or (fv,c,s)) = And (fv, countNegate c, neg_set s) 209 | neg (Xor (fv,c,p,s)) = Xor (fv, c, not p, s) 210 | neg (Exists (fv,c,n,f)) = Forall (fv, countNegate c, n, neg f) 211 | neg (Forall (fv,c,n,f)) = Exists (fv, countNegate c, n, neg f) 212 213 and neg_set s = Set.foldl neg_elt empty s 214 215 and neg_elt (f,s) = Set.add s (neg f); 216in 217 val negate = neg; 218 219 val negateSet = neg_set; 220end; 221 222fun negateMember x s = Set.member (negate x) s; 223 224local 225 fun member s x = negateMember x s; 226in 227 fun negateDisjoint s1 s2 = 228 if Set.size s1 < Set.size s2 then not (Set.exists (member s2) s1) 229 else not (Set.exists (member s1) s2); 230end; 231 232fun polarity True = true 233 | polarity False = false 234 | polarity (Literal (_,(pol,_))) = not pol 235 | polarity (And _) = true 236 | polarity (Or _) = false 237 | polarity (Xor (_,_,pol,_)) = pol 238 | polarity (Exists _) = true 239 | polarity (Forall _) = false; 240 241(*MetisDebug 242val polarity = fn f => 243 let 244 val res1 = compare (f, negate f) = LESS 245 val res2 = polarity f 246 val _ = res1 = res2 orelse raise Bug "polarity" 247 in 248 res2 249 end; 250*) 251 252fun applyPolarity true fm = fm 253 | applyPolarity false fm = negate fm; 254 255fun freeVars True = NameSet.empty 256 | freeVars False = NameSet.empty 257 | freeVars (Literal (fv,_)) = fv 258 | freeVars (And (fv,_,_)) = fv 259 | freeVars (Or (fv,_,_)) = fv 260 | freeVars (Xor (fv,_,_,_)) = fv 261 | freeVars (Exists (fv,_,_,_)) = fv 262 | freeVars (Forall (fv,_,_,_)) = fv; 263 264fun freeIn v fm = NameSet.member v (freeVars fm); 265 266val freeVarsSet = 267 let 268 fun free (fm,acc) = NameSet.union (freeVars fm) acc 269 in 270 Set.foldl free NameSet.empty 271 end; 272 273fun count True = countTrue 274 | count False = countFalse 275 | count (Literal _) = countLiteral 276 | count (And (_,c,_)) = c 277 | count (Or (_,c,_)) = c 278 | count (Xor (_,c,p,_)) = if p then c else countNegate c 279 | count (Exists (_,c,_,_)) = c 280 | count (Forall (_,c,_,_)) = c; 281 282val countAndSet = 283 let 284 fun countAnd (fm,c) = countAnd2 (count fm, c) 285 in 286 Set.foldl countAnd countTrue 287 end; 288 289val countOrSet = 290 let 291 fun countOr (fm,c) = countOr2 (count fm, c) 292 in 293 Set.foldl countOr countFalse 294 end; 295 296val countXorSet = 297 let 298 fun countXor (fm,c) = countXor2 (count fm, c) 299 in 300 Set.foldl countXor countFalse 301 end; 302 303fun And2 (False,_) = False 304 | And2 (_,False) = False 305 | And2 (True,f2) = f2 306 | And2 (f1,True) = f1 307 | And2 (f1,f2) = 308 let 309 val (fv1,c1,s1) = 310 case f1 of 311 And fv_c_s => fv_c_s 312 | _ => (freeVars f1, count f1, singleton f1) 313 314 and (fv2,c2,s2) = 315 case f2 of 316 And fv_c_s => fv_c_s 317 | _ => (freeVars f2, count f2, singleton f2) 318 in 319 if not (negateDisjoint s1 s2) then False 320 else 321 let 322 val s = Set.union s1 s2 323 in 324 case Set.size s of 325 0 => True 326 | 1 => Set.pick s 327 | n => 328 if n = Set.size s1 + Set.size s2 then 329 And (NameSet.union fv1 fv2, countAnd2 (c1,c2), s) 330 else 331 And (freeVarsSet s, countAndSet s, s) 332 end 333 end; 334 335val AndList = List.foldl And2 True; 336 337val AndSet = Set.foldl And2 True; 338 339fun Or2 (True,_) = True 340 | Or2 (_,True) = True 341 | Or2 (False,f2) = f2 342 | Or2 (f1,False) = f1 343 | Or2 (f1,f2) = 344 let 345 val (fv1,c1,s1) = 346 case f1 of 347 Or fv_c_s => fv_c_s 348 | _ => (freeVars f1, count f1, singleton f1) 349 350 and (fv2,c2,s2) = 351 case f2 of 352 Or fv_c_s => fv_c_s 353 | _ => (freeVars f2, count f2, singleton f2) 354 in 355 if not (negateDisjoint s1 s2) then True 356 else 357 let 358 val s = Set.union s1 s2 359 in 360 case Set.size s of 361 0 => False 362 | 1 => Set.pick s 363 | n => 364 if n = Set.size s1 + Set.size s2 then 365 Or (NameSet.union fv1 fv2, countOr2 (c1,c2), s) 366 else 367 Or (freeVarsSet s, countOrSet s, s) 368 end 369 end; 370 371val OrList = List.foldl Or2 False; 372 373val OrSet = Set.foldl Or2 False; 374 375fun pushOr2 (f1,f2) = 376 let 377 val s1 = case f1 of And (_,_,s) => s | _ => singleton f1 378 and s2 = case f2 of And (_,_,s) => s | _ => singleton f2 379 380 fun g x1 (x2,acc) = And2 (Or2 (x1,x2), acc) 381 382 fun f (x1,acc) = Set.foldl (g x1) acc s2 383 in 384 Set.foldl f True s1 385 end; 386 387val pushOrList = List.foldl pushOr2 False; 388 389local 390 fun normalize fm = 391 let 392 val p = polarity fm 393 val fm = applyPolarity p fm 394 in 395 (freeVars fm, count fm, p, singleton fm) 396 end; 397in 398 fun Xor2 (False,f2) = f2 399 | Xor2 (f1,False) = f1 400 | Xor2 (True,f2) = negate f2 401 | Xor2 (f1,True) = negate f1 402 | Xor2 (f1,f2) = 403 let 404 val (fv1,c1,p1,s1) = case f1 of Xor x => x | _ => normalize f1 405 and (fv2,c2,p2,s2) = case f2 of Xor x => x | _ => normalize f2 406 407 val s = Set.symmetricDifference s1 s2 408 409 val fm = 410 case Set.size s of 411 0 => False 412 | 1 => Set.pick s 413 | n => 414 if n = Set.size s1 + Set.size s2 then 415 Xor (NameSet.union fv1 fv2, countXor2 (c1,c2), true, s) 416 else 417 Xor (freeVarsSet s, countXorSet s, true, s) 418 419 val p = p1 = p2 420 in 421 applyPolarity p fm 422 end; 423end; 424 425val XorList = List.foldl Xor2 False; 426 427val XorSet = Set.foldl Xor2 False; 428 429fun XorPolarityList (p,l) = applyPolarity p (XorList l); 430 431fun XorPolaritySet (p,s) = applyPolarity p (XorSet s); 432 433fun destXor (Xor (_,_,p,s)) = 434 let 435 val (fm1,s) = Set.deletePick s 436 val fm2 = 437 if Set.size s = 1 then applyPolarity p (Set.pick s) 438 else Xor (freeVarsSet s, countXorSet s, p, s) 439 in 440 (fm1,fm2) 441 end 442 | destXor _ = raise Error "destXor"; 443 444fun pushXor fm = 445 let 446 val (f1,f2) = destXor fm 447 val f1' = negate f1 448 and f2' = negate f2 449 in 450 And2 (Or2 (f1,f2), Or2 (f1',f2')) 451 end; 452 453fun Exists1 (v,init_fm) = 454 let 455 fun exists_gen fm = 456 let 457 val fv = NameSet.delete (freeVars fm) v 458 val c = count fm 459 val n = NameSet.singleton v 460 in 461 Exists (fv,c,n,fm) 462 end 463 464 fun exists fm = if freeIn v fm then exists_free fm else fm 465 466 and exists_free (Or (_,_,s)) = OrList (Set.transform exists s) 467 | exists_free (fm as And (_,_,s)) = 468 let 469 val sv = Set.filter (freeIn v) s 470 in 471 if Set.size sv <> 1 then exists_gen fm 472 else 473 let 474 val fm = Set.pick sv 475 val s = Set.delete s fm 476 in 477 And2 (exists_free fm, AndSet s) 478 end 479 end 480 | exists_free (Exists (fv,c,n,f)) = 481 Exists (NameSet.delete fv v, c, NameSet.add n v, f) 482 | exists_free fm = exists_gen fm 483 in 484 exists init_fm 485 end; 486 487fun ExistsList (vs,f) = List.foldl Exists1 f vs; 488 489fun ExistsSet (n,f) = NameSet.foldl Exists1 f n; 490 491fun Forall1 (v,init_fm) = 492 let 493 fun forall_gen fm = 494 let 495 val fv = NameSet.delete (freeVars fm) v 496 val c = count fm 497 val n = NameSet.singleton v 498 in 499 Forall (fv,c,n,fm) 500 end 501 502 fun forall fm = if freeIn v fm then forall_free fm else fm 503 504 and forall_free (And (_,_,s)) = AndList (Set.transform forall s) 505 | forall_free (fm as Or (_,_,s)) = 506 let 507 val sv = Set.filter (freeIn v) s 508 in 509 if Set.size sv <> 1 then forall_gen fm 510 else 511 let 512 val fm = Set.pick sv 513 val s = Set.delete s fm 514 in 515 Or2 (forall_free fm, OrSet s) 516 end 517 end 518 | forall_free (Forall (fv,c,n,f)) = 519 Forall (NameSet.delete fv v, c, NameSet.add n v, f) 520 | forall_free fm = forall_gen fm 521 in 522 forall init_fm 523 end; 524 525fun ForallList (vs,f) = List.foldl Forall1 f vs; 526 527fun ForallSet (n,f) = NameSet.foldl Forall1 f n; 528 529fun generalize f = ForallSet (freeVars f, f); 530 531local 532 fun subst_fv fvSub = 533 let 534 fun add_fv (v,s) = NameSet.union (NameMap.get fvSub v) s 535 in 536 NameSet.foldl add_fv NameSet.empty 537 end; 538 539 fun subst_rename (v,(avoid,bv,sub,domain,fvSub)) = 540 let 541 val v' = Term.variantPrime avoid v 542 val avoid = NameSet.add avoid v' 543 val bv = NameSet.add bv v' 544 val sub = Subst.insert sub (v, Term.Var v') 545 val domain = NameSet.add domain v 546 val fvSub = NameMap.insert fvSub (v, NameSet.singleton v') 547 in 548 (avoid,bv,sub,domain,fvSub) 549 end; 550 551 fun subst_check sub domain fvSub fm = 552 let 553 val domain = NameSet.intersect domain (freeVars fm) 554 in 555 if NameSet.null domain then fm 556 else subst_domain sub domain fvSub fm 557 end 558 559 and subst_domain sub domain fvSub fm = 560 case fm of 561 Literal (fv,lit) => 562 let 563 val fv = NameSet.difference fv domain 564 val fv = NameSet.union fv (subst_fv fvSub domain) 565 val lit = Literal.subst sub lit 566 in 567 Literal (fv,lit) 568 end 569 | And (_,_,s) => 570 AndList (Set.transform (subst_check sub domain fvSub) s) 571 | Or (_,_,s) => 572 OrList (Set.transform (subst_check sub domain fvSub) s) 573 | Xor (_,_,p,s) => 574 XorPolarityList (p, Set.transform (subst_check sub domain fvSub) s) 575 | Exists fv_c_n_f => subst_quant Exists sub domain fvSub fv_c_n_f 576 | Forall fv_c_n_f => subst_quant Forall sub domain fvSub fv_c_n_f 577 | _ => raise Bug "subst_domain" 578 579 and subst_quant quant sub domain fvSub (fv,c,bv,fm) = 580 let 581 val sub_fv = subst_fv fvSub domain 582 val fv = NameSet.union sub_fv (NameSet.difference fv domain) 583 val captured = NameSet.intersect bv sub_fv 584 val bv = NameSet.difference bv captured 585 val avoid = NameSet.union fv bv 586 val (_,bv,sub,domain,fvSub) = 587 NameSet.foldl subst_rename (avoid,bv,sub,domain,fvSub) captured 588 val fm = subst_domain sub domain fvSub fm 589 in 590 quant (fv,c,bv,fm) 591 end; 592in 593 fun subst sub = 594 let 595 fun mk_dom (v,tm,(d,fv)) = 596 (NameSet.add d v, NameMap.insert fv (v, Term.freeVars tm)) 597 598 val domain_fvSub = (NameSet.empty, NameMap.new ()) 599 val (domain,fvSub) = Subst.foldl mk_dom domain_fvSub sub 600 in 601 subst_check sub domain fvSub 602 end; 603end; 604 605fun fromFormula fm = 606 case fm of 607 Formula.True => True 608 | Formula.False => False 609 | Formula.Atom atm => Literal (Atom.freeVars atm, (true,atm)) 610 | Formula.Not p => negateFromFormula p 611 | Formula.And (p,q) => And2 (fromFormula p, fromFormula q) 612 | Formula.Or (p,q) => Or2 (fromFormula p, fromFormula q) 613 | Formula.Imp (p,q) => Or2 (negateFromFormula p, fromFormula q) 614 | Formula.Iff (p,q) => Xor2 (negateFromFormula p, fromFormula q) 615 | Formula.Forall (v,p) => Forall1 (v, fromFormula p) 616 | Formula.Exists (v,p) => Exists1 (v, fromFormula p) 617 618and negateFromFormula fm = 619 case fm of 620 Formula.True => False 621 | Formula.False => True 622 | Formula.Atom atm => Literal (Atom.freeVars atm, (false,atm)) 623 | Formula.Not p => fromFormula p 624 | Formula.And (p,q) => Or2 (negateFromFormula p, negateFromFormula q) 625 | Formula.Or (p,q) => And2 (negateFromFormula p, negateFromFormula q) 626 | Formula.Imp (p,q) => And2 (fromFormula p, negateFromFormula q) 627 | Formula.Iff (p,q) => Xor2 (fromFormula p, fromFormula q) 628 | Formula.Forall (v,p) => Exists1 (v, negateFromFormula p) 629 | Formula.Exists (v,p) => Forall1 (v, negateFromFormula p); 630 631local 632 fun lastElt (s : formula Set.set) = 633 case Set.findr (K true) s of 634 NONE => raise Bug "lastElt: empty set" 635 | SOME fm => fm; 636 637 fun negateLastElt s = 638 let 639 val fm = lastElt s 640 in 641 Set.add (Set.delete s fm) (negate fm) 642 end; 643 644 fun form fm = 645 case fm of 646 True => Formula.True 647 | False => Formula.False 648 | Literal (_,lit) => Literal.toFormula lit 649 | And (_,_,s) => Formula.listMkConj (Set.transform form s) 650 | Or (_,_,s) => Formula.listMkDisj (Set.transform form s) 651 | Xor (_,_,p,s) => 652 let 653 val s = if p then negateLastElt s else s 654 in 655 Formula.listMkEquiv (Set.transform form s) 656 end 657 | Exists (_,_,n,f) => Formula.listMkExists (NameSet.toList n, form f) 658 | Forall (_,_,n,f) => Formula.listMkForall (NameSet.toList n, form f); 659in 660 val toFormula = form; 661end; 662 663fun toLiteral (Literal (_,lit)) = lit 664 | toLiteral _ = raise Error "Normalize.toLiteral"; 665 666local 667 fun addLiteral (l,s) = LiteralSet.add s (toLiteral l); 668in 669 fun toClause False = LiteralSet.empty 670 | toClause (Or (_,_,s)) = Set.foldl addLiteral LiteralSet.empty s 671 | toClause l = LiteralSet.singleton (toLiteral l); 672end; 673 674val pp = Print.ppMap toFormula Formula.pp; 675 676val toString = Print.toString pp; 677 678(* ------------------------------------------------------------------------- *) 679(* Negation normal form. *) 680(* ------------------------------------------------------------------------- *) 681 682fun nnf fm = toFormula (fromFormula fm); 683 684(* ------------------------------------------------------------------------- *) 685(* Basic conjunctive normal form. *) 686(* ------------------------------------------------------------------------- *) 687 688local 689 val counter : int StringMap.map ref = ref (StringMap.new ()); 690 691 fun new n () = 692 let 693 val ref m = counter 694 val s = Name.toString n 695 val i = Option.getOpt (StringMap.peek m s, 0) 696 val () = counter := StringMap.insert m (s, i + 1) 697 val i = if i = 0 then "" else "_" ^ Int.toString i 698 val s = skolemPrefix ^ "_" ^ s ^ i 699 in 700 Name.fromString s 701 end; 702in 703 fun newSkolemFunction n = Portable.critical (new n) (); 704end; 705 706fun skolemize fv bv fm = 707 let 708 val fv = NameSet.transform Term.Var fv 709 710 fun mk (v,s) = Subst.insert s (v, Term.Fn (newSkolemFunction v, fv)) 711 in 712 subst (NameSet.foldl mk Subst.empty bv) fm 713 end; 714 715local 716 fun rename avoid fv bv fm = 717 let 718 val captured = NameSet.intersect avoid bv 719 in 720 if NameSet.null captured then fm 721 else 722 let 723 fun ren (v,(a,s)) = 724 let 725 val v' = Term.variantPrime a v 726 in 727 (NameSet.add a v', Subst.insert s (v, Term.Var v')) 728 end 729 730 val avoid = NameSet.union (NameSet.union avoid fv) bv 731 732 val (_,sub) = NameSet.foldl ren (avoid,Subst.empty) captured 733 in 734 subst sub fm 735 end 736 end; 737 738 fun cnfFm avoid fm = 739(*MetisTrace5 740 let 741 val fm' = cnfFm' avoid fm 742 val () = Print.trace pp "Normalize.cnfFm: fm" fm 743 val () = Print.trace pp "Normalize.cnfFm: fm'" fm' 744 in 745 fm' 746 end 747 and cnfFm' avoid fm = 748*) 749 case fm of 750 True => True 751 | False => False 752 | Literal _ => fm 753 | And (_,_,s) => AndList (Set.transform (cnfFm avoid) s) 754 | Or (fv,_,s) => 755 let 756 val avoid = NameSet.union avoid fv 757 val (fms,_) = Set.foldl cnfOr ([],avoid) s 758 in 759 pushOrList fms 760 end 761 | Xor _ => cnfFm avoid (pushXor fm) 762 | Exists (fv,_,n,f) => cnfFm avoid (skolemize fv n f) 763 | Forall (fv,_,n,f) => cnfFm avoid (rename avoid fv n f) 764 765 and cnfOr (fm,(fms,avoid)) = 766 let 767 val fm = cnfFm avoid fm 768 val fms = fm :: fms 769 val avoid = NameSet.union avoid (freeVars fm) 770 in 771 (fms,avoid) 772 end; 773in 774 val basicCnf = cnfFm NameSet.empty; 775end; 776 777(* ------------------------------------------------------------------------- *) 778(* Finding the formula definition that minimizes the number of clauses. *) 779(* ------------------------------------------------------------------------- *) 780 781local 782 type best = count * formula option; 783 784 fun minBreak countClauses fm best = 785 case fm of 786 True => best 787 | False => best 788 | Literal _ => best 789 | And (_,_,s) => 790 minBreakSet countClauses countAnd2 countTrue AndSet s best 791 | Or (_,_,s) => 792 minBreakSet countClauses countOr2 countFalse OrSet s best 793 | Xor (_,_,_,s) => 794 minBreakSet countClauses countXor2 countFalse XorSet s best 795 | Exists (_,_,_,f) => minBreak countClauses f best 796 | Forall (_,_,_,f) => minBreak countClauses f best 797 798 and minBreakSet countClauses count2 count0 mkSet fmSet best = 799 let 800 fun cumulatives fms = 801 let 802 fun fwd (fm,(c1,s1,l)) = 803 let 804 val c1' = count2 (count fm, c1) 805 and s1' = Set.add s1 fm 806 in 807 (c1', s1', (c1,s1,fm) :: l) 808 end 809 810 fun bwd ((c1,s1,fm),(c2,s2,l)) = 811 let 812 val c2' = count2 (count fm, c2) 813 and s2' = Set.add s2 fm 814 in 815 (c2', s2', (c1,s1,fm,c2,s2) :: l) 816 end 817 818 val (c1,_,fms) = List.foldl fwd (count0,empty,[]) fms 819 val (c2,_,fms) = List.foldl bwd (count0,empty,[]) fms 820 821(*MetisDebug 822 val _ = countEquivish c1 c2 orelse 823 raise Bug ("cumulativeCounts: c1 = " ^ countToString c1 ^ 824 ", c2 = " ^ countToString c2) 825*) 826 in 827 fms 828 end 829 830 fun breakSing ((c1,_,fm,c2,_),best) = 831 let 832 val cFms = count2 (c1,c2) 833 834 fun countCls cFm = countClauses (count2 (cFms,cFm)) 835 in 836 minBreak countCls fm best 837 end 838 839 val breakSet1 = 840 let 841 fun break c1 s1 fm c2 (best as (bcl,_)) = 842 if Set.null s1 then best 843 else 844 let 845 val cDef = countDefinition (countXor2 (c1, count fm)) 846 val cFm = count2 (countLiteral,c2) 847 val cl = countAnd2 (cDef, countClauses cFm) 848 val noBetter = countLeqish bcl cl 849 in 850 if noBetter then best 851 else (cl, SOME (mkSet (Set.add s1 fm))) 852 end 853 in 854 fn ((c1,s1,fm,c2,s2),best) => 855 break c1 s1 fm c2 (break c2 s2 fm c1 best) 856 end 857 858 val fms = Set.toList fmSet 859 860 fun breakSet measure best = 861 let 862 val fms = sortMap (measure o count) countCompare fms 863 in 864 List.foldl breakSet1 best (cumulatives fms) 865 end 866 867 val best = List.foldl breakSing best (cumulatives fms) 868 val best = breakSet I best 869 val best = breakSet countNegate best 870 val best = breakSet countClauses best 871 in 872 best 873 end 874in 875 fun minimumDefinition fm = 876 let 877 val cl = count fm 878 in 879 if countLeqish cl countLiteral then NONE 880 else 881 let 882 val (cl',def) = minBreak I fm (cl,NONE) 883(*MetisTrace1 884 val () = 885 case def of 886 NONE => () 887 | SOME d => 888 Print.trace pp ("defCNF: before = " ^ countToString cl ^ 889 ", after = " ^ countToString cl' ^ 890 ", definition") d 891*) 892 in 893 def 894 end 895 end; 896end; 897 898(* ------------------------------------------------------------------------- *) 899(* Conjunctive normal form derivations. *) 900(* ------------------------------------------------------------------------- *) 901 902datatype thm = Thm of formula * inference 903 904and inference = 905 Axiom of Formula.formula 906 | Definition of string * Formula.formula 907 | Simplify of thm * thm list 908 | Conjunct of thm 909 | Specialize of thm 910 | Skolemize of thm 911 | Clausify of thm; 912 913fun parentsInference inf = 914 case inf of 915 Axiom _ => [] 916 | Definition _ => [] 917 | Simplify (th,ths) => th :: ths 918 | Conjunct th => [th] 919 | Specialize th => [th] 920 | Skolemize th => [th] 921 | Clausify th => [th]; 922 923fun compareThm (Thm (fm1,_), Thm (fm2,_)) = compare (fm1,fm2); 924 925fun parentsThm (Thm (_,inf)) = parentsInference inf; 926 927fun mkAxiom fm = Thm (fromFormula fm, Axiom fm); 928 929fun destThm (Thm (fm,inf)) = (toFormula fm, inf); 930 931local 932 val emptyProved : (thm,Formula.formula) Map.map = Map.new compareThm; 933 934 fun isProved proved th = Map.inDomain th proved; 935 936 fun isUnproved proved th = not (isProved proved th); 937 938 fun lookupProved proved th = 939 case Map.peek proved th of 940 SOME fm => fm 941 | NONE => raise Bug "Normalize.lookupProved"; 942 943 fun prove acc proved ths = 944 case ths of 945 [] => List.rev acc 946 | th :: ths' => 947 if isProved proved th then prove acc proved ths' 948 else 949 let 950 val pars = parentsThm th 951 952 val deps = List.filter (isUnproved proved) pars 953 in 954 if List.null deps then 955 let 956 val (fm,inf) = destThm th 957 958 val fms = List.map (lookupProved proved) pars 959 960 val acc = (fm,inf,fms) :: acc 961 962 val proved = Map.insert proved (th,fm) 963 in 964 prove acc proved ths' 965 end 966 else 967 let 968 val ths = deps @ ths 969 in 970 prove acc proved ths 971 end 972 end; 973in 974 val proveThms = prove [] emptyProved; 975end; 976 977fun toStringInference inf = 978 case inf of 979 Axiom _ => "Axiom" 980 | Definition _ => "Definition" 981 | Simplify _ => "Simplify" 982 | Conjunct _ => "Conjunct" 983 | Specialize _ => "Specialize" 984 | Skolemize _ => "Skolemize" 985 | Clausify _ => "Clausify"; 986 987val ppInference = Print.ppMap toStringInference Print.ppString; 988 989(* ------------------------------------------------------------------------- *) 990(* Simplifying with definitions. *) 991(* ------------------------------------------------------------------------- *) 992 993datatype simplify = 994 Simp of 995 {formula : (formula, formula * thm) Map.map, 996 andSet : (formula Set.set * formula * thm) list, 997 orSet : (formula Set.set * formula * thm) list, 998 xorSet : (formula Set.set * formula * thm) list}; 999 1000val simplifyEmpty = 1001 Simp 1002 {formula = Map.new compare, 1003 andSet = [], 1004 orSet = [], 1005 xorSet = []}; 1006 1007local 1008 fun simpler fm s = 1009 Set.size s <> 1 orelse 1010 case Set.pick s of 1011 True => false 1012 | False => false 1013 | Literal _ => false 1014 | _ => true; 1015 1016 fun addSet set_defs body_def = 1017 let 1018 fun def_body_size (body,_,_) = Set.size body 1019 1020 val body_size = def_body_size body_def 1021 1022 val (body,_,_) = body_def 1023 1024 fun add acc [] = List.revAppend (acc,[body_def]) 1025 | add acc (l as (bd as (b,_,_)) :: bds) = 1026 case Int.compare (def_body_size bd, body_size) of 1027 LESS => List.revAppend (acc, body_def :: l) 1028 | EQUAL => 1029 if Set.equal b body then List.revAppend (acc,l) 1030 else add (bd :: acc) bds 1031 | GREATER => add (bd :: acc) bds 1032 in 1033 add [] set_defs 1034 end; 1035 1036 fun add simp (body,False,th) = add simp (negate body, True, th) 1037 | add simp (True,_,_) = simp 1038 | add (Simp {formula,andSet,orSet,xorSet}) (And (_,_,s), def, th) = 1039 let 1040 val andSet = addSet andSet (s,def,th) 1041 and orSet = addSet orSet (negateSet s, negate def, th) 1042 in 1043 Simp 1044 {formula = formula, 1045 andSet = andSet, 1046 orSet = orSet, 1047 xorSet = xorSet} 1048 end 1049 | add (Simp {formula,andSet,orSet,xorSet}) (Or (_,_,s), def, th) = 1050 let 1051 val orSet = addSet orSet (s,def,th) 1052 and andSet = addSet andSet (negateSet s, negate def, th) 1053 in 1054 Simp 1055 {formula = formula, 1056 andSet = andSet, 1057 orSet = orSet, 1058 xorSet = xorSet} 1059 end 1060 | add simp (Xor (_,_,p,s), def, th) = 1061 let 1062 val simp = addXorSet simp (s, applyPolarity p def, th) 1063 in 1064 case def of 1065 True => 1066 let 1067 fun addXorLiteral (fm as Literal _, simp) = 1068 let 1069 val s = Set.delete s fm 1070 in 1071 if not (simpler fm s) then simp 1072 else addXorSet simp (s, applyPolarity (not p) fm, th) 1073 end 1074 | addXorLiteral (_,simp) = simp 1075 in 1076 Set.foldl addXorLiteral simp s 1077 end 1078 | _ => simp 1079 end 1080 | add (simp as Simp {formula,andSet,orSet,xorSet}) (body,def,th) = 1081 if Map.inDomain body formula then simp 1082 else 1083 let 1084 val formula = Map.insert formula (body,(def,th)) 1085 val formula = Map.insert formula (negate body, (negate def, th)) 1086 in 1087 Simp 1088 {formula = formula, 1089 andSet = andSet, 1090 orSet = orSet, 1091 xorSet = xorSet} 1092 end 1093 1094 and addXorSet (simp as Simp {formula,andSet,orSet,xorSet}) (s,def,th) = 1095 if Set.size s = 1 then add simp (Set.pick s, def, th) 1096 else 1097 let 1098 val xorSet = addSet xorSet (s,def,th) 1099 in 1100 Simp 1101 {formula = formula, 1102 andSet = andSet, 1103 orSet = orSet, 1104 xorSet = xorSet} 1105 end; 1106in 1107 fun simplifyAdd simp (th as Thm (fm,_)) = add simp (fm,True,th); 1108end; 1109 1110local 1111 fun simplifySet set_defs set = 1112 let 1113 fun pred (s,_,_) = Set.subset s set 1114 in 1115 case List.find pred set_defs of 1116 NONE => NONE 1117 | SOME (s,f,th) => 1118 let 1119 val set = Set.add (Set.difference set s) f 1120 in 1121 SOME (set,th) 1122 end 1123 end; 1124in 1125 fun simplify (Simp {formula,andSet,orSet,xorSet}) = 1126 let 1127 fun simp fm inf = 1128 case simp_sub fm inf of 1129 NONE => simp_top fm inf 1130 | SOME (fm,inf) => try_simp_top fm inf 1131 1132 and try_simp_top fm inf = 1133 case simp_top fm inf of 1134 NONE => SOME (fm,inf) 1135 | x => x 1136 1137 and simp_top fm inf = 1138 case fm of 1139 And (_,_,s) => 1140 (case simplifySet andSet s of 1141 NONE => NONE 1142 | SOME (s,th) => 1143 let 1144 val fm = AndSet s 1145 val inf = th :: inf 1146 in 1147 try_simp_top fm inf 1148 end) 1149 | Or (_,_,s) => 1150 (case simplifySet orSet s of 1151 NONE => NONE 1152 | SOME (s,th) => 1153 let 1154 val fm = OrSet s 1155 val inf = th :: inf 1156 in 1157 try_simp_top fm inf 1158 end) 1159 | Xor (_,_,p,s) => 1160 (case simplifySet xorSet s of 1161 NONE => NONE 1162 | SOME (s,th) => 1163 let 1164 val fm = XorPolaritySet (p,s) 1165 val inf = th :: inf 1166 in 1167 try_simp_top fm inf 1168 end) 1169 | _ => 1170 (case Map.peek formula fm of 1171 NONE => NONE 1172 | SOME (fm,th) => 1173 let 1174 val inf = th :: inf 1175 in 1176 try_simp_top fm inf 1177 end) 1178 1179 and simp_sub fm inf = 1180 case fm of 1181 And (_,_,s) => 1182 (case simp_set s inf of 1183 NONE => NONE 1184 | SOME (l,inf) => SOME (AndList l, inf)) 1185 | Or (_,_,s) => 1186 (case simp_set s inf of 1187 NONE => NONE 1188 | SOME (l,inf) => SOME (OrList l, inf)) 1189 | Xor (_,_,p,s) => 1190 (case simp_set s inf of 1191 NONE => NONE 1192 | SOME (l,inf) => SOME (XorPolarityList (p,l), inf)) 1193 | Exists (_,_,n,f) => 1194 (case simp f inf of 1195 NONE => NONE 1196 | SOME (f,inf) => SOME (ExistsSet (n,f), inf)) 1197 | Forall (_,_,n,f) => 1198 (case simp f inf of 1199 NONE => NONE 1200 | SOME (f,inf) => SOME (ForallSet (n,f), inf)) 1201 | _ => NONE 1202 1203 and simp_set s inf = 1204 let 1205 val (changed,l,inf) = Set.foldr simp_set_elt (false,[],inf) s 1206 in 1207 if changed then SOME (l,inf) else NONE 1208 end 1209 1210 and simp_set_elt (fm,(changed,l,inf)) = 1211 case simp fm inf of 1212 NONE => (changed, fm :: l, inf) 1213 | SOME (fm,inf) => (true, fm :: l, inf) 1214 in 1215 fn th as Thm (fm,_) => 1216 case simp fm [] of 1217 SOME (fm,ths) => 1218 let 1219 val inf = Simplify (th,ths) 1220 in 1221 Thm (fm,inf) 1222 end 1223 | NONE => th 1224 end; 1225end; 1226 1227(*MetisTrace2 1228val simplify = fn simp => fn th as Thm (fm,_) => 1229 let 1230 val th' as Thm (fm',_) = simplify simp th 1231 val () = if compare (fm,fm') = EQUAL then () 1232 else (Print.trace pp "Normalize.simplify: fm" fm; 1233 Print.trace pp "Normalize.simplify: fm'" fm') 1234 in 1235 th' 1236 end; 1237*) 1238 1239(* ------------------------------------------------------------------------- *) 1240(* Definitions. *) 1241(* ------------------------------------------------------------------------- *) 1242 1243local 1244 val counter : int ref = ref 0; 1245 1246 fun new () = 1247 let 1248 val ref i = counter 1249 val () = counter := i + 1 1250 in 1251 definitionPrefix ^ "_" ^ Int.toString i 1252 end; 1253in 1254 fun newDefinitionRelation () = Portable.critical new (); 1255end; 1256 1257fun newDefinition def = 1258 let 1259 val fv = freeVars def 1260 val rel = newDefinitionRelation () 1261 val atm = (Name.fromString rel, NameSet.transform Term.Var fv) 1262 val fm = Formula.Iff (Formula.Atom atm, toFormula def) 1263 val fm = Formula.setMkForall (fv,fm) 1264 val inf = Definition (rel,fm) 1265 val lit = Literal (fv,(false,atm)) 1266 val fm = Xor2 (lit,def) 1267 in 1268 Thm (fm,inf) 1269 end; 1270 1271(* ------------------------------------------------------------------------- *) 1272(* Definitional conjunctive normal form. *) 1273(* ------------------------------------------------------------------------- *) 1274 1275datatype cnf = 1276 ConsistentCnf of simplify 1277 | InconsistentCnf; 1278 1279val initialCnf = ConsistentCnf simplifyEmpty; 1280 1281local 1282 fun def_cnf_inconsistent th = 1283 let 1284 val cls = [(LiteralSet.empty,th)] 1285 in 1286 (cls,InconsistentCnf) 1287 end; 1288 1289 fun def_cnf_clause inf (fm,acc) = 1290 let 1291 val cl = toClause fm 1292 val th = Thm (fm,inf) 1293 in 1294 (cl,th) :: acc 1295 end 1296(*MetisDebug 1297 handle Error err => 1298 (Print.trace pp "Normalize.addCnf.def_cnf_clause: fm" fm; 1299 raise Bug ("Normalize.addCnf.def_cnf_clause: " ^ err)); 1300*) 1301 1302 fun def_cnf cls simp ths = 1303 case ths of 1304 [] => (cls, ConsistentCnf simp) 1305 | th :: ths => def_cnf_formula cls simp (simplify simp th) ths 1306 1307 and def_cnf_formula cls simp (th as Thm (fm,_)) ths = 1308 case fm of 1309 True => def_cnf cls simp ths 1310 | False => def_cnf_inconsistent th 1311 | And (_,_,s) => 1312 let 1313 fun add (f,z) = Thm (f, Conjunct th) :: z 1314 in 1315 def_cnf cls simp (Set.foldr add ths s) 1316 end 1317 | Exists (fv,_,n,f) => 1318 let 1319 val th = Thm (skolemize fv n f, Skolemize th) 1320 in 1321 def_cnf_formula cls simp th ths 1322 end 1323 | Forall (_,_,_,f) => 1324 let 1325 val th = Thm (f, Specialize th) 1326 in 1327 def_cnf_formula cls simp th ths 1328 end 1329 | _ => 1330 case minimumDefinition fm of 1331 SOME def => 1332 let 1333 val ths = th :: ths 1334 val th = newDefinition def 1335 in 1336 def_cnf_formula cls simp th ths 1337 end 1338 | NONE => 1339 let 1340 val simp = simplifyAdd simp th 1341 1342 val fm = basicCnf fm 1343 1344 val inf = Clausify th 1345 in 1346 case fm of 1347 True => def_cnf cls simp ths 1348 | False => def_cnf_inconsistent (Thm (fm,inf)) 1349 | And (_,_,s) => 1350 let 1351 val inf = Conjunct (Thm (fm,inf)) 1352 val cls = Set.foldl (def_cnf_clause inf) cls s 1353 in 1354 def_cnf cls simp ths 1355 end 1356 | fm => def_cnf (def_cnf_clause inf (fm,cls)) simp ths 1357 end; 1358in 1359 fun addCnf th cnf = 1360 case cnf of 1361 ConsistentCnf simp => def_cnf [] simp [th] 1362 | InconsistentCnf => ([],cnf); 1363end; 1364 1365local 1366 fun add (th,(cls,cnf)) = 1367 let 1368 val (cls',cnf) = addCnf th cnf 1369 in 1370 (cls' @ cls, cnf) 1371 end; 1372in 1373 fun proveCnf ths = 1374 let 1375 val (cls,_) = List.foldl add ([],initialCnf) ths 1376 in 1377 List.rev cls 1378 end; 1379end; 1380 1381fun cnf fm = 1382 let 1383 val cls = proveCnf [mkAxiom fm] 1384 in 1385 List.map fst cls 1386 end; 1387 1388end 1389