module BooleanFormula (
BooleanFormula(..), LBooleanFormula,
mkFalse, mkTrue, mkAnd, mkOr, mkVar,
isFalse, isTrue,
eval, simplify, isUnsatisfied,
implies, impliesAtom,
pprBooleanFormula, pprBooleanFormulaNice
) where
import GhcPrelude
import Data.List ( nub, intersperse )
import Data.Data
import MonadUtils
import Outputable
import Binary
import SrcLoc
import Unique
import UniqSet
type LBooleanFormula a = Located (BooleanFormula a)
data BooleanFormula a = Var a | And [LBooleanFormula a] | Or [LBooleanFormula a]
| Parens (LBooleanFormula a)
deriving (Eq, Data, Functor, Foldable, Traversable)
mkVar :: a -> BooleanFormula a
mkVar = Var
mkFalse, mkTrue :: BooleanFormula a
mkFalse = Or []
mkTrue = And []
mkBool :: Bool -> BooleanFormula a
mkBool False = mkFalse
mkBool True = mkTrue
mkAnd :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkAnd = maybe mkFalse (mkAnd' . nub) . concatMapM fromAnd
where
fromAnd :: LBooleanFormula a -> Maybe [LBooleanFormula a]
fromAnd (L _ (And xs)) = Just xs
fromAnd (L _ (Or [])) = Nothing
fromAnd x = Just [x]
mkAnd' [x] = unLoc x
mkAnd' xs = And xs
mkOr :: Eq a => [LBooleanFormula a] -> BooleanFormula a
mkOr = maybe mkTrue (mkOr' . nub) . concatMapM fromOr
where
fromOr (L _ (Or xs)) = Just xs
fromOr (L _ (And [])) = Nothing
fromOr x = Just [x]
mkOr' [x] = unLoc x
mkOr' xs = Or xs
isFalse :: BooleanFormula a -> Bool
isFalse (Or []) = True
isFalse _ = False
isTrue :: BooleanFormula a -> Bool
isTrue (And []) = True
isTrue _ = False
eval :: (a -> Bool) -> BooleanFormula a -> Bool
eval f (Var x) = f x
eval f (And xs) = all (eval f . unLoc) xs
eval f (Or xs) = any (eval f . unLoc) xs
eval f (Parens x) = eval f (unLoc x)
simplify :: Eq a => (a -> Maybe Bool) -> BooleanFormula a -> BooleanFormula a
simplify f (Var a) = case f a of
Nothing -> Var a
Just b -> mkBool b
simplify f (And xs) = mkAnd (map (\(L l x) -> L l (simplify f x)) xs)
simplify f (Or xs) = mkOr (map (\(L l x) -> L l (simplify f x)) xs)
simplify f (Parens x) = simplify f (unLoc x)
isUnsatisfied :: Eq a => (a -> Bool) -> BooleanFormula a -> Maybe (BooleanFormula a)
isUnsatisfied f bf
| isTrue bf' = Nothing
| otherwise = Just bf'
where
f' x = if f x then Just True else Nothing
bf' = simplify f' bf
impliesAtom :: Eq a => BooleanFormula a -> a -> Bool
Var x `impliesAtom` y = x == y
And xs `impliesAtom` y = any (\x -> (unLoc x) `impliesAtom` y) xs
Or xs `impliesAtom` y = all (\x -> (unLoc x) `impliesAtom` y) xs
Parens x `impliesAtom` y = (unLoc x) `impliesAtom` y
implies :: Uniquable a => BooleanFormula a -> BooleanFormula a -> Bool
implies e1 e2 = go (Clause emptyUniqSet [e1]) (Clause emptyUniqSet [e2])
where
go :: Uniquable a => Clause a -> Clause a -> Bool
go l@Clause{ clauseExprs = hyp:hyps } r =
case hyp of
Var x | memberClauseAtoms x r -> True
| otherwise -> go (extendClauseAtoms l x) { clauseExprs = hyps } r
Parens hyp' -> go l { clauseExprs = unLoc hyp':hyps } r
And hyps' -> go l { clauseExprs = map unLoc hyps' ++ hyps } r
Or hyps' -> all (\hyp' -> go l { clauseExprs = unLoc hyp':hyps } r) hyps'
go l r@Clause{ clauseExprs = con:cons } =
case con of
Var x | memberClauseAtoms x l -> True
| otherwise -> go l (extendClauseAtoms r x) { clauseExprs = cons }
Parens con' -> go l r { clauseExprs = unLoc con':cons }
And cons' -> all (\con' -> go l r { clauseExprs = unLoc con':cons }) cons'
Or cons' -> go l r { clauseExprs = map unLoc cons' ++ cons }
go _ _ = False
data Clause a = Clause {
clauseAtoms :: UniqSet a,
clauseExprs :: [BooleanFormula a]
}
extendClauseAtoms :: Uniquable a => Clause a -> a -> Clause a
extendClauseAtoms c x = c { clauseAtoms = addOneToUniqSet (clauseAtoms c) x }
memberClauseAtoms :: Uniquable a => a -> Clause a -> Bool
memberClauseAtoms x c = x `elementOfUniqSet` clauseAtoms c
pprBooleanFormula' :: (Rational -> a -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> (Rational -> [SDoc] -> SDoc)
-> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula' pprVar pprAnd pprOr = go
where
go p (Var x) = pprVar p x
go p (And []) = cparen (p > 0) $ empty
go p (And xs) = pprAnd p (map (go 3 . unLoc) xs)
go _ (Or []) = keyword $ text "FALSE"
go p (Or xs) = pprOr p (map (go 2 . unLoc) xs)
go p (Parens x) = go p (unLoc x)
pprBooleanFormula :: (Rational -> a -> SDoc) -> Rational -> BooleanFormula a -> SDoc
pprBooleanFormula pprVar = pprBooleanFormula' pprVar pprAnd pprOr
where
pprAnd p = cparen (p > 3) . fsep . punctuate comma
pprOr p = cparen (p > 2) . fsep . intersperse vbar
pprBooleanFormulaNice :: Outputable a => BooleanFormula a -> SDoc
pprBooleanFormulaNice = pprBooleanFormula' pprVar pprAnd pprOr 0
where
pprVar _ = quotes . ppr
pprAnd p = cparen (p > 1) . pprAnd'
pprAnd' [] = empty
pprAnd' [x,y] = x <+> text "and" <+> y
pprAnd' xs@(_:_) = fsep (punctuate comma (init xs)) <> text ", and" <+> last xs
pprOr p xs = cparen (p > 1) $ text "either" <+> sep (intersperse (text "or") xs)
instance (OutputableBndr a) => Outputable (BooleanFormula a) where
ppr = pprBooleanFormulaNormal
pprBooleanFormulaNormal :: (OutputableBndr a)
=> BooleanFormula a -> SDoc
pprBooleanFormulaNormal = go
where
go (Var x) = pprPrefixOcc x
go (And xs) = fsep $ punctuate comma (map (go . unLoc) xs)
go (Or []) = keyword $ text "FALSE"
go (Or xs) = fsep $ intersperse vbar (map (go . unLoc) xs)
go (Parens x) = parens (go $ unLoc x)
instance Binary a => Binary (BooleanFormula a) where
put_ bh (Var x) = putByte bh 0 >> put_ bh x
put_ bh (And xs) = putByte bh 1 >> put_ bh xs
put_ bh (Or xs) = putByte bh 2 >> put_ bh xs
put_ bh (Parens x) = putByte bh 3 >> put_ bh x
get bh = do
h <- getByte bh
case h of
0 -> Var <$> get bh
1 -> And <$> get bh
2 -> Or <$> get bh
_ -> Parens <$> get bh