94
|
1 |
signature IFF_SOLVER =
|
|
2 |
sig
|
|
3 |
val decide : string -> bool
|
|
4 |
end
|
|
5 |
|
|
6 |
|
|
7 |
structure IffSolver : IFF_SOLVER =
|
|
8 |
struct
|
|
9 |
|
|
10 |
exception FAIL
|
|
11 |
|
|
12 |
datatype formula = Atom of string | Iff of formula * formula
|
|
13 |
|
|
14 |
fun scan s =
|
|
15 |
let
|
|
16 |
|
|
17 |
fun push yss = [] :: yss
|
|
18 |
|
|
19 |
fun add x (ys :: yss) = (x :: ys) :: yss
|
|
20 |
| add _ _ = raise FAIL
|
|
21 |
|
|
22 |
fun pop ([a, b] :: yss) = add (Iff (b, a)) yss
|
|
23 |
| pop _ = raise FAIL
|
|
24 |
|
|
25 |
fun formula [] acc = acc
|
|
26 |
| formula ("(" :: xs) acc = formula xs (push acc)
|
|
27 |
| formula (")" :: xs) acc = formula xs (pop acc)
|
|
28 |
| formula ("<=>" :: xs) acc = formula xs acc
|
|
29 |
| formula (x :: xs) acc = formula xs (add (Atom x) acc)
|
|
30 |
|
|
31 |
val tokens = String.tokens (fn c => c = #" ") s
|
|
32 |
in
|
|
33 |
(case formula tokens [[]] of
|
|
34 |
[[f]] => f
|
|
35 |
| _ => raise FAIL)
|
|
36 |
end
|
|
37 |
|
|
38 |
|
|
39 |
fun decide s =
|
|
40 |
let
|
|
41 |
fun fold_atoms f (Atom n) = f s
|
|
42 |
| fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q
|
|
43 |
|
|
44 |
fun collect s tab =
|
|
45 |
(case Symtab.lookup tab s of
|
|
46 |
NONE => Symtab.update (s, false) tab
|
|
47 |
| SOME v => Symtab.update (s, not v) tab)
|
|
48 |
|
|
49 |
fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true
|
|
50 |
in
|
|
51 |
(case try scan s of
|
|
52 |
NONE => false
|
|
53 |
| SOME f => check (fold_atoms collect f Symtab.empty))
|
|
54 |
end
|
|
55 |
|
|
56 |
end
|