1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
|
(* Find a satisfying interpretation via brute force *)
open Types
open Lib_utils
(* lazy list *)
type 'a seq = Nil | Cons of 'a * (unit -> 'a seq)
let head = function
| Nil -> None
| Cons(x, _) -> Some x
let tail = function
| Nil -> None
| Cons(_, tl) -> Some tl
let rec get k s =
match k, s with
| 0, _ -> []
| _, Nil -> []
| k, Cons(x, f) -> x :: get (k - 1) (f ())
(* Find all the literals in a formula *)
let extract_symbols (prop : proposition) =
let rec search prop acc =
match prop with
| True -> acc
| False -> acc
| Lit s -> Lit s :: acc
| Not p -> search p acc
| And(p1, p2) -> search p1 (search p2 acc)
| Or(p1, p2) -> search p1 (search p2 acc)
| Implies(p1, p2) -> search p1 (search p2 acc)
| Iff(p1, p2) -> search p1 (search p2 acc)
in
search prop []
(* Generate all possible truth assignments for a list of symbols *)
let rec generate_truth_vals symbols =
let rec prepend_all x llist = (* prepend x to each item in the lazy list *)
match llist with
| Nil -> Nil
| Cons(xs, fn) -> Cons(x::xs, fun () -> prepend_all x (fn ()))
in
let rec interleave s1 s2 =
match s1, s2 with
| _, Nil -> s1
| Nil, _ -> s2
| Cons(x1, f1), _ -> Cons(x1, fun () -> interleave s2 (f1 ()))
in
match symbols with
| [] -> Cons ([], fun () -> Nil)
| Lit s :: tl ->
let tl_vals = generate_truth_vals tl in
let s_true = prepend_all (s, true) tl_vals in
let s_false = prepend_all (s, false) tl_vals in
interleave s_true s_false
| _ -> failwith "discovered a bug"
(* brute force search for a satisfying interpretation *)
let satisfy prop =
let symbols = extract_symbols prop in
let truth_vals = generate_truth_vals symbols in
let rec try_next truth_vals =
match truth_vals with
| Nil -> None
| Cons(i, f) ->
begin
match test_interpretation prop i with
| Some true -> Some i
| _ -> try_next (f ())
end
in
try_next truth_vals
|
