1 (* ========================================================================= *) |
|
2 (* RANDOM FINITE MODELS *) |
|
3 (* Copyright (c) 2003-2007 Joe Hurd, distributed under the BSD License *) |
|
4 (* ========================================================================= *) |
|
5 |
|
6 structure Model :> Model = |
|
7 struct |
|
8 |
|
9 open Useful; |
|
10 |
|
11 (* ------------------------------------------------------------------------- *) |
|
12 (* Helper functions. *) |
|
13 (* ------------------------------------------------------------------------- *) |
|
14 |
|
15 fun intExp x y = exp op* x y 1; |
|
16 |
|
17 fun natFromString "" = NONE |
|
18 | natFromString "0" = SOME 0 |
|
19 | natFromString s = |
|
20 case charToInt (String.sub (s,0)) of |
|
21 NONE => NONE |
|
22 | SOME 0 => NONE |
|
23 | SOME d => |
|
24 let |
|
25 fun parse 0 _ acc = SOME acc |
|
26 | parse n i acc = |
|
27 case charToInt (String.sub (s,i)) of |
|
28 NONE => NONE |
|
29 | SOME d => parse (n - 1) (i + 1) (10 * acc + d) |
|
30 in |
|
31 parse (size s - 1) 1 d |
|
32 end; |
|
33 |
|
34 fun projection (_,[]) = NONE |
|
35 | projection ("#1", x :: _) = SOME x |
|
36 | projection ("#2", _ :: x :: _) = SOME x |
|
37 | projection ("#3", _ :: _ :: x :: _) = SOME x |
|
38 | projection (func,args) = |
|
39 let |
|
40 val f = size func |
|
41 and n = length args |
|
42 |
|
43 val p = |
|
44 if f < 2 orelse n <= 3 orelse String.sub (func,0) <> #"#" then NONE |
|
45 else if f = 2 then |
|
46 (case charToInt (String.sub (func,1)) of |
|
47 NONE => NONE |
|
48 | p as SOME d => if d <= 3 then NONE else p) |
|
49 else if (n < intExp 10 (f - 2) handle Overflow => true) then NONE |
|
50 else |
|
51 (natFromString (String.extract (func,1,NONE)) |
|
52 handle Overflow => NONE) |
|
53 in |
|
54 case p of |
|
55 NONE => NONE |
|
56 | SOME k => if k > n then NONE else SOME (List.nth (args, k - 1)) |
|
57 end; |
|
58 |
|
59 (* ------------------------------------------------------------------------- *) |
|
60 (* The parts of the model that are fixed. *) |
|
61 (* Note: a model of size N has integer elements 0...N-1. *) |
|
62 (* ------------------------------------------------------------------------- *) |
|
63 |
|
64 type fixedModel = |
|
65 {functions : (Term.functionName * int list) -> int option, |
|
66 relations : (Atom.relationName * int list) -> bool option}; |
|
67 |
|
68 type fixed = {size : int} -> fixedModel |
|
69 |
|
70 fun fixedMerge fixed1 fixed2 parm = |
|
71 let |
|
72 val {functions = f1, relations = r1} = fixed1 parm |
|
73 and {functions = f2, relations = r2} = fixed2 parm |
|
74 |
|
75 fun functions x = case f2 x of NONE => f1 x | s => s |
|
76 |
|
77 fun relations x = case r2 x of NONE => r1 x | s => s |
|
78 in |
|
79 {functions = functions, relations = relations} |
|
80 end; |
|
81 |
|
82 fun fixedMergeList [] = raise Bug "fixedMergeList: empty" |
|
83 | fixedMergeList (f :: l) = foldl (uncurry fixedMerge) f l; |
|
84 |
|
85 fun fixedPure {size = _} = |
|
86 let |
|
87 fun functions (":",[x,_]) = SOME x |
|
88 | functions _ = NONE |
|
89 |
|
90 fun relations (rel,[x,y]) = |
|
91 if (rel,2) = Atom.eqRelation then SOME (x = y) else NONE |
|
92 | relations _ = NONE |
|
93 in |
|
94 {functions = functions, relations = relations} |
|
95 end; |
|
96 |
|
97 fun fixedBasic {size = _} = |
|
98 let |
|
99 fun functions ("id",[x]) = SOME x |
|
100 | functions ("fst",[x,_]) = SOME x |
|
101 | functions ("snd",[_,x]) = SOME x |
|
102 | functions func_args = projection func_args |
|
103 |
|
104 fun relations ("<>",[x,y]) = SOME (x <> y) |
|
105 | relations _ = NONE |
|
106 in |
|
107 {functions = functions, relations = relations} |
|
108 end; |
|
109 |
|
110 fun fixedModulo {size = N} = |
|
111 let |
|
112 fun mod_N k = k mod N |
|
113 |
|
114 val one = mod_N 1 |
|
115 |
|
116 fun mult (x,y) = mod_N (x * y) |
|
117 |
|
118 fun divides_N 0 = false |
|
119 | divides_N x = N mod x = 0 |
|
120 |
|
121 val even_N = divides_N 2 |
|
122 |
|
123 fun functions (numeral,[]) = |
|
124 Option.map mod_N (natFromString numeral handle Overflow => NONE) |
|
125 | functions ("suc",[x]) = SOME (if x = N - 1 then 0 else x + 1) |
|
126 | functions ("pre",[x]) = SOME (if x = 0 then N - 1 else x - 1) |
|
127 | functions ("~",[x]) = SOME (if x = 0 then 0 else N - x) |
|
128 | functions ("+",[x,y]) = SOME (mod_N (x + y)) |
|
129 | functions ("-",[x,y]) = SOME (if x < y then N + x - y else x - y) |
|
130 | functions ("*",[x,y]) = SOME (mult (x,y)) |
|
131 | functions ("exp",[x,y]) = SOME (exp mult x y one) |
|
132 | functions ("div",[x,y]) = if divides_N y then SOME (x div y) else NONE |
|
133 | functions ("mod",[x,y]) = if divides_N y then SOME (x mod y) else NONE |
|
134 | functions _ = NONE |
|
135 |
|
136 fun relations ("is_0",[x]) = SOME (x = 0) |
|
137 | relations ("divides",[x,y]) = |
|
138 if x = 0 then SOME (y = 0) |
|
139 else if divides_N x then SOME (y mod x = 0) else NONE |
|
140 | relations ("even",[x]) = if even_N then SOME (x mod 2 = 0) else NONE |
|
141 | relations ("odd",[x]) = if even_N then SOME (x mod 2 = 1) else NONE |
|
142 | relations _ = NONE |
|
143 in |
|
144 {functions = functions, relations = relations} |
|
145 end; |
|
146 |
|
147 local |
|
148 datatype onum = ONeg | ONum of int | OInf; |
|
149 |
|
150 val zero = ONum 0 |
|
151 and one = ONum 1 |
|
152 and two = ONum 2; |
|
153 |
|
154 fun suc (ONum x) = ONum (x + 1) |
|
155 | suc v = v; |
|
156 |
|
157 fun pre (ONum 0) = ONeg |
|
158 | pre (ONum x) = ONum (x - 1) |
|
159 | pre v = v; |
|
160 |
|
161 fun neg ONeg = NONE |
|
162 | neg (n as ONum 0) = SOME n |
|
163 | neg _ = SOME ONeg; |
|
164 |
|
165 fun add ONeg ONeg = SOME ONeg |
|
166 | add ONeg (ONum y) = if y = 0 then SOME ONeg else NONE |
|
167 | add ONeg OInf = NONE |
|
168 | add (ONum x) ONeg = if x = 0 then SOME ONeg else NONE |
|
169 | add (ONum x) (ONum y) = SOME (ONum (x + y)) |
|
170 | add (ONum _) OInf = SOME OInf |
|
171 | add OInf ONeg = NONE |
|
172 | add OInf (ONum _) = SOME OInf |
|
173 | add OInf OInf = SOME OInf; |
|
174 |
|
175 fun sub ONeg ONeg = NONE |
|
176 | sub ONeg (ONum _) = SOME ONeg |
|
177 | sub ONeg OInf = SOME ONeg |
|
178 | sub (ONum _) ONeg = NONE |
|
179 | sub (ONum x) (ONum y) = SOME (if x < y then ONeg else ONum (x - y)) |
|
180 | sub (ONum _) OInf = SOME ONeg |
|
181 | sub OInf ONeg = SOME OInf |
|
182 | sub OInf (ONum y) = if y = 0 then SOME OInf else NONE |
|
183 | sub OInf OInf = NONE; |
|
184 |
|
185 fun mult ONeg ONeg = NONE |
|
186 | mult ONeg (ONum y) = SOME (if y = 0 then zero else ONeg) |
|
187 | mult ONeg OInf = SOME ONeg |
|
188 | mult (ONum x) ONeg = SOME (if x = 0 then zero else ONeg) |
|
189 | mult (ONum x) (ONum y) = SOME (ONum (x * y)) |
|
190 | mult (ONum x) OInf = SOME (if x = 0 then zero else OInf) |
|
191 | mult OInf ONeg = SOME ONeg |
|
192 | mult OInf (ONum y) = SOME (if y = 0 then zero else OInf) |
|
193 | mult OInf OInf = SOME OInf; |
|
194 |
|
195 fun exp ONeg ONeg = NONE |
|
196 | exp ONeg (ONum y) = |
|
197 if y = 0 then SOME one else if y mod 2 = 0 then NONE else SOME ONeg |
|
198 | exp ONeg OInf = NONE |
|
199 | exp (ONum x) ONeg = NONE |
|
200 | exp (ONum x) (ONum y) = SOME (ONum (intExp x y) handle Overflow => OInf) |
|
201 | exp (ONum x) OInf = |
|
202 SOME (if x = 0 then zero else if x = 1 then one else OInf) |
|
203 | exp OInf ONeg = NONE |
|
204 | exp OInf (ONum y) = SOME (if y = 0 then one else OInf) |
|
205 | exp OInf OInf = SOME OInf; |
|
206 |
|
207 fun odiv ONeg ONeg = NONE |
|
208 | odiv ONeg (ONum y) = if y = 1 then SOME ONeg else NONE |
|
209 | odiv ONeg OInf = NONE |
|
210 | odiv (ONum _) ONeg = NONE |
|
211 | odiv (ONum x) (ONum y) = if y = 0 then NONE else SOME (ONum (x div y)) |
|
212 | odiv (ONum _) OInf = SOME zero |
|
213 | odiv OInf ONeg = NONE |
|
214 | odiv OInf (ONum y) = if y = 1 then SOME OInf else NONE |
|
215 | odiv OInf OInf = NONE; |
|
216 |
|
217 fun omod ONeg ONeg = NONE |
|
218 | omod ONeg (ONum y) = if y = 1 then SOME zero else NONE |
|
219 | omod ONeg OInf = NONE |
|
220 | omod (ONum _) ONeg = NONE |
|
221 | omod (ONum x) (ONum y) = if y = 0 then NONE else SOME (ONum (x mod y)) |
|
222 | omod (x as ONum _) OInf = SOME x |
|
223 | omod OInf ONeg = NONE |
|
224 | omod OInf (ONum y) = if y = 1 then SOME OInf else NONE |
|
225 | omod OInf OInf = NONE; |
|
226 |
|
227 fun le ONeg ONeg = NONE |
|
228 | le ONeg (ONum y) = SOME true |
|
229 | le ONeg OInf = SOME true |
|
230 | le (ONum _) ONeg = SOME false |
|
231 | le (ONum x) (ONum y) = SOME (x <= y) |
|
232 | le (ONum _) OInf = SOME true |
|
233 | le OInf ONeg = SOME false |
|
234 | le OInf (ONum _) = SOME false |
|
235 | le OInf OInf = NONE; |
|
236 |
|
237 fun lt x y = Option.map not (le y x); |
|
238 |
|
239 fun ge x y = le y x; |
|
240 |
|
241 fun gt x y = lt y x; |
|
242 |
|
243 fun divides ONeg ONeg = NONE |
|
244 | divides ONeg (ONum y) = if y = 0 then SOME true else NONE |
|
245 | divides ONeg OInf = NONE |
|
246 | divides (ONum x) ONeg = |
|
247 if x = 0 then SOME false else if x = 1 then SOME true else NONE |
|
248 | divides (ONum x) (ONum y) = SOME (Useful.divides x y) |
|
249 | divides (ONum x) OInf = |
|
250 if x = 0 then SOME false else if x = 1 then SOME true else NONE |
|
251 | divides OInf ONeg = NONE |
|
252 | divides OInf (ONum y) = SOME (y = 0) |
|
253 | divides OInf OInf = NONE; |
|
254 |
|
255 fun even n = divides two n; |
|
256 |
|
257 fun odd n = Option.map not (even n); |
|
258 |
|
259 fun fixedOverflow mk_onum dest_onum = |
|
260 let |
|
261 fun partial_dest_onum NONE = NONE |
|
262 | partial_dest_onum (SOME n) = dest_onum n |
|
263 |
|
264 fun functions (numeral,[]) = |
|
265 (case (natFromString numeral handle Overflow => NONE) of |
|
266 NONE => NONE |
|
267 | SOME n => dest_onum (ONum n)) |
|
268 | functions ("suc",[x]) = dest_onum (suc (mk_onum x)) |
|
269 | functions ("pre",[x]) = dest_onum (pre (mk_onum x)) |
|
270 | functions ("~",[x]) = partial_dest_onum (neg (mk_onum x)) |
|
271 | functions ("+",[x,y]) = |
|
272 partial_dest_onum (add (mk_onum x) (mk_onum y)) |
|
273 | functions ("-",[x,y]) = |
|
274 partial_dest_onum (sub (mk_onum x) (mk_onum y)) |
|
275 | functions ("*",[x,y]) = |
|
276 partial_dest_onum (mult (mk_onum x) (mk_onum y)) |
|
277 | functions ("exp",[x,y]) = |
|
278 partial_dest_onum (exp (mk_onum x) (mk_onum y)) |
|
279 | functions ("div",[x,y]) = |
|
280 partial_dest_onum (odiv (mk_onum x) (mk_onum y)) |
|
281 | functions ("mod",[x,y]) = |
|
282 partial_dest_onum (omod (mk_onum x) (mk_onum y)) |
|
283 | functions _ = NONE |
|
284 |
|
285 fun relations ("is_0",[x]) = SOME (mk_onum x = zero) |
|
286 | relations ("<=",[x,y]) = le (mk_onum x) (mk_onum y) |
|
287 | relations ("<",[x,y]) = lt (mk_onum x) (mk_onum y) |
|
288 | relations (">=",[x,y]) = ge (mk_onum x) (mk_onum y) |
|
289 | relations (">",[x,y]) = gt (mk_onum x) (mk_onum y) |
|
290 | relations ("divides",[x,y]) = divides (mk_onum x) (mk_onum y) |
|
291 | relations ("even",[x]) = even (mk_onum x) |
|
292 | relations ("odd",[x]) = odd (mk_onum x) |
|
293 | relations _ = NONE |
|
294 in |
|
295 {functions = functions, relations = relations} |
|
296 end; |
|
297 in |
|
298 fun fixedOverflowNum {size = N} = |
|
299 let |
|
300 val oinf = N - 1 |
|
301 |
|
302 fun mk_onum x = if x = oinf then OInf else ONum x |
|
303 |
|
304 fun dest_onum ONeg = NONE |
|
305 | dest_onum (ONum x) = SOME (if x < oinf then x else oinf) |
|
306 | dest_onum OInf = SOME oinf |
|
307 in |
|
308 fixedOverflow mk_onum dest_onum |
|
309 end; |
|
310 |
|
311 fun fixedOverflowInt {size = N} = |
|
312 let |
|
313 val oinf = N - 2 |
|
314 val oneg = N - 1 |
|
315 |
|
316 fun mk_onum x = |
|
317 if x = oneg then ONeg else if x = oinf then OInf else ONum x |
|
318 |
|
319 fun dest_onum ONeg = SOME oneg |
|
320 | dest_onum (ONum x) = SOME (if x < oinf then x else oinf) |
|
321 | dest_onum OInf = SOME oinf |
|
322 in |
|
323 fixedOverflow mk_onum dest_onum |
|
324 end; |
|
325 end; |
|
326 |
|
327 fun fixedSet {size = N} = |
|
328 let |
|
329 val M = |
|
330 let |
|
331 fun f 0 acc = acc |
|
332 | f x acc = f (x div 2) (acc + 1) |
|
333 in |
|
334 f N 0 |
|
335 end |
|
336 |
|
337 val univ = IntSet.fromList (interval 0 M) |
|
338 |
|
339 val mk_set = |
|
340 let |
|
341 fun f _ s 0 = s |
|
342 | f k s x = |
|
343 let |
|
344 val s = if x mod 2 = 0 then s else IntSet.add s k |
|
345 in |
|
346 f (k + 1) s (x div 2) |
|
347 end |
|
348 in |
|
349 f 0 IntSet.empty |
|
350 end |
|
351 |
|
352 fun dest_set s = |
|
353 let |
|
354 fun f 0 x = x |
|
355 | f k x = |
|
356 let |
|
357 val k = k - 1 |
|
358 in |
|
359 f k (if IntSet.member k s then 2 * x + 1 else 2 * x) |
|
360 end |
|
361 |
|
362 val x = case IntSet.findr (K true) s of NONE => 0 | SOME k => f k 1 |
|
363 in |
|
364 if x < N then SOME x else NONE |
|
365 end |
|
366 |
|
367 fun functions ("empty",[]) = dest_set IntSet.empty |
|
368 | functions ("univ",[]) = dest_set univ |
|
369 | functions ("union",[x,y]) = |
|
370 dest_set (IntSet.union (mk_set x) (mk_set y)) |
|
371 | functions ("intersect",[x,y]) = |
|
372 dest_set (IntSet.intersect (mk_set x) (mk_set y)) |
|
373 | functions ("compl",[x]) = |
|
374 dest_set (IntSet.difference univ (mk_set x)) |
|
375 | functions ("card",[x]) = SOME (IntSet.size (mk_set x)) |
|
376 | functions _ = NONE |
|
377 |
|
378 fun relations ("in",[x,y]) = SOME (IntSet.member (x mod M) (mk_set y)) |
|
379 | relations ("subset",[x,y]) = |
|
380 SOME (IntSet.subset (mk_set x) (mk_set y)) |
|
381 | relations _ = NONE |
|
382 in |
|
383 {functions = functions, relations = relations} |
|
384 end; |
|
385 |
|
386 (* ------------------------------------------------------------------------- *) |
|
387 (* A type of random finite models. *) |
|
388 (* ------------------------------------------------------------------------- *) |
|
389 |
|
390 type parameters = {size : int, fixed : fixed}; |
|
391 |
|
392 datatype model = |
|
393 Model of |
|
394 {size : int, |
|
395 fixed : fixedModel, |
|
396 functions : (Term.functionName * int list, int) Map.map ref, |
|
397 relations : (Atom.relationName * int list, bool) Map.map ref}; |
|
398 |
|
399 local |
|
400 fun cmp ((n1,l1),(n2,l2)) = |
|
401 case String.compare (n1,n2) of |
|
402 LESS => LESS |
|
403 | EQUAL => lexCompare Int.compare (l1,l2) |
|
404 | GREATER => GREATER; |
|
405 in |
|
406 fun new {size = N, fixed} = |
|
407 Model |
|
408 {size = N, |
|
409 fixed = fixed {size = N}, |
|
410 functions = ref (Map.new cmp), |
|
411 relations = ref (Map.new cmp)}; |
|
412 end; |
|
413 |
|
414 fun size (Model {size = s, ...}) = s; |
|
415 |
|
416 (* ------------------------------------------------------------------------- *) |
|
417 (* Valuations. *) |
|
418 (* ------------------------------------------------------------------------- *) |
|
419 |
|
420 type valuation = int NameMap.map; |
|
421 |
|
422 val valuationEmpty : valuation = NameMap.new (); |
|
423 |
|
424 fun valuationRandom {size = N} vs = |
|
425 let |
|
426 fun f (v,V) = NameMap.insert V (v, Portable.randomInt N) |
|
427 in |
|
428 NameSet.foldl f valuationEmpty vs |
|
429 end; |
|
430 |
|
431 fun valuationFold {size = N} vs f = |
|
432 let |
|
433 val vs = NameSet.toList vs |
|
434 |
|
435 fun inc [] _ = NONE |
|
436 | inc (v :: l) V = |
|
437 case NameMap.peek V v of |
|
438 NONE => raise Bug "Model.valuationFold" |
|
439 | SOME k => |
|
440 let |
|
441 val k = if k = N - 1 then 0 else k + 1 |
|
442 val V = NameMap.insert V (v,k) |
|
443 in |
|
444 if k = 0 then inc l V else SOME V |
|
445 end |
|
446 |
|
447 val zero = foldl (fn (v,V) => NameMap.insert V (v,0)) valuationEmpty vs |
|
448 |
|
449 fun fold V acc = |
|
450 let |
|
451 val acc = f (V,acc) |
|
452 in |
|
453 case inc vs V of NONE => acc | SOME V => fold V acc |
|
454 end |
|
455 in |
|
456 fold zero |
|
457 end; |
|
458 |
|
459 (* ------------------------------------------------------------------------- *) |
|
460 (* Interpreting terms and formulas in the model. *) |
|
461 (* ------------------------------------------------------------------------- *) |
|
462 |
|
463 fun interpretTerm M V = |
|
464 let |
|
465 val Model {size = N, fixed, functions, ...} = M |
|
466 val {functions = fixed_functions, ...} = fixed |
|
467 |
|
468 fun interpret (Term.Var v) = |
|
469 (case NameMap.peek V v of |
|
470 NONE => raise Error "Model.interpretTerm: incomplete valuation" |
|
471 | SOME i => i) |
|
472 | interpret (tm as Term.Fn f_tms) = |
|
473 let |
|
474 val (f,tms) = |
|
475 case Term.stripComb tm of |
|
476 (_,[]) => f_tms |
|
477 | (v as Term.Var _, tms) => (".", v :: tms) |
|
478 | (Term.Fn (f,tms), tms') => (f, tms @ tms') |
|
479 val elts = map interpret tms |
|
480 val f_elts = (f,elts) |
|
481 val ref funcs = functions |
|
482 in |
|
483 case Map.peek funcs f_elts of |
|
484 SOME k => k |
|
485 | NONE => |
|
486 let |
|
487 val k = |
|
488 case fixed_functions f_elts of |
|
489 SOME k => k |
|
490 | NONE => Portable.randomInt N |
|
491 |
|
492 val () = functions := Map.insert funcs (f_elts,k) |
|
493 in |
|
494 k |
|
495 end |
|
496 end; |
|
497 in |
|
498 interpret |
|
499 end; |
|
500 |
|
501 fun interpretAtom M V (r,tms) = |
|
502 let |
|
503 val Model {fixed,relations,...} = M |
|
504 val {relations = fixed_relations, ...} = fixed |
|
505 |
|
506 val elts = map (interpretTerm M V) tms |
|
507 val r_elts = (r,elts) |
|
508 val ref rels = relations |
|
509 in |
|
510 case Map.peek rels r_elts of |
|
511 SOME b => b |
|
512 | NONE => |
|
513 let |
|
514 val b = |
|
515 case fixed_relations r_elts of |
|
516 SOME b => b |
|
517 | NONE => Portable.randomBool () |
|
518 |
|
519 val () = relations := Map.insert rels (r_elts,b) |
|
520 in |
|
521 b |
|
522 end |
|
523 end; |
|
524 |
|
525 fun interpretFormula M = |
|
526 let |
|
527 val Model {size = N, ...} = M |
|
528 |
|
529 fun interpret _ Formula.True = true |
|
530 | interpret _ Formula.False = false |
|
531 | interpret V (Formula.Atom atm) = interpretAtom M V atm |
|
532 | interpret V (Formula.Not p) = not (interpret V p) |
|
533 | interpret V (Formula.Or (p,q)) = interpret V p orelse interpret V q |
|
534 | interpret V (Formula.And (p,q)) = interpret V p andalso interpret V q |
|
535 | interpret V (Formula.Imp (p,q)) = |
|
536 interpret V (Formula.Or (Formula.Not p, q)) |
|
537 | interpret V (Formula.Iff (p,q)) = interpret V p = interpret V q |
|
538 | interpret V (Formula.Forall (v,p)) = interpret' V v p N |
|
539 | interpret V (Formula.Exists (v,p)) = |
|
540 interpret V (Formula.Not (Formula.Forall (v, Formula.Not p))) |
|
541 and interpret' _ _ _ 0 = true |
|
542 | interpret' V v p i = |
|
543 let |
|
544 val i = i - 1 |
|
545 val V' = NameMap.insert V (v,i) |
|
546 in |
|
547 interpret V' p andalso interpret' V v p i |
|
548 end |
|
549 in |
|
550 interpret |
|
551 end; |
|
552 |
|
553 fun interpretLiteral M V (true,atm) = interpretAtom M V atm |
|
554 | interpretLiteral M V (false,atm) = not (interpretAtom M V atm); |
|
555 |
|
556 fun interpretClause M V cl = LiteralSet.exists (interpretLiteral M V) cl; |
|
557 |
|
558 (* ------------------------------------------------------------------------- *) |
|
559 (* Check whether random groundings of a formula are true in the model. *) |
|
560 (* Note: if it's cheaper, a systematic check will be performed instead. *) |
|
561 (* ------------------------------------------------------------------------- *) |
|
562 |
|
563 local |
|
564 fun checkGen freeVars interpret {maxChecks} M x = |
|
565 let |
|
566 val Model {size = N, ...} = M |
|
567 |
|
568 fun score (V,{T,F}) = |
|
569 if interpret M V x then {T = T + 1, F = F} else {T = T, F = F + 1} |
|
570 |
|
571 val vs = freeVars x |
|
572 |
|
573 fun randomCheck acc = score (valuationRandom {size = N} vs, acc) |
|
574 |
|
575 val small = |
|
576 intExp N (NameSet.size vs) <= maxChecks handle Overflow => false |
|
577 in |
|
578 if small then valuationFold {size = N} vs score {T = 0, F = 0} |
|
579 else funpow maxChecks randomCheck {T = 0, F = 0} |
|
580 end; |
|
581 in |
|
582 val checkAtom = checkGen Atom.freeVars interpretAtom; |
|
583 |
|
584 val checkFormula = checkGen Formula.freeVars interpretFormula; |
|
585 |
|
586 val checkLiteral = checkGen Literal.freeVars interpretLiteral; |
|
587 |
|
588 val checkClause = checkGen LiteralSet.freeVars interpretClause; |
|
589 end; |
|
590 |
|
591 end |
|