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