1(* ========================================================================= *) 2(* METIS TESTS *) 3(* Copyright (c) 2004 Joe Hurd, distributed under the BSD License *) 4(* ========================================================================= *) 5 6(* ------------------------------------------------------------------------- *) 7(* Dummy versions of Moscow ML declarations to stop real compilers barfing. *) 8(* ------------------------------------------------------------------------- *) 9 10(*mlton 11val quotation = ref true; 12val quietdec = ref true; 13val loadPath = ref ([] : string list); 14val load = fn (_ : string) => (); 15*) 16 17(*polyml 18val quotation = ref true; 19val quietdec = ref true; 20val loadPath = ref ([] : string list); 21val load = fn (_ : string) => (); 22*) 23 24(* ------------------------------------------------------------------------- *) 25(* Load and open some useful modules *) 26(* ------------------------------------------------------------------------- *) 27 28val () = loadPath := !loadPath @ ["../bin/mosml"]; 29val () = app load ["Options"]; 30 31open Useful; 32 33val time = Portable.time; 34 35(* ------------------------------------------------------------------------- *) 36(* Problem data. *) 37(* ------------------------------------------------------------------------- *) 38 39val ref oldquietdec = quietdec; 40val () = quietdec := true; 41val () = quotation := true; 42use "../src/problems.sml"; 43val () = quietdec := oldquietdec; 44 45(* ------------------------------------------------------------------------- *) 46(* Helper functions. *) 47(* ------------------------------------------------------------------------- *) 48 49fun partialOrderToString (SOME LESS) = "SOME LESS" 50 | partialOrderToString (SOME GREATER) = "SOME GREATER" 51 | partialOrderToString (SOME EQUAL) = "SOME EQUAL" 52 | partialOrderToString NONE = "NONE"; 53 54fun SAY s = 55 TextIO.print 56 ("-------------------------------------" ^ 57 "-------------------------------------\n" ^ s ^ "\n\n"); 58 59fun printval p x = (TextIO.print (Print.toString p x ^ "\n\n"); x); 60 61fun mkCl p th = Clause.mk {parameters = p, id = Clause.newId (), thm = th}; 62 63val pvBool = printval Print.ppBool 64and pvPo = printval (Print.ppMap partialOrderToString Print.ppString) 65and pvFm = printval Formula.pp 66and pvFms = printval (Print.ppList Formula.pp) 67and pvThm = printval Thm.pp 68and pvEqn : Rule.equation -> Rule.equation = printval (Print.ppMap snd Thm.pp) 69and pvNet = printval (LiteralNet.pp Print.ppInt) 70and pvRw = printval Rewrite.pp 71and pvU = printval Units.pp 72and pvLits = printval LiteralSet.pp 73and pvCl = printval Clause.pp 74and pvCls = printval (Print.ppList Clause.pp) 75and pvM = printval Model.pp; 76 77val NV = Name.fromString 78and NF = Name.fromString 79and NR = Name.fromString; 80val V = Term.Var o NV 81and C = (fn c => Term.Fn (NF c, [])) 82and T = Term.parse 83and A = Atom.parse 84and L = Literal.parse 85and F = Formula.parse 86and S = Subst.fromList; 87val LS = LiteralSet.fromList o List.map L; 88val AX = Thm.axiom o LS; 89val CL = mkCl Clause.default o AX; 90val Q = (fn th => (Thm.destUnitEq th, th)) o AX o singleton 91and U = (fn th => (Thm.destUnit th, th)) o AX o singleton; 92 93fun test_fun eq p r a = 94 if eq r a then p a ^ "\n" else 95 (TextIO.print 96 ("\n\n" ^ 97 "test: should have\n-->" ^ p r ^ "<--\n\n" ^ 98 "test: actually have\n-->" ^ p a ^ "<--\n\n"); 99 raise Fail "test: failed a test"); 100 101fun test eq p r a = TextIO.print (test_fun eq p r a ^ "\n"); 102 103val test_tm = test Term.equal Term.toString o Term.parse; 104 105val test_fm = test Formula.equal Formula.toString o Formula.parse; 106 107fun test_id p f a = test p a (f a); 108 109fun chop_newline s = 110 if String.sub (s,0) = #"\n" then String.extract (s,1,NONE) else s; 111 112fun unquote (QUOTE q) = q 113 | unquote (ANTIQUOTE _) = raise Fail "unquote"; 114 115(* ------------------------------------------------------------------------- *) 116val () = SAY "The parser and pretty-printer"; 117(* ------------------------------------------------------------------------- *) 118 119fun prep l = (chop_newline o String.concat o List.map unquote) l; 120 121fun mini_print n fm = withRef (Print.lineLength,n) Formula.toString fm; 122 123fun testlen_pp n q = 124 (fn s => test_fun equal I s ((mini_print n o Formula.fromString) s)) 125 (prep q); 126 127fun test_pp q = TextIO.print (testlen_pp 40 q ^ "\n"); 128 129val () = test_pp `3 = f x`; 130 131val () = test_pp `f x y = y`; 132 133val () = test_pp `P x y`; 134 135val () = test_pp `P (f x) y`; 136 137val () = test_pp `f x = 3`; 138 139val () = test_pp `!x. P x y`; 140 141val () = test_pp `!x y. P x y`; 142 143val () = test_pp `!x y z. P x y z`; 144 145val () = test_pp `x = y`; 146 147val () = test_pp `x = 3`; 148 149val () = test_pp `x + y = y`; 150 151val () = test_pp `x / y * z = w`; 152 153val () = test_pp `x * y * z = x * (y * z)`; 154 155val () = test_pp `!x. ?y. x <= y /\ y <= x`; 156 157val () = test_pp `?x. !y. x + y = y /\ y <= x`; 158 159val () = test_pp `p /\ q \/ r /\ p ==> q <=> p`; 160 161val () = test_pp `p`; 162 163val () = test_pp `~!x. bool x`; 164 165val () = test_pp `p ==> !x. bool x`; 166 167val () = test_pp `p ==> ~!x. bool x`; 168 169val () = test_pp `~!x. bool x`; 170 171val () = test_pp `~~!x. bool x`; 172 173val () = test_pp `hello + there <> everybody`; 174 175val () = test_pp `!x y. ?z. x < z /\ y < z`; 176 177val () = test_pp `~(!x. P x) <=> ?y. ~P y`; 178 179val () = test_pp `?y. x < y ==> !v. ?w. x * v < y * w`; 180 181val () = test_pp `(<=)`; 182 183val () = test_pp `(<=) <= b`; 184 185val () = test_pp `(<=) <= (+)`; 186 187val () = test_pp `(<=) x`; 188 189val () = test_pp `(<=) <= (+) x`; 190 191val () = test_pp `~B (P % ((,) % c_a % v_b))`; 192 193val () = test_pp `B ((<=) % 0 % (LENGTH % NIL))`; 194 195val () = test_pp `~(a = b)`; 196 197val () = test_pp `!x. p x ==> !y. p y`; 198 199val () = test_pp `(!x. p x) ==> !y. p y`; 200 201val () = test_pp `!x. ~~x = x`; 202 203val () = test_pp `x + (y + z) = a`; 204 205val () = test_pp `(x @ y) @ z = a`; 206 207val () = test_pp `p ((a @ a) @ a = a)`; 208 209val () = test_pp `!x y z. (x @ y) @ z = (x @ z) @ y @ z`; 210 211val () = test_pp `~(!x. q x) /\ p`; 212 213val () = test_pp `!x. f (~~x) b (~c)`; 214 215val () = test_pp `p ==> ~(a /\ b)`; 216 217val () = test_pp `!water. drinks (water)`; 218 219val () = test_pp `!vat water. drinks ((vat) p x (water))`; 220 221val () = test_pp `!x y. ~{x < y} /\ T`; 222 223val () = test_pp `[3]`; 224 225val () = test_pp ` 226!x y z. ?x' y' z'. 227 P x y z ==> P x' y' z'`; 228 229val () = test_pp ` 230(!x. P x ==> !x. Q x) /\ 231((!x. Q x \/ R x) ==> ?x. Q x /\ R x) /\ 232((?x. R x) ==> !x. L x ==> M x) ==> 233!x. P x /\ L x ==> M x`; 234 235val () = test_pp ` 236!x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 237 x12 x13 x14 x15 x16 x17 x18 x19 x20 238 x21 x22 x23 x24 x25 x26 x27 x28 x29 239 x30 x31 x32. ?y0 y1 y2 y3 y4 y5 y6 y7. 240 P`; 241 242val () = test_pp ` 243!x x x x x x x x x x x x x x x x x x x x 244 x x x x x x x x x x. ?y y y y y y y y 245 y y y y y y y y y y y. 246 P (x, y) /\ P (x, y) /\ P (x, y) /\ 247 P (x, y) /\ P (x, y) /\ P (x, y) /\ 248 P (x, y) /\ P (x, y) /\ P (x, y) /\ 249 P (x, y) /\ P (x, y) /\ P (x, y) /\ 250 P (x, y) /\ P (x, y) /\ 251 ~~~~~~~~~~~~~f 252 (f (f (f x y) (f x y)) 253 (f (f x y) (f x y))) 254 (f (f (f x y) (f x y)) 255 (f (f x y) (f x y)))`; 256 257val () = test_pp ` 258(!x. 259 extremely__long__predicate__name) /\ 260F`; 261 262val () = test_pp ` 263(!x. x = x) /\ 264(!x y. ~(x = y) \/ y = x) /\ 265(!x y z. 266 ~(x = y) \/ ~(y = z) \/ x = z) /\ 267(!x y z. b . x . y . z = x . (y . z)) /\ 268(!x y. t . x . y = y . x) /\ 269(!x y z. ~(x = y) \/ x . z = y . z) /\ 270(!x y z. ~(x = y) \/ z . x = z . y) ==> 271~(b . (b . (t . b) . b) . t . x . y . 272 z = y . (x . z)) ==> F`; 273 274(* ------------------------------------------------------------------------- *) 275val () = SAY "Substitution"; 276(* ------------------------------------------------------------------------- *) 277 278val () = 279 test Name.equal Name.toString (NV"x") 280 (Term.variantPrime (NameSet.fromList [NV"y",NV"z" ]) (NV"x")); 281 282val () = 283 test Name.equal Name.toString (NV"x'") 284 (Term.variantPrime (NameSet.fromList [NV"x",NV"y" ]) (NV"x")); 285 286val () = 287 test Name.equal Name.toString (NV"x''") 288 (Term.variantPrime (NameSet.fromList [NV"x",NV"x'"]) (NV"x")); 289 290val () = 291 test Name.equal Name.toString (NV"x") 292 (Term.variantNum (NameSet.fromList [NV"y",NV"z"]) (NV"x")); 293 294val () = 295 test Name.equal Name.toString (NV"x0") 296 (Term.variantNum (NameSet.fromList [NV"x",NV"y"]) (NV"x")); 297 298val () = 299 test Name.equal Name.toString (NV"x1") 300 (Term.variantNum (NameSet.fromList [NV"x",NV"x0"]) (NV"x")); 301 302val () = 303 test_fm 304 `!x. x = $z` 305 (Formula.subst (S [(NV"y", V"z")]) (F`!x. x = $y`)); 306 307val () = 308 test_fm 309 `!x'. x' = $x` 310 (Formula.subst (S [(NV"y", V"x")]) (F`!x. x = $y`)); 311 312val () = 313 test_fm 314 `!x' x''. x' = $x ==> x' = x''` 315 (Formula.subst (S [(NV"y", V"x")]) 316 (F`!x x'. x = $y ==> x = x'`)); 317 318(* ------------------------------------------------------------------------- *) 319val () = SAY "Unification"; 320(* ------------------------------------------------------------------------- *) 321 322fun unify_and_apply tm1 tm2 = 323 Subst.subst (Subst.unify Subst.empty tm1 tm2) tm1; 324 325val () = test_tm `c` (unify_and_apply (V"x") (C"c")); 326 327val () = test_tm `c` (unify_and_apply (C"c") (V"x")); 328 329val () = 330 test_tm 331 `f c` 332 (unify_and_apply 333 (Term.Fn (NF"f", [V"x"])) 334 (Term.Fn (NF"f", [C"c"]))); 335 336val () = test_tm `f 0 0 0` (unify_and_apply (T`f 0 $x $x`) (T`f $y $y $z`)); 337 338fun f x y = (printval Subst.pp (Atom.unify Subst.empty x y); ()); 339 340val () = f (NR"P", [V"x"]) (NR"P", [V"x"]); 341 342val () = f (NR"P", [V"x"]) (NR"P", [C"c"]); 343 344val () = f (A`P c_x`) (A`P $x`); 345 346val () = f (A`q $x (f $x)`) (A`q $y $z`); 347 348(* ------------------------------------------------------------------------- *) 349val () = SAY "The logical kernel"; 350(* ------------------------------------------------------------------------- *) 351 352val th0 = AX [`p`,`q`]; 353val th1 = AX [`~p`,`r`]; 354val th2 = Thm.resolve (L`p`) th0 th1; 355val _ = printval Proof.pp (Proof.proof th2); 356 357val th0 = Rule.relationCongruence Atom.eqRelation; 358val th1 = 359 Thm.subst (S [(NV"y0",T`$x`),(NV"y1",T`$y`),(NV"x1",T`$z`),(NV"x0",T`$x`)]) th0; 360val th2 = Thm.resolve (L`$x = $x`) Rule.reflexivity th1; 361val th3 = Rule.symNeq (L`~($z = $y)`) th2; 362val _ = printval Proof.pp (Proof.proof th3); 363 364(* Testing the elimination of redundancies in proofs *) 365 366val th0 = Rule.reflexivity; 367val th1 = Thm.subst (S [(NV"x", Term.Fn (NF"f", [V"y"]))]) th0; 368val th2 = Thm.subst (S [(NV"y", C"c")]) th1; 369val _ = printval Proof.pp (Proof.proof th2); 370 371(* ------------------------------------------------------------------------- *) 372val () = SAY "Derived rules of inference"; 373(* ------------------------------------------------------------------------- *) 374 375val th0 = pvThm (AX [`$x = a`, `f a = $x`, `~(a = b)`, `a = $x`, 376 `$x = a`, `a = $x`, `~(b = a)`]); 377val th1 = pvThm (Rule.removeSym th0); 378val th2 = pvThm (Rule.symEq (L`a = $x`) th0); 379val th3 = pvThm (Rule.symEq (L`f a = $x`) th0); 380val th5 = pvThm (Rule.symNeq (L`~(a = b)`) th0); 381 382(* Testing the rewrConv conversion *) 383val (x_y as (x,y), eqTh) = pvEqn (Q`e * (i $z * $z) = e`); 384val tm = Term.Fn (NF"f",[x]); 385val path : int list = [0]; 386val reflTh = Thm.refl tm; 387val reflLit = Thm.destUnit reflTh; 388val th = Thm.equality reflLit (1 :: path) y; 389val th = Thm.resolve reflLit reflTh th; 390val th = pvThm (try (Thm.resolve (Literal.mkEq x_y) eqTh) th); 391 392(* ------------------------------------------------------------------------- *) 393val () = SAY "Discrimination nets for literals"; 394(* ------------------------------------------------------------------------- *) 395 396val n = pvNet (LiteralNet.new {fifo = true}); 397val n = pvNet (LiteralNet.insert n (L`P (f c $x a)`, 1)); 398val n = pvNet (LiteralNet.insert n (L`P (f c $y a)`, 2)); 399val n = pvNet (LiteralNet.insert n (L`P (f c a a)`, 3)); 400val n = pvNet (LiteralNet.insert n (L`P (f c b a)`, 4)); 401val n = pvNet (LiteralNet.insert n (L`~Q`, 5)); 402val n = pvNet (LiteralNet.insert n (L`~Q`, 6)); 403val n = pvNet (LiteralNet.insert n (L`~Q`, 7)); 404val n = pvNet (LiteralNet.insert n (L`~Q`, 8)); 405 406(* ------------------------------------------------------------------------- *) 407val () = SAY "The Knuth-Bendix ordering on terms"; 408(* ------------------------------------------------------------------------- *) 409 410val kboOrder = KnuthBendixOrder.default; 411val kboCmp = KnuthBendixOrder.compare kboOrder; 412 413val x = pvPo (kboCmp (T`f a`, T`g b`)); 414val x = pvPo (kboCmp (T`f a b`, T`g b`)); 415val x = pvPo (kboCmp (T`f $x`, T`g a`)); 416val x = pvPo (kboCmp (T`f a $x`, T`g $x`)); 417val x = pvPo (kboCmp (T`f $x`, T`g $x`)); 418val x = pvPo (kboCmp (T`f $x`, T`f $x`)); 419val x = pvPo (kboCmp (T`$x + $y`, T`$x + $x`)); 420val x = pvPo (kboCmp (T`$x + $y + $x`, T`$y + $x + $x`)); 421val x = pvPo (kboCmp (T`$x + $y + $x`, T`$y * $x + $x`)); 422val x = pvPo (kboCmp (T`a`, T`$x`)); 423val x = pvPo (kboCmp (T`f a`, T`$x`)); 424val x = pvPo (kboCmp (T`f $x (f $y $z)`, T`f (f $x $y) $z`)); 425val x = pvPo (kboCmp (T`f (g $x a)`, T`f (h a $x)`)); 426val x = pvPo (kboCmp (T`f (g a)`, T`f (h $x)`)); 427val x = pvPo (kboCmp (T`f (h a)`, T`f (g $x)`)); 428val x = pvPo (kboCmp (T`f $y`, T`f (g a b c)`)); 429val x = pvPo (kboCmp (T`$x * $y + $x * $z`, T`$x * ($y + $z)`)); 430 431(* ------------------------------------------------------------------------- *) 432val () = SAY "Rewriting"; 433(* ------------------------------------------------------------------------- *) 434 435val eqnsToRw = Rewrite.addList (Rewrite.new kboCmp) o enumerate; 436 437val eqns = [Q`e * $x = $x`, Q`$x * e = $x`, Q`i $x * $x = e`, Q`$x * i $x = e`]; 438val ax = pvThm (AX [`e * (i $z * $z) = i e * e`]); 439val th = pvThm (Rewrite.orderedRewrite kboCmp eqns ax); 440 441val rw = pvRw (eqnsToRw eqns); 442val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * e`))); 443val th = pvThm (snd (try (Rewrite.rewriteConv rw kboCmp) (T`e * (i $z * $z)`))); 444val th = pvThm (try (Rewrite.rewriteRule rw kboCmp) ax); 445 446(* Bug check: in this one a literal goes missing, due to the Resolve in Subst *) 447val eqns = [Q`f a = a`]; 448val ax = pvThm (AX [`~(g (f a) = b)`, `~(f a = a)`]); 449val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); 450 451(* Bug check: term paths were not being reversed before use *) 452val eqns = [Q`a = f a`]; 453val ax = pvThm (AX [`a <= f (f a)`]); 454val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); 455 456(* Bug check: Equality used to complain if the literal didn't exist *) 457val eqns = [Q`b = f a`]; 458val ax = pvThm (AX [`~(f a = f a)`]); 459val th = pvThm (try (Rewrite.orderedRewrite kboCmp eqns) ax); 460 461(* Testing the rewriting with disequalities in the same clause *) 462val ax = pvThm (AX [`~(a = b)`, `P a`, `P b`]); 463val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 464 465val ax = pvThm (AX [`~(f $x = $x)`, `P (f a)`, `P (f $x)`, `P (f $y)`]); 466val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 467 468val ax = pvThm 469 (AX [`~(f (f (f (f (f $x)))) = $x)`, 470 `~(f (f (f (f (f (f (f (f $x))))))) = $x)`, 471 `P (f $x)`]); 472val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 473 474(* Symmetry should yield a tautology on ground clauses *) 475val ax = pvThm (AX [`~(a = b)`, `b = a`]); 476val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 477 478(* Transitivity should yield a tautology on ground clauses *) 479val ax = pvThm (AX [`~(a = b)`, `~(b = c)`, `a = c`]); 480val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 481 482(* Extended transitivity should yield a tautology on ground clauses *) 483val ax = pvThm (AX [`~(a = b)`, `~(b = c)`, `~(c = d)`, `a = d`]); 484val th = pvThm (try (Rewrite.orderedRewrite kboCmp []) ax); 485 486(* ------------------------------------------------------------------------- *) 487val () = SAY "Unit cache"; 488(* ------------------------------------------------------------------------- *) 489 490val u = pvU (Units.add Units.empty (U`~p $x`)); 491val u = pvU (Units.add u (U`a = b`)); 492val _ = pvThm (Units.reduce u (AX [`p 0`,`~(b = a)`])); 493 494(* ------------------------------------------------------------------------- *) 495val () = SAY "Negation normal form"; 496(* ------------------------------------------------------------------------- *) 497 498val nnf = Normalize.nnf; 499 500val _ = pvFm (nnf (F`p /\ ~p`)); 501val _ = pvFm (nnf (F`(!x. P x) ==> ((?y. Q y) <=> (?z. P z /\ Q z))`)); 502val _ = pvFm (nnf (F`~(~(p <=> q) <=> r) <=> ~(p <=> ~(q <=> r))`)); 503 504(* ------------------------------------------------------------------------- *) 505val () = SAY "Conjunctive normal form"; 506(* ------------------------------------------------------------------------- *) 507 508local 509 fun clauseToFormula cl = 510 Formula.listMkDisj (LiteralSet.transform Literal.toFormula cl); 511in 512 fun clausesToFormula cls = Formula.listMkConj (List.map clauseToFormula cls); 513end; 514 515val cnf' = pvFm o clausesToFormula o Normalize.cnf o F; 516 517val cnf = pvFm o clausesToFormula o Normalize.cnf o 518 Formula.Not o Formula.generalize o F; 519 520val _ = cnf `p \/ ~p`; 521val _ = cnf `~((p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s))`; 522val _ = cnf `~((p /\ (q \/ r /\ s)) /\ (~p \/ ~q \/ ~s) /\ (p \/ ~p))`; 523val _ = cnf `~(~(p <=> q) <=> r) <=> ~(p <=> ~(q <=> r))`; 524val _ = cnf `((p <=> q) <=> r) <=> (p <=> (q <=> r))`; 525val _ = cnf `~(!x. ?y. x < y ==> !v. ?w. x * v < y * w)`; 526val _ = cnf `~(!x. P x ==> (?y z. Q y \/ ~(?z. P z /\ Q z)))`; 527val _ = cnf `~(?x y. x + y = 2)`; 528val _ = cnf' `(!x. p x) \/ (!y. r $x y)`; 529 530val _ = cnf 531 `(!x. P x ==> (!x. Q x)) /\ ((!x. Q x \/ R x) ==> (?x. Q x /\ R x)) /\ 532 ((?x. R x) ==> (!x. L x ==> M x)) ==> (!x. P x /\ L x ==> M x)`; 533 534(* ------------------------------------------------------------------------- *) 535val () = SAY "Finite models"; 536(* ------------------------------------------------------------------------- *) 537 538fun checkModelClause M cl = 539 let 540 val randomSamples = 100 541 542 fun addRandomSample {T,F} = 543 let 544 val {T = T', F = F'} = Model.checkClause {maxChecks = SOME 1} M cl 545 in 546 {T = T + T', F = F + F'} 547 end 548 549 val {T,F} = funpow randomSamples addRandomSample {T = 0, F = 0} 550 val rx = Real.fromInt T / Real.fromInt (T + F) 551 552 val {T,F} = Model.checkClause {maxChecks = NONE} M cl 553 val ry = Real.fromInt T / Real.fromInt (T + F) 554 in 555 [Formula.toString (LiteralSet.disjoin cl), 556 " | random sampling = " ^ percentToString rx, 557 " | exhaustive = " ^ percentToString ry] 558 end; 559 560local 561 val format = 562 [{leftAlign = true, padChar = #" "}, 563 {leftAlign = true, padChar = #" "}, 564 {leftAlign = true, padChar = #" "}]; 565in 566 fun checkModel M cls = 567 let 568 val table = List.map (checkModelClause M) cls 569 570 val rows = alignTable format table 571 572 val () = TextIO.print (join "\n" rows ^ "\n\n") 573 in 574 () 575 end; 576end; 577 578fun perturbModel M cls n = 579 let 580 val N = {size = Model.size M} 581 582 fun perturbClause (fv,cl) = 583 let 584 val V = Model.randomValuation N fv 585 in 586 if Model.interpretClause M V cl then () 587 else Model.perturbClause M V cl 588 end 589 590 val cls = List.map (fn cl => (LiteralSet.freeVars cl, cl)) cls 591 592 fun perturbClauses () = app perturbClause cls 593 594 val () = funpow n perturbClauses () 595 in 596 M 597 end; 598 599val groupAxioms = 600 [LS[`0 + $x = $x`], 601 LS[`~$x + $x = 0`], 602 LS[`$x + $y + $z = $x + ($y + $z)`]]; 603 604val groupThms = 605 [LS[`$x + 0 = $x`], 606 LS[`$x + ~$x = 0`], 607 LS[`~~$x = $x`]]; 608 609fun newM fixed = Model.new {size = 8, fixed = fixed}; 610val M = pvM (newM Model.basicFixed); 611val () = checkModel M (groupAxioms @ groupThms); 612val M = pvM (perturbModel M groupAxioms 1000); 613val () = checkModel M (groupAxioms @ groupThms); 614val M = pvM (newM (Model.unionFixed Model.modularFixed Model.basicFixed)); 615val () = checkModel M (groupAxioms @ groupThms); 616 617(* ------------------------------------------------------------------------- *) 618val () = SAY "Checking the standard model"; 619(* ------------------------------------------------------------------------- *) 620 621fun ppPercentClause (r,cl) = 622 let 623 val ind = 6 624 625 val p = percentToString r 626 627 val fm = LiteralSet.disjoin cl 628 in 629 Print.consistentBlock ind 630 [Print.ppString p, 631 Print.ppString (nChars #" " (ind - size p)), 632 Formula.pp fm] 633 end; 634 635val standardModel = Model.new Model.default; 636 637fun checkStandardModelClause cl = 638 let 639 val {T,F} = Model.checkClause {maxChecks = SOME 1000} standardModel cl 640 val r = Real.fromInt T / Real.fromInt (T + F) 641 in 642 (r,cl) 643 end; 644 645val pvPCl = printval ppPercentClause 646 647(* Equality *) 648 649val cl = LS[`$x = $x`]; 650val _ = pvPCl (checkStandardModelClause cl); 651val cl = LS[`~($x = $y)`,`$y = $x`]; 652val _ = pvPCl (checkStandardModelClause cl); 653val cl = LS[`~($x = $y)`,`~($y = $z)`,`$x = $z`]; 654val _ = pvPCl (checkStandardModelClause cl); 655 656(* Projections *) 657 658val cl = LS[`project1 $x1 = $x1`]; 659val _ = pvPCl (checkStandardModelClause cl); 660val cl = LS[`project1 $x1 $x2 = $x1`]; 661val _ = pvPCl (checkStandardModelClause cl); 662val cl = LS[`project2 $x1 $x2 = $x2`]; 663val _ = pvPCl (checkStandardModelClause cl); 664val cl = LS[`project1 $x1 $x2 $x3 = $x1`]; 665val _ = pvPCl (checkStandardModelClause cl); 666val cl = LS[`project2 $x1 $x2 $x3 = $x2`]; 667val _ = pvPCl (checkStandardModelClause cl); 668val cl = LS[`project3 $x1 $x2 $x3 = $x3`]; 669val _ = pvPCl (checkStandardModelClause cl); 670val cl = LS[`project1 $x1 $x2 $x3 $x4 = $x1`]; 671val _ = pvPCl (checkStandardModelClause cl); 672val cl = LS[`project2 $x1 $x2 $x3 $x4 = $x2`]; 673val _ = pvPCl (checkStandardModelClause cl); 674val cl = LS[`project3 $x1 $x2 $x3 $x4 = $x3`]; 675val _ = pvPCl (checkStandardModelClause cl); 676val cl = LS[`project4 $x1 $x2 $x3 $x4 = $x4`]; 677val _ = pvPCl (checkStandardModelClause cl); 678val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 = $x1`]; 679val _ = pvPCl (checkStandardModelClause cl); 680val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 = $x2`]; 681val _ = pvPCl (checkStandardModelClause cl); 682val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 = $x3`]; 683val _ = pvPCl (checkStandardModelClause cl); 684val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 = $x4`]; 685val _ = pvPCl (checkStandardModelClause cl); 686val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 = $x5`]; 687val _ = pvPCl (checkStandardModelClause cl); 688val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 = $x1`]; 689val _ = pvPCl (checkStandardModelClause cl); 690val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 = $x2`]; 691val _ = pvPCl (checkStandardModelClause cl); 692val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 = $x3`]; 693val _ = pvPCl (checkStandardModelClause cl); 694val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 = $x4`]; 695val _ = pvPCl (checkStandardModelClause cl); 696val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 = $x5`]; 697val _ = pvPCl (checkStandardModelClause cl); 698val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 = $x6`]; 699val _ = pvPCl (checkStandardModelClause cl); 700val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x1`]; 701val _ = pvPCl (checkStandardModelClause cl); 702val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x2`]; 703val _ = pvPCl (checkStandardModelClause cl); 704val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x3`]; 705val _ = pvPCl (checkStandardModelClause cl); 706val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x4`]; 707val _ = pvPCl (checkStandardModelClause cl); 708val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x5`]; 709val _ = pvPCl (checkStandardModelClause cl); 710val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x6`]; 711val _ = pvPCl (checkStandardModelClause cl); 712val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 = $x7`]; 713val _ = pvPCl (checkStandardModelClause cl); 714val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x1`]; 715val _ = pvPCl (checkStandardModelClause cl); 716val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x2`]; 717val _ = pvPCl (checkStandardModelClause cl); 718val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x3`]; 719val _ = pvPCl (checkStandardModelClause cl); 720val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x4`]; 721val _ = pvPCl (checkStandardModelClause cl); 722val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x5`]; 723val _ = pvPCl (checkStandardModelClause cl); 724val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x6`]; 725val _ = pvPCl (checkStandardModelClause cl); 726val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x7`]; 727val _ = pvPCl (checkStandardModelClause cl); 728val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 = $x8`]; 729val _ = pvPCl (checkStandardModelClause cl); 730val cl = LS[`project1 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x1`]; 731val _ = pvPCl (checkStandardModelClause cl); 732val cl = LS[`project2 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x2`]; 733val _ = pvPCl (checkStandardModelClause cl); 734val cl = LS[`project3 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x3`]; 735val _ = pvPCl (checkStandardModelClause cl); 736val cl = LS[`project4 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x4`]; 737val _ = pvPCl (checkStandardModelClause cl); 738val cl = LS[`project5 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x5`]; 739val _ = pvPCl (checkStandardModelClause cl); 740val cl = LS[`project6 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x6`]; 741val _ = pvPCl (checkStandardModelClause cl); 742val cl = LS[`project7 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x7`]; 743val _ = pvPCl (checkStandardModelClause cl); 744val cl = LS[`project8 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x8`]; 745val _ = pvPCl (checkStandardModelClause cl); 746val cl = LS[`project9 $x1 $x2 $x3 $x4 $x5 $x6 $x7 $x8 $x9 = $x9`]; 747val _ = pvPCl (checkStandardModelClause cl); 748 749(* Arithmetic *) 750 751(* Zero *) 752val cl = LS[`~isZero $x`,`$x = 0`]; 753val _ = pvPCl (checkStandardModelClause cl); 754val cl = LS[`isZero $x`,`~($x = 0)`]; 755val _ = pvPCl (checkStandardModelClause cl); 756 757(* Positive numerals *) 758val cl = LS[`0 + 1 = 1`]; 759val _ = pvPCl (checkStandardModelClause cl); 760val cl = LS[`1 + 1 = 2`]; 761val _ = pvPCl (checkStandardModelClause cl); 762val cl = LS[`2 + 1 = 3`]; 763val _ = pvPCl (checkStandardModelClause cl); 764val cl = LS[`3 + 1 = 4`]; 765val _ = pvPCl (checkStandardModelClause cl); 766val cl = LS[`4 + 1 = 5`]; 767val _ = pvPCl (checkStandardModelClause cl); 768val cl = LS[`5 + 1 = 6`]; 769val _ = pvPCl (checkStandardModelClause cl); 770val cl = LS[`6 + 1 = 7`]; 771val _ = pvPCl (checkStandardModelClause cl); 772val cl = LS[`7 + 1 = 8`]; 773val _ = pvPCl (checkStandardModelClause cl); 774val cl = LS[`8 + 1 = 9`]; 775val _ = pvPCl (checkStandardModelClause cl); 776val cl = LS[`9 + 1 = 10`]; 777val _ = pvPCl (checkStandardModelClause cl); 778 779(* Negative numerals *) 780val cl = LS[`~1 = negative1`]; 781val _ = pvPCl (checkStandardModelClause cl); 782val cl = LS[`~2 = negative2`]; 783val _ = pvPCl (checkStandardModelClause cl); 784val cl = LS[`~3 = negative3`]; 785val _ = pvPCl (checkStandardModelClause cl); 786val cl = LS[`~4 = negative4`]; 787val _ = pvPCl (checkStandardModelClause cl); 788val cl = LS[`~5 = negative5`]; 789val _ = pvPCl (checkStandardModelClause cl); 790val cl = LS[`~6 = negative6`]; 791val _ = pvPCl (checkStandardModelClause cl); 792val cl = LS[`~7 = negative7`]; 793val _ = pvPCl (checkStandardModelClause cl); 794val cl = LS[`~8 = negative8`]; 795val _ = pvPCl (checkStandardModelClause cl); 796val cl = LS[`~9 = negative9`]; 797val _ = pvPCl (checkStandardModelClause cl); 798val cl = LS[`~10 = negative10`]; 799val _ = pvPCl (checkStandardModelClause cl); 800 801(* Addition *) 802val cl = LS[`0 + $x = $x`]; 803val _ = pvPCl (checkStandardModelClause cl); 804val cl = LS[`$x + $y = $y + $x`]; 805val _ = pvPCl (checkStandardModelClause cl); 806val cl = LS[`$x + ($y + $z) = ($x + $y) + $z`]; 807val _ = pvPCl (checkStandardModelClause cl); 808 809(* Negation *) 810val cl = LS[`~$x + $x = 0`]; 811val _ = pvPCl (checkStandardModelClause cl); 812val cl = LS[`~~$x = $x`]; 813val _ = pvPCl (checkStandardModelClause cl); 814 815(* Subtraction *) 816val cl = LS[`$x - $y = $x + ~$y`]; 817val _ = pvPCl (checkStandardModelClause cl); 818 819(* Successor *) 820val cl = LS[`suc $x = $x + 1`]; 821val _ = pvPCl (checkStandardModelClause cl); 822 823(* Predecessor *) 824val cl = LS[`pre $x = $x - 1`]; 825val _ = pvPCl (checkStandardModelClause cl); 826 827(* Ordering *) 828val cl = LS[`$x <= $x`]; 829val _ = pvPCl (checkStandardModelClause cl); 830val cl = LS[`~($x <= $y)`,`~($y <= $z)`,`$x <= $z`]; 831val _ = pvPCl (checkStandardModelClause cl); 832val cl = LS[`~($x <= $y)`,`~($y <= $x)`,`$x = $y`]; 833val _ = pvPCl (checkStandardModelClause cl); 834val cl = LS[`0 <= $x`]; 835val _ = pvPCl (checkStandardModelClause cl); 836val cl = LS[`~($x >= $y)`,`$y <= $x`]; 837val _ = pvPCl (checkStandardModelClause cl); 838val cl = LS[`$x >= $y`,`~($y <= $x)`]; 839val _ = pvPCl (checkStandardModelClause cl); 840val cl = LS[`$x > $y`,`$x <= $y`]; 841val _ = pvPCl (checkStandardModelClause cl); 842val cl = LS[`~($x > $y)`,`~($x <= $y)`]; 843val _ = pvPCl (checkStandardModelClause cl); 844val cl = LS[`$x < $y`,`$y <= $x`]; 845val _ = pvPCl (checkStandardModelClause cl); 846val cl = LS[`~($x < $y)`,`~($y <= $x)`]; 847val _ = pvPCl (checkStandardModelClause cl); 848val cl = LS[`$x = 0`,`~($x <= $y)`,`~$y <= ~$x`]; 849val _ = pvPCl (checkStandardModelClause cl); 850 851(* Multiplication *) 852val cl = LS[`1 * $x = $x`]; 853val _ = pvPCl (checkStandardModelClause cl); 854val cl = LS[`0 * $x = 0`]; 855val _ = pvPCl (checkStandardModelClause cl); 856val cl = LS[`$x * $y = $y * $x`]; 857val _ = pvPCl (checkStandardModelClause cl); 858val cl = LS[`$x * ($y * $z) = ($x * $y) * $z`]; 859val _ = pvPCl (checkStandardModelClause cl); 860val cl = LS[`$x * ($y + $z) = ($x * $y) + ($x * $z)`]; 861val _ = pvPCl (checkStandardModelClause cl); 862val cl = LS[`$x * ~$y = ~($x * $y)`]; 863val _ = pvPCl (checkStandardModelClause cl); 864 865(* Division *) 866val cl = LS[`$y = 0`,`$x mod $y < $y`]; 867val _ = pvPCl (checkStandardModelClause cl); 868val cl = LS[`$y * ($x div $y) + $x mod $y = $x`]; 869val _ = pvPCl (checkStandardModelClause cl); 870 871(* Exponentiation *) 872val cl = LS[`exp $x 0 = 1`]; 873val _ = pvPCl (checkStandardModelClause cl); 874val cl = LS[`$y = 0`,`exp $x $y = $x * exp $x (pre $y)`]; 875val _ = pvPCl (checkStandardModelClause cl); 876 877(* Divides *) 878val cl = LS[`divides $x $x`]; 879val _ = pvPCl (checkStandardModelClause cl); 880val cl = LS[`~(divides $x $y)`,`~(divides $y $z)`,`divides $x $z`]; 881val _ = pvPCl (checkStandardModelClause cl); 882val cl = LS[`~(divides $x $y)`,`~(divides $y $x)`,`$x = $y`]; 883val _ = pvPCl (checkStandardModelClause cl); 884val cl = LS[`divides 1 $x`]; 885val _ = pvPCl (checkStandardModelClause cl); 886val cl = LS[`divides $x 0`]; 887val _ = pvPCl (checkStandardModelClause cl); 888 889(* Even and odd *) 890val cl = LS[`even 0`]; 891val _ = pvPCl (checkStandardModelClause cl); 892val cl = LS[`$x = 0`,`~(even (pre $x))`,`odd $x`]; 893val _ = pvPCl (checkStandardModelClause cl); 894val cl = LS[`$x = 0`,`~(odd (pre $x))`,`even $x`]; 895val _ = pvPCl (checkStandardModelClause cl); 896 897(* Sets *) 898 899(* The empty set *) 900val cl = LS[`~member $x empty`]; 901val _ = pvPCl (checkStandardModelClause cl); 902 903(* The universal set *) 904val cl = LS[`member $x universe`]; 905val _ = pvPCl (checkStandardModelClause cl); 906 907(* Complement *) 908val cl = LS[`member $x $y`,`member $x (complement $y)`]; 909val _ = pvPCl (checkStandardModelClause cl); 910val cl = LS[`~(member $x $y)`,`~member $x (complement $y)`]; 911val _ = pvPCl (checkStandardModelClause cl); 912val cl = LS[`complement (complement $x) = $x`]; 913val _ = pvPCl (checkStandardModelClause cl); 914val cl = LS[`complement empty = universe`]; 915val _ = pvPCl (checkStandardModelClause cl); 916val cl = LS[`complement universe = empty`]; 917val _ = pvPCl (checkStandardModelClause cl); 918 919(* The subset relation *) 920val cl = LS[`subset $x $x`]; 921val _ = pvPCl (checkStandardModelClause cl); 922val cl = LS[`~subset $x $y`,`~subset $y $z`,`subset $x $z`]; 923val _ = pvPCl (checkStandardModelClause cl); 924val cl = LS[`~subset $x $y`,`~subset $y $x`,`$x = $y`]; 925val _ = pvPCl (checkStandardModelClause cl); 926val cl = LS[`subset empty $x`]; 927val _ = pvPCl (checkStandardModelClause cl); 928val cl = LS[`subset $x universe`]; 929val _ = pvPCl (checkStandardModelClause cl); 930val cl = LS[`~subset $x $y`,`subset (complement $y) (complement $x)`]; 931val _ = pvPCl (checkStandardModelClause cl); 932val cl = LS[`~member $x $y`,`~subset $y $z`,`member $x $z`]; 933val _ = pvPCl (checkStandardModelClause cl); 934 935(* Union *) 936val cl = LS[`union $x $y = union $y $x`]; 937val _ = pvPCl (checkStandardModelClause cl); 938val cl = LS[`union $x (union $y $z) = union (union $x $y) $z`]; 939val _ = pvPCl (checkStandardModelClause cl); 940val cl = LS[`union empty $x = $x`]; 941val _ = pvPCl (checkStandardModelClause cl); 942val cl = LS[`union universe $x = universe`]; 943val _ = pvPCl (checkStandardModelClause cl); 944val cl = LS[`subset $x (union $x $y)`]; 945val _ = pvPCl (checkStandardModelClause cl); 946val cl = LS[`~member $x (union $y $z)`,`member $x $y`,`member $x $z`]; 947val _ = pvPCl (checkStandardModelClause cl); 948 949(* Intersection *) 950val cl = LS[`intersect $x $y = 951 complement (union (complement $x) (complement $y))`]; 952val _ = pvPCl (checkStandardModelClause cl); 953val cl = LS[`subset (intersect $x $y) $x`]; 954val _ = pvPCl (checkStandardModelClause cl); 955 956(* Difference *) 957val cl = LS[`difference $x $y = intersect $x (complement $y)`]; 958val _ = pvPCl (checkStandardModelClause cl); 959 960(* Symmetric difference *) 961val cl = LS[`symmetricDifference $x $y = 962 union (difference $x $y) (difference $y $x)`]; 963val _ = pvPCl (checkStandardModelClause cl); 964 965(* Insert *) 966val cl = LS[`member $x (insert $x $y)`]; 967val _ = pvPCl (checkStandardModelClause cl); 968 969(* Singleton *) 970val cl = LS[`singleton $x = (insert $x empty)`]; 971val _ = pvPCl (checkStandardModelClause cl); 972 973(* Cardinality *) 974val cl = LS[`card empty = 0`]; 975val _ = pvPCl (checkStandardModelClause cl); 976val cl = LS[`member $x $y`,`card (insert $x $y) = suc (card $y)`]; 977val _ = pvPCl (checkStandardModelClause cl); 978 979(* Lists *) 980 981(* Nil *) 982val cl = LS[`null nil`]; 983val _ = pvPCl (checkStandardModelClause cl); 984val cl = LS[`~null $x`, `$x = nil`]; 985val _ = pvPCl (checkStandardModelClause cl); 986 987(* Cons *) 988val cl = LS[`~(nil = $x :: $y)`]; 989val _ = pvPCl (checkStandardModelClause cl); 990 991(* Append *) 992val cl = LS[`$x @ ($y @ $z) = ($x @ $y) @ $z`]; 993val _ = pvPCl (checkStandardModelClause cl); 994val cl = LS[`nil @ $x = $x`]; 995val _ = pvPCl (checkStandardModelClause cl); 996val cl = LS[`$x @ nil = $x`]; 997val _ = pvPCl (checkStandardModelClause cl); 998 999(* Length *) 1000val cl = LS[`length nil = 0`]; 1001val _ = pvPCl (checkStandardModelClause cl); 1002val cl = LS[`length ($x :: $y) >= length $y`]; 1003val _ = pvPCl (checkStandardModelClause cl); 1004val cl = LS[`length ($x @ $y) >= length $x`]; 1005val _ = pvPCl (checkStandardModelClause cl); 1006val cl = LS[`length ($x @ $y) >= length $y`]; 1007val _ = pvPCl (checkStandardModelClause cl); 1008 1009(* Tail *) 1010val cl = LS[`null $x`,`suc (length (tail $x)) = length $x`]; 1011val _ = pvPCl (checkStandardModelClause cl); 1012 1013(* ------------------------------------------------------------------------- *) 1014val () = SAY "Clauses"; 1015(* ------------------------------------------------------------------------- *) 1016 1017val cl = pvCl (CL[`P $x`,`P $y`]); 1018val _ = pvLits (Clause.largestLiterals cl); 1019val _ = pvCls (Clause.factor cl); 1020val cl = pvCl (CL[`P $x`,`~P (f $x)`]); 1021val _ = pvLits (Clause.largestLiterals cl); 1022val cl = pvCl (CL[`$x = $y`,`f $y = f $x`]); 1023val _ = pvLits (Clause.largestLiterals cl); 1024val cl = pvCl (CL[`$x = f $y`,`f $x = $y`]); 1025val _ = pvLits (Clause.largestLiterals cl); 1026val cl = pvCl (CL[`s = a`,`s = b`,`h b c`]); 1027val _ = pvLits (Clause.largestLiterals cl); 1028val cl = pvCl (CL[`a = a`,`a = b`,`h b c`]); 1029val _ = pvLits (Clause.largestLiterals cl); 1030 1031(* Test cases contributed by Larry Paulson *) 1032 1033local 1034 val lnFnName = Name.fromString "ln" 1035 and expFnName = Name.fromString "exp" 1036 and divFnName = Name.fromString "/" 1037 1038 val leRelName = Name.fromString "<"; 1039 1040 fun weight na = 1041 case na of 1042 (n,1) => 1043 if Name.equal n lnFnName then 500 1044 else if Name.equal n expFnName then 500 1045 else 1 1046 | (n,2) => 1047 if Name.equal n divFnName then 50 1048 else if Name.equal n leRelName then 20 1049 else 1 1050 | _ => 1; 1051 1052 val ordering = 1053 {weight = weight, precedence = #precedence KnuthBendixOrder.default}; 1054 1055 val clauseParameters = 1056 {ordering = ordering, 1057 orderLiterals = Clause.UnsignedLiteralOrder, 1058 orderTerms = true}; 1059in 1060 val LcpCL = mkCl clauseParameters o AX; 1061end; 1062 1063val cl = pvCl (LcpCL[`~($y <= (2 + (2 * $x + pow $x 2)) / 2)`, `~(0 <= $x)`, 1064 `$y <= exp $x`]); 1065val _ = pvLits (Clause.largestLiterals cl); 1066 1067(* ------------------------------------------------------------------------- *) 1068val () = SAY "Syntax checking the problem sets"; 1069(* ------------------------------------------------------------------------- *) 1070 1071local 1072 fun same n = raise Fail ("Two goals called " ^ n); 1073 1074 fun dup n n' = 1075 raise Fail ("Goal " ^ n' ^ " is probable duplicate of " ^ n); 1076 1077 fun quot fm = 1078 let 1079 fun f (v,s) = Subst.insert s (v,V"_") 1080 1081 val sub = NameSet.foldl f Subst.empty (Formula.freeVars fm) 1082 in 1083 Formula.subst sub fm 1084 end; 1085 1086 val quot_clauses = 1087 Formula.listMkConj o sort Formula.compare o 1088 List.map (quot o snd o Formula.stripForall) o Formula.stripConj; 1089 1090 fun quotient (Formula.Imp (a, Formula.Imp (b, Formula.False))) = 1091 Formula.Imp (quot_clauses a, Formula.Imp (quot_clauses b, Formula.False)) 1092 | quotient fm = fm; 1093 1094 fun check ({name,goal,...}, acc) = 1095 let 1096 val g = prep goal 1097 val p = 1098 Formula.fromString g 1099 handle Parse.NoParse => 1100 raise Error ("failed to parse problem " ^ name) 1101 1102 val () = 1103 case List.find (fn (n,_) => n = name) acc of NONE => () 1104 | SOME _ => same name 1105 1106 val () = 1107 case List.find (fn (_,x) => Formula.equal x p) acc of NONE => () 1108 | SOME (n,_) => dup n name 1109 1110 val _ = 1111 test_fun equal I g (mini_print (!Print.lineLength) p) 1112 handle e => 1113 (TextIO.print ("Error in problem " ^ name ^ "\n\n"); 1114 raise e) 1115 in 1116 (name,p) :: acc 1117 end; 1118in 1119 fun check_syntax (p : problem list) = 1120 let 1121 val _ = List.foldl check [] p 1122 in 1123 TextIO.print "ok\n\n" 1124 end; 1125end; 1126 1127val () = check_syntax problems; 1128 1129(* ------------------------------------------------------------------------- *) 1130val () = SAY "Parsing TPTP problems"; 1131(* ------------------------------------------------------------------------- *) 1132 1133fun tptp f = 1134 let 1135 val () = TextIO.print ("parsing " ^ f ^ "... ") 1136 val filename = "tptp/" ^ f ^ ".tptp" 1137 val mapping = Tptp.defaultMapping 1138 val goal = Tptp.goal (Tptp.read {filename = filename, mapping = mapping}) 1139 val () = TextIO.print "ok\n" 1140 in 1141 pvFm goal 1142 end; 1143 1144val _ = tptp "PUZ001-1"; 1145val _ = tptp "NO_FORMULAS"; 1146val _ = tptp "SEPARATED_COMMENTS"; 1147val _ = tptp "NUMBERED_FORMULAS"; 1148val _ = tptp "DEFINED_TERMS"; 1149val _ = tptp "SYSTEM_TERMS"; 1150val _ = tptp "QUOTED_TERMS"; 1151val _ = tptp "QUOTED_TERMS_IDENTITY"; 1152val _ = tptp "QUOTED_TERMS_DIFFERENT"; 1153val _ = tptp "QUOTED_TERMS_SPECIAL"; 1154val _ = tptp "RENAMING_VARIABLES"; 1155val _ = tptp "MIXED_PROBLEM"; 1156val _ = tptp "BLOCK_COMMENTS"; 1157 1158(* ------------------------------------------------------------------------- *) 1159val () = SAY "The TPTP finite model"; 1160(* ------------------------------------------------------------------------- *) 1161 1162val _ = printval (Tptp.ppFixedMap Tptp.defaultMapping) Tptp.defaultFixedMap; 1163