{-# 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
[DNF lit] -> ShowS
DNF lit -> String
(Int -> DNF lit -> ShowS)
-> (DNF lit -> String) -> ([DNF lit] -> ShowS) -> Show (DNF lit)
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
$cshowsPrec :: forall lit. Show lit => Int -> DNF lit -> ShowS
showsPrec :: Int -> DNF lit -> ShowS
$cshow :: forall lit. Show lit => DNF lit -> String
show :: DNF lit -> String
$cshowList :: forall lit. Show lit => [DNF lit] -> ShowS
showList :: [DNF lit] -> ShowS
Show)

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

instance MonotoneBoolean (DNF lit) where
  true :: DNF lit
true  = [[lit]] -> DNF lit
forall lit. [[lit]] -> DNF lit
DNF [[]]
  false :: DNF lit
false = [[lit]] -> DNF lit
forall lit. [[lit]] -> DNF lit
DNF []
  DNF [[lit]]
xs .||. :: DNF lit -> DNF lit -> DNF lit
.||. DNF [[lit]]
ys = [[lit]] -> DNF lit
forall lit. [[lit]] -> DNF lit
DNF ([[lit]]
xs[[lit]] -> [[lit]] -> [[lit]]
forall a. [a] -> [a] -> [a]
++[[lit]]
ys)
  DNF [[lit]]
xs .&&. :: DNF lit -> DNF lit -> DNF lit
.&&. DNF [[lit]]
ys = [[lit]] -> DNF lit
forall lit. [[lit]] -> DNF lit
DNF [[lit]
x[lit] -> [lit] -> [lit]
forall 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 = DNF lit -> DNF lit -> DNF lit -> DNF lit
forall a. Boolean a => a -> a -> a -> a
iteBoolean

instance Complement lit => Boolean (DNF lit)