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