content: {-# OPTIONS_HADDOCK show-extensions #-}
  {-# LANGUAGE MultiParamTypeClasses #-}
  -----------------------------------------------------------------------------
  -- |
  -- Module      :  ToySolver.Data.DNF
  -- Copyright   :  (c) Masahiro Sakai 2011-2013
  -- License     :  BSD-style
  --
  -- Maintainer  :  masahiro.sakai@gmail.com
  -- Stability   :  provisional
  -- Portability :  non-portable
  --
  -- Disjunctive Normal Form
  --
  -----------------------------------------------------------------------------
  module ToySolver.Data.DNF
    ( DNF (..)
    ) where
  
  import ToySolver.Data.Boolean
  
  -- | Disjunctive normal form
  newtype DNF lit
    = DNF
    { unDNF :: [[lit]] -- ^ list of conjunction of literals
    } 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)
  