module ToySolver.Data.DNF
( DNF (..)
) where
import ToySolver.Data.Boolean
newtype DNF lit
= DNF
{ unDNF :: [[lit]]
} deriving (Show)
instance Complement lit => Complement (DNF lit) where
notB (DNF xs) = DNF . sequence . map (map notB) $ xs
instance MonotoneBoolean (DNF lit) where
true = DNF [[]]
false = DNF []
DNF xs .||. DNF ys = DNF (xs++ys)
DNF xs .&&. DNF ys = DNF [x++y | x<-xs, y<-ys]
instance Complement lit => IfThenElse (DNF lit) (DNF lit) where
ite = iteBoolean
instance Complement lit => Boolean (DNF lit)