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