(* sat.sml
 *
 * Robert Oestling
 * http://www.robos.org/
 *
 * A standard ML program which can verify statements in propositional logic,
 * or produce counterexamples. There is no parser, so you will have to
 * construct an expression of type boolex yourself.
 *
 * It works by converting the negation of the proposition to DNF (disjunctive
 * normal form) and simplifying it. If it simplifies to false, the proposition
 * is a tautology. Otherwise any clause of the resulting DNF expression  will
 * provide a set of variable mappings that produce a counterexample.
 *
 * The example statement is the (single) axiom in Meredith's propositional
 * logic.
 *)

datatype boolex =
    Var of int * bool
|   Not of boolex
|   And of boolex * boolex
|   Or of boolex * boolex
|   Impl of boolex * boolex
|   Eq of boolex * boolex

exception Contradiction
exception InternalError

fun sort f [] = []
|   sort f (x::[]) = [x]
|   sort f (x::xs) = let
    val (left, right) = List.partition (f x) xs
    in (sort f left) @ (x::(sort f right)) end

fun dnf e = let
    fun nnf (Var v)                 = Var v
    |   nnf (Not (Var (i, p)))      = Var (i, not p)
    |   nnf (Not (Not a))           = nnf a
    |   nnf (Not (And (a, b)))      = Or (nnf (Not a), nnf (Not b))
    |   nnf (Not (Or (a, b)))       = And (nnf (Not a), nnf (Not b))
    |   nnf (Not (Impl (a, b)))     = And (nnf a, nnf (Not b))
    |   nnf (Not (Eq (a, b)))       = Or (  And (nnf (Not a), nnf b),
                                            And (nnf a, nnf (Not b)))
    |   nnf (And (a, b))            = And (nnf a, nnf b)
    |   nnf (Or (a, b))             = Or (nnf a, nnf b)
    |   nnf (Impl (a, b))           = Or (nnf (Not a), nnf b)
    |   nnf (Eq (a, b))             = Or (  And (nnf a, nnf b),
                                            And (nnf (Not a), nnf (Not b)))
    fun distr (Or (a, b), c)        = Or (distr (a, c), distr (b, c))
    |   distr (c, Or (a, b))        = Or (distr (c, a), distr (c, b))
    |   distr (a, b)                = And (a, b)
    fun dnfn (Or (a, b))            = Or (dnfn a, dnfn b)
    |   dnfn (And (a, b))           = distr (dnfn a, dnfn b)
    |   dnfn a                      = a
    in dnfn (nnf e) end

fun flatdnf e = let
    fun vrel (Var (i, _)) (Var (j, _)) = i > j
    |   vrel _ _ = raise InternalError
    fun sortc l = sort vrel l
    fun simpc [] = []
    |   simpc (x::[]) = [x]
    |   simpc ((Var (i, b1))::(Var (j, b2))::xs) =
        if i = j
            then if b1 = b2
                then simpc ((Var (i, b1))::xs)
                else raise Contradiction
            else (Var (i, b1))::(simpc ((Var (j, b2))::xs))
    |   simpc _ = raise InternalError
    fun flatc (And (a, b))  = (flatc a) @ (flatc b)
    |   flatc a             = [a]
    fun flatd (Or (a, b))   = (flatd a) @ (flatd b)
    |   flatd a             = [flatc a]
    in List.mapPartial (fn c => SOME (simpc (sortc c))
        handle Contradiction => NONE) (flatd e)
    end

fun boolex2str (Var (i, true))  = Char.toString (chr ((ord #"a") + i))
|   boolex2str (Var (i, false)) = "!" ^ (boolex2str (Var (i, true)))
|   boolex2str (Not a)          = "!" ^ (boolex2str a)
|   boolex2str (And (a, b)) =
        "(" ^ (boolex2str a) ^ " & " ^ (boolex2str b) ^ ")"
|   boolex2str (Or (a, b)) =
        "(" ^ (boolex2str a) ^ " | " ^ (boolex2str b) ^ ")"
|   boolex2str (Impl (a, b)) =
        "(" ^ (boolex2str a) ^ " -> " ^ (boolex2str b) ^ ")"
|   boolex2str (Eq (a, b)) =
        "(" ^ (boolex2str a) ^ " = " ^ (boolex2str b) ^ ")"

fun flat2str [] = "Done"
|   flat2str e = let
    fun c2str [] = ""
    |   c2str (a::[]) = boolex2str a
    |   c2str (a::x::xs) = (boolex2str a) ^ " & " ^ (c2str (x::xs))
    fun d2str [] = ""
    |   d2str (a::[]) = "(" ^ (c2str a) ^ ")"
    |   d2str (a::x::xs) = "(" ^ (c2str a) ^ ") | " ^ (d2str (x::xs))
    in (d2str e) end

fun verify e = let
    val dnfe = dnf (Not e)
    val flat = flatdnf dnfe
    in print (
        (boolex2str e) ^ "\n\n" ^
        "DNF: " ^ (boolex2str dnfe) ^ "\n\n" ^
        "Result: " ^ (flat2str flat) ^ "\n")
    end

val meredith =
    Impl
        (Impl
            (Impl
                (Impl
                    (Impl (Var (0, true), Var (1, true)),
                    Impl (Var (2, false), Var (3, false))),
                Var (2, true)),
            Var (4, true)),
        Impl
            (Impl (Var (4, true), Var (0, true)),
            Impl (Var (3, true), Var (0, true))))

val _ = verify meredith