module Data.Boolean (
Boolean(..),
Literal(..), literalVar, invLiteral, isPositiveLiteral,
CNF, booleanToCNF
) where
data Boolean
= Var Int
| Yes
| No
| Not Boolean
| Boolean :&&: Boolean
| Boolean :||: Boolean
data Literal = Pos Int | Neg Int deriving (Eq, Show)
literalVar :: Literal -> Int
literalVar (Pos n) = n
literalVar (Neg n) = n
invLiteral :: Literal -> Literal
invLiteral (Pos n) = Neg n
invLiteral (Neg n) = Pos n
isPositiveLiteral :: Literal -> Bool
isPositiveLiteral (Pos _) = True
isPositiveLiteral _ = False
type CNF = [Clause]
type Clause = [Literal]
booleanToCNF :: Boolean -> CNF
booleanToCNF
= map (map literal . disjunction)
. conjunction
. asLongAsPossible distribute
. asLongAsPossible pushNots
. asLongAsPossible elim
where
elim (Not Yes) = Just No
elim (Not No) = Just Yes
elim (No :&&: _) = Just No
elim (Yes :&&: x) = Just x
elim (_ :&&: No) = Just No
elim (x :&&: Yes) = Just x
elim (Yes :||: _) = Just Yes
elim (No :||: x) = Just x
elim (_ :||: Yes) = Just Yes
elim (x :||: No) = Just x
elim _ = Nothing
pushNots (Not (Not x)) = Just x
pushNots (Not (x:&&:y)) = Just (Not x :||: Not y)
pushNots (Not (x:||:y)) = Just (Not x :&&: Not y)
pushNots _ = Nothing
distribute (x:||:(y:&&:z)) = Just ((x:||:y):&&:(x:||:z))
distribute ((x:&&:y):||:z) = Just ((x:||:z):&&:(y:||:z))
distribute _ = Nothing
literal (Var x) = Pos x
literal (Not (Var x)) = Neg x
conjunction :: Boolean -> [Boolean]
conjunction b = flat b []
where flat Yes = id
flat (x:&&:y) = flat x . flat y
flat x = (x:)
disjunction :: Boolean -> [Boolean]
disjunction b = flat b []
where flat No = id
flat (x:||:y) = flat x . flat y
flat x = (x:)
asLongAsPossible :: (Boolean -> Maybe Boolean) -> Boolean -> Boolean
asLongAsPossible f = everywhere g
where g x = maybe x (everywhere g) (f x)
everywhere :: (Boolean -> Boolean) -> Boolean -> Boolean
everywhere f = f . atChildren (everywhere f)
atChildren :: (Boolean -> Boolean) -> Boolean -> Boolean
atChildren f (Not x) = Not (f x)
atChildren f (x:&&:y) = f x :&&: f y
atChildren f (x:||:y) = f x :||: f y
atChildren _ x = x