data BE vn
   = F
   | T
   | Var vn
   | Not (BE vn)
   | And (BE vn) (BE vn)
   | Or  (BE vn) (BE vn)
   | Imp (BE vn) (BE vn)
   | Eqv (BE vn) (BE vn)
   deriving (Eq, Read, Show)
type BE1 = BE Int

data ROBDD vn
   = R_False
   | R_True
   | R_If vn (ROBDD vn) (ROBDD vn)
   deriving (Eq, Read, Show)

robdd :: (Ord vn) => BE vn -> ROBDD vn
robdd F = R_False
robdd T = R_True
robdd (Var v) = R_If v R_True R_False
robdd (Not e) = opposite (robdd e)
robdd (And e f) = and_merge (robdd e) (robdd f)
robdd (Or  e f) = or_merge  (robdd e) (robdd f)
robdd (Imp e f) = imp_merge (robdd e) (robdd f)
robdd (Eqv e f) = eqv_merge (robdd e) (robdd f)

opposite :: ROBDD vn -> ROBDD vn
opposite R_False = R_True
opposite R_True = R_False
opposite (R_If v e f) = R_If v (opposite e) (opposite f)

mk_if :: (Eq vn) => vn -> ROBDD vn -> ROBDD vn -> ROBDD vn
mk_if v x y = if x == y then x else R_If v x y

{- The general pattern is
    foo_merge :: (Ord vn) => ROBDD vn -> ROBDD vn -> ROBDD vn
    foo_merge R_False y = ??
    foo_merge x R_False = ??
    foo_merge R_True  y = ??
    foo_merge x R_True  = ??
    foo_merge x@(R_If u a b) y@(R_If v c d)
       | x == y = ??
       | u < v  = mk_if u (foo_merge a y) (foo_merge b y)
       | v < u  = mk_if v (foo_merge x c) (foo_merge x d)
       | True   = mk_if u (foo_merge a c) (foo_merge b d)

   The five places where ?? appears above are different for each of
   the Boolean operators (and, or, imp, eqv), would be different for
   xor if we had it.
-}
and_merge :: (Ord vn) => ROBDD vn -> ROBDD vn -> ROBDD vn
and_merge R_False _ = R_False
and_merge _ R_False = R_False
and_merge R_True y  = y
and_merge x R_True  = x
and_merge x@(R_If u a b) y@(R_If v c d)
    | x == y = x
    | u < v = mk_if u (and_merge a y) (and_merge b y)
    | u > v = mk_if v (and_merge x c) (and_merge x d)
    | True  = mk_if u (and_merge a c) (and_merge b d)

or_merge :: (Ord vn) => ROBDD vn -> ROBDD vn -> ROBDD vn
or_merge R_False y = y
or_merge x R_False = x
or_merge R_True _  = R_True
or_merge _ R_True  = R_True
or_merge x@(R_If u a b) y@(R_If v c d)
    | x == y = x
    | u < v = mk_if u (or_merge a y) (or_merge b y)
    | u > v = mk_if v (or_merge x c) (or_merge x d)
    | True  = mk_if u (or_merge a c) (or_merge b d)

imp_merge :: (Ord vn) => ROBDD vn -> ROBDD vn -> ROBDD vn
imp_merge R_False _ = R_True
imp_merge x R_False = opposite x
imp_merge R_True y  = y
imp_merge _ R_True  = R_True
imp_merge x@(R_If u a b) y@(R_If v c d)
    | x == y = R_True
    | u < v = mk_if u (imp_merge a y) (imp_merge b y)
    | u > v = mk_if v (imp_merge x c) (imp_merge x d)
    | True  = mk_if u (imp_merge a c) (imp_merge b d)

eqv_merge :: (Ord vn) => ROBDD vn -> ROBDD vn -> ROBDD vn
eqv_merge R_False y = opposite y
eqv_merge x R_False = opposite x
eqv_merge R_True y  = y
eqv_merge x R_True  = x
eqv_merge x@(R_If u a b) y@(R_If v c d)
    | x == y = R_True
    | u < v = mk_if u (eqv_merge a y) (eqv_merge b y)
    | u > v = mk_if v (eqv_merge x c) (eqv_merge x d)
    | True  = mk_if u (eqv_merge a c) (eqv_merge b d)


{-  Given a ROBDD, we can ask for a (partial) model
    or a (partial) counter-model.  It might be that there is none.
    We'll use (Maybe [(var,Bool)]) as the type for possible partial models.
    We'll exploit laziness; our functions will LAZILY construct a list of
    all partial (counter-)models, and we'll pick the first if there is one.
-}

first_model, first_counter_model :: ROBDD vn -> Maybe [(vn,Bool)]

first_model r = list_to_maybe (models r [])
  where models R_False      _ = []
        models R_True       m = [reverse m]
        models (R_If u a b) m =
	    models a ((u,True):m) ++ models b ((u,False):m)

first_counter_model r = list_to_maybe (counter_models r [])
  where counter_models R_False      m = [reverse m]
        counter_models R_True       _ = []
        counter_models (R_If u a b) m =
            counter_models a ((u,True):m) ++ counter_models b ((u,False):m)

list_to_maybe [] = Nothing
list_to_maybe (x:_) = Just x

mm n = first_model (robdd (tc n))
cm n = first_counter_model (robdd (tc n))

{- Here are some test cases -}

tc :: Int -> BE1
tc 1 = (Var 1)
tc 2 = (Or (Var 1) (Var 1))
tc 3 = (Eqv (Imp (Var 1) (Var 2)) (Or (Not (Var 1)) (Var 2)))
tc 4 = (Eqv (And (Var 1) (Var 1)) (Var 1))
tc 5 = (And (And (And (Eqv (Var 13) (Or (And F (Var 1)) (Or (And F (Var
        5)) (And (Var 1) (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not (Var
        1))) (Not (Var 5))))) (And (And (Eqv (Var 14) (Or (And (Var 13)
        (Var 2)) (Or (And (Var 13) (Var 6)) (And (Var 2) (Var 6)))))
        (Eqv (Var 10) (Eqv (Eqv (Var 13) (Not (Var 2))) (Not (Var 6)))))
        (And (And (Eqv (Var 15) (Or (And (Var 14) (Var 3)) (Or (And (Var
        14) (Var 7)) (And (Var 3) (Var 7))))) (Eqv (Var 11) (Eqv (Eqv
        (Var 14) (Not (Var 3))) (Not (Var 7))))) (And (Eqv (Var 16) (Or
        (And (Var 15) (Var 4)) (Or (And (Var 15) (Var 8)) (And (Var 4)
        (Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not (Var 4))) (Not
        (Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not F)
        (And (Var 1) (Var 5))) (And F (Or (Var 1) (Var 5))))) (Eqv (Var
        9) (Or (And F (And (Var 1) (Var 5))) (Or (And F (And (Not (Var
        1)) (Not (Var 5)))) (Or (And (Not F) (And (Var 1) (Not (Var
        5)))) (And (Not F) (And (Not (Var 1)) (Var 5)))))))) (And (And
        (Eqv (Var 18) (Or (And (Not (Var 17)) (And (Var 2) (Var 6)))
        (And (Var 17) (Or (Var 2) (Var 6))))) (Eqv (Var 10) (Or (And
        (Var 17) (And (Var 2) (Var 6))) (Or (And (Var 17) (And (Not (Var
        2)) (Not (Var 6)))) (Or (And (Not (Var 17)) (And (Var 2) (Not
        (Var 6)))) (And (Not (Var 17)) (And (Not (Var 2)) (Var 6))))))))
        (And (And (Eqv (Var 19) (Or (And (Not (Var 18)) (And (Var 3)
        (Var 7))) (And (Var 18) (Or (Var 3) (Var 7))))) (Eqv (Var 11)
        (Or (And (Var 18) (And (Var 3) (Var 7))) (Or (And (Var 18) (And
        (Not (Var 3)) (Not (Var 7)))) (Or (And (Not (Var 18)) (And (Var
        3) (Not (Var 7)))) (And (Not (Var 18)) (And (Not (Var 3)) (Var
        7)))))))) (And (Eqv (Var 20) (Or (And (Not (Var 19)) (And (Var
        4) (Var 8))) (And (Var 19) (Or (Var 4) (Var 8))))) (Eqv (Var 12)
        (Or (And (Var 19) (And (Var 4) (Var 8))) (Or (And (Var 19) (And
        (Not (Var 4)) (Not (Var 8)))) (Or (And (Not (Var 19)) (And (Var
        4) (Not (Var 8)))) (And (Not (Var 19)) (And (Not (Var 4)) (Var
        8))))))))))) (Eqv (Var 16) (Var 20))))
tc 6 = (And (And (And (Eqv (Var 13) (Or (And F T) (Or (And F (Var 5))
        (And T (Var 5))))) (Eqv (Var 9) (Eqv (Eqv F (Not T)) (Not (Var
        5))))) (And (And (Eqv (Var 14) (Or (And (Var 13) F) (Or (And
        (Var 13) (Var 6)) (And F (Var 6))))) (Eqv (Var 10) (Eqv (Eqv
        (Var 13) (Not F)) (Not (Var 6))))) (And (And (Eqv (Var 15) (Or
        (And (Var 14) F) (Or (And (Var 14) (Var 7)) (And F (Var 7)))))
        (Eqv (Var 11) (Eqv (Eqv (Var 14) (Not F)) (Not (Var 7))))) (And
        (Eqv (Var 16) (Or (And (Var 15) T) (Or (And (Var 15) (Var 8))
        (And T (Var 8))))) (Eqv (Var 12) (Eqv (Eqv (Var 15) (Not T))
        (Not (Var 8)))))))) (And (And (And (Eqv (Var 17) (Or (And (Not
        F) (And T (Var 5))) (And F (Or T (Var 5))))) (Eqv (Var 9) (Or
        (And F (And T (Var 5))) (Or (And F (And (Not T) (Not (Var 5))))
        (Or (And (Not F) (And T (Not (Var 5)))) (And (Not F) (And (Not
        T) (Var 5)))))))) (And (And (Eqv (Var 18) (Or (And (Not (Var
        17)) (And F (Var 6))) (And (Var 17) (Or F (Var 6))))) (Eqv (Var
        10) (Or (And (Var 17) (And F (Var 6))) (Or (And (Var 17) (And
        (Not F) (Not (Var 6)))) (Or (And (Not (Var 17)) (And F (Not (Var
        6)))) (And (Not (Var 17)) (And (Not F) (Var 6)))))))) (And (And
        (Eqv (Var 19) (Or (And (Not (Var 18)) (And F (Var 7))) (And (Var
        18) (Or F (Var 7))))) (Eqv (Var 11) (Or (And (Var 18) (And F
        (Var 7))) (Or (And (Var 18) (And (Not F) (Not (Var 7)))) (Or
        (And (Not (Var 18)) (And F (Not (Var 7)))) (And (Not (Var 18))
        (And (Not F) (Var 7)))))))) (And (Eqv (Var 20) (Or (And (Not
        (Var 19)) (And T (Var 8))) (And (Var 19) (Or T (Var 8))))) (Eqv
        (Var 12) (Or (And (Var 19) (And T (Var 8))) (Or (And (Var 19)
        (And (Not T) (Not (Var 8)))) (Or (And (Not (Var 19)) (And T (Not
        (Var 8)))) (And (Not (Var 19)) (And (Not T) (Var 8)))))))))))
        (Eqv (Var 16) (Var 20))))
tc 7 = Eqv (Not (Or (Var 1) (Or (Var 2) (Var 3))))
           (And (Not (Var 1)) (And (Not (Var 2)) (Not (Var 3)) ))
tc 8 = (Eqv (Not (And (Var 1) (And (Var 2) (And (Var 3) (And (Var 4)
        (And (Var 5) (And (Var 6) (And (Var 7) (And (Var 8) (And (Var 9)
        (And (Var 10) (And (Var 11) (And (Var 12) (And (Var 13) (And
        (Var 14) (And (Var 15) (Var 16))))))))))))))))) (Or (Not (Var
        1)) (Or (Not (Var 2)) (Or (Not (Var 3)) (Or (Not (Var 4)) (Or
        (Not (Var 5)) (Or (Not (Var 6)) (Or (Not (Var 7)) (Or (Not (Var
        8)) (Or (Not (Var 9)) (Or (Not (Var 10)) (Or (Not (Var 11)) (Or
        (Not (Var 12)) (Or (Not (Var 13)) (Or (Not (Var 14)) (Or (Not
        (Var 15)) (Not (Var 16))))))))))))))))))
tc 9 = (Eqv (Not (Or (Var 1) (Or (Var 2) (Or (Var 3) (Or (Var 4) (Or
        (Var 5) (Or (Var 6) (Or (Var 7) (Or (Var 8) (Or (Var 9) (Or (Var
        10) (Or (Var 11) (Or (Var 12) (Or (Var 13) (Or (Var 14) (Or (Var
        15) (Var 16))))))))))))))))) (And (Not (Var 1)) (And (Not (Var
        2)) (And (Not (Var 3)) (And (Not (Var 4)) (And (Not (Var 5))
        (And (Not (Var 6)) (And (Not (Var 7)) (And (Not (Var 8)) (And
        (Not (Var 9)) (And (Not (Var 10)) (And (Not (Var 11)) (And (Not
        (Var 12)) (And (Not (Var 13)) (And (Not (Var 14)) (And (Not (Var
        15)) (Not (Var 16))))))))))))))))))
-- Test cases 10 to 21 were provided by Jonathan Pengelly
tc 10 = (And (Var 1) (Not (Var 1)))
tc 11 = (Or (And (Var 1) (Not (Var 2))) (And (Not (Var 1)) (Var 2)))
-- Modus Ponens test
tc 12 = (And (And (Var 1) (Imp (Var 1) (Var 2))) (Not (Var 2)))
-- Modus Tollens test
tc 13 = (And (And (Not (Var 2)) (Imp (Var 1) (Var 2))) (Var 1))
-- Double negation test
tc 14 = (Eqv (Var 1) (Not (Not (Var 1))))
-- Associativity
tc 15 = (Eqv (And (And (Var 1) (Var 2)) (Var 3))
             (And (Var 1) (And (Var 2) (Var 3))))
-- De Morgan's rules
tc 16 = (Eqv (Not (Or (Var 1) (Var 2))) (And (Not (Var 1)) (Not (Var 2))))
-- Show that the following is not a tautology
tc 17 = (Imp (Imp (Var 1) (Var 3)) (Imp (Imp (Var 2) (Var 4))
        (Imp (Or (Var 1) (Var 2)) (Var 3))))
-- Unsatisfiable set of clauses
tc 18 = (And (And (And (Or (Or (Var 1) (Var 2)) (Not (Var 3)))
	(Or (Or (Var 1) (Var 2)) (Var 3))) (Or (Var 1) (Not (Var 2))))
	(Not (Var 1)))
-- Tautology
tc 19 = (Imp (Var 1) (Imp (Var 2) (Var 1)))
tc 20 = T
tc 21 = F