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