signature IFF_SOLVER =+
−
sig+
−
  val decide : string -> bool+
−
end+
−
+
−
+
−
structure IffSolver : IFF_SOLVER =+
−
struct+
−
+
−
exception FAIL+
−
+
−
datatype formula = Atom of string | Iff of formula * formula+
−
+
−
fun scan s =+
−
  let+
−
+
−
    fun push yss = [] :: yss +
−
+
−
    fun add x (ys :: yss) = (x :: ys) :: yss+
−
      | add _ _ = raise FAIL+
−
+
−
    fun pop ([a, b] :: yss) = add (Iff (b, a)) yss+
−
      | pop _ = raise FAIL+
−
+
−
    fun formula [] acc = acc+
−
      | formula ("(" :: xs) acc = formula xs (push acc)+
−
      | formula (")" :: xs) acc = formula xs (pop acc)+
−
      | formula ("<=>" :: xs) acc = formula xs acc+
−
      | formula (x :: xs) acc = formula xs (add (Atom x) acc)+
−
+
−
    val tokens = String.tokens (fn c => c = #" ") s+
−
  in+
−
    (case formula tokens [[]] of+
−
      [[f]] => f+
−
    | _ => raise FAIL)+
−
  end+
−
+
−
+
−
fun decide s =+
−
  let+
−
    fun fold_atoms f (Atom n) = f s+
−
      | fold_atoms f (Iff (p, q)) = fold_atoms f p #> fold_atoms f q+
−
+
−
    fun collect s tab =+
−
      (case Symtab.lookup tab s of+
−
        NONE => Symtab.update (s, false) tab+
−
      | SOME v => Symtab.update (s, not v) tab)+
−
+
−
    fun check tab = Symtab.fold (fn (_, v) => fn b => b andalso v) tab true+
−
  in +
−
    (case try scan s of+
−
      NONE => false+
−
    | SOME f => check (fold_atoms collect f Symtab.empty))+
−
  end+
−
+
−
end+
−