{-# 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
  { forall lit. DNF lit -> [[lit]]
unDNF :: [[lit]] -- ^ list of conjunction of literals
  } deriving (Int -> DNF lit -> ShowS
forall lit. Show lit => Int -> DNF lit -> ShowS
forall lit. Show lit => [DNF lit] -> ShowS
forall lit. Show lit => DNF lit -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [DNF lit] -> ShowS
$cshowList :: forall lit. Show lit => [DNF lit] -> ShowS
show :: DNF lit -> String
$cshow :: forall lit. Show lit => DNF lit -> String
showsPrec :: Int -> DNF lit -> ShowS
$cshowsPrec :: forall lit. Show lit => Int -> DNF lit -> ShowS
Show)

instance Complement lit => Complement (DNF lit) where
  notB :: DNF lit -> DNF lit
notB (DNF [[lit]]
xs) = forall lit. [[lit]] -> DNF lit
DNF forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a -> b) -> [a] -> [b]
map forall a. Complement a => a -> a
notB) forall a b. (a -> b) -> a -> b
$ [[lit]]
xs

instance MonotoneBoolean (DNF lit) where
  true :: DNF lit
true  = forall lit. [[lit]] -> DNF lit
DNF [[]]
  false :: DNF lit
false = forall lit. [[lit]] -> DNF lit
DNF []
  DNF [[lit]]
xs .||. :: DNF lit -> DNF lit -> DNF lit
.||. DNF [[lit]]
ys = forall lit. [[lit]] -> DNF lit
DNF ([[lit]]
xsforall a. [a] -> [a] -> [a]
++[[lit]]
ys)
  DNF [[lit]]
xs .&&. :: DNF lit -> DNF lit -> DNF lit
.&&. DNF [[lit]]
ys = forall lit. [[lit]] -> DNF lit
DNF [[lit]
xforall a. [a] -> [a] -> [a]
++[lit]
y | [lit]
x<-[[lit]]
xs, [lit]
y<-[[lit]]
ys]

instance Complement lit => IfThenElse (DNF lit) (DNF lit) where
  ite :: DNF lit -> DNF lit -> DNF lit -> DNF lit
ite = forall a. Boolean a => a -> a -> a -> a
iteBoolean

instance Complement lit => Boolean (DNF lit)