{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# OPTIONS_HADDOCK not-home #-}
module Ersatz.Internal.Formula
(
Clause(..), clauseLiterals, fromLiteral
, Formula(..)
, formulaEmpty, formulaLiteral, fromClause
, formulaNot, formulaAnd, formulaOr, formulaXor, formulaMux
, formulaFAS, formulaFAC
) where
import Data.IntSet (IntSet)
import qualified Data.IntSet as IntSet
import qualified Data.List as List (intersperse)
import Data.Typeable
import Ersatz.Internal.Literal
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Foldable (toList)
#if !(MIN_VERSION_base(4,8,0))
import Control.Applicative
import Data.Monoid (Monoid(..))
#endif
#if !(MIN_VERSION_base(4,11,0))
import Data.Semigroup (Semigroup(..))
#endif
newtype Clause = Clause { clauseSet :: IntSet }
deriving (Eq, Ord, Typeable)
clauseLiterals :: Clause -> [Literal]
clauseLiterals (Clause is) = Literal <$> IntSet.toList is
instance Semigroup Clause where
Clause x <> Clause y = Clause (x <> y)
instance Monoid Clause where
mempty = Clause mempty
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
fromLiteral :: Literal -> Clause
fromLiteral l = Clause { clauseSet = IntSet.singleton $ literalId l }
newtype Formula = Formula { formulaSet :: Seq Clause }
deriving (Eq, Ord, Typeable)
instance Semigroup Formula where
Formula x <> Formula y = Formula (x <> y)
instance Monoid Formula where
mempty = Formula mempty
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
instance Show Formula where
showsPrec p = showParen (p > 2) . foldr (.) id
. List.intersperse (showString " & ") . map (showsPrec 3)
. Data.Foldable.toList . formulaSet
instance Show Clause where
showsPrec p = showParen (p > 1) . foldr (.) id
. List.intersperse (showString " | ") . map (showsPrec 2)
. IntSet.toList . clauseSet
formulaEmpty :: Formula
formulaEmpty = mempty
formulaLiteral :: Literal -> Formula
formulaLiteral (Literal l) = fromClause (Clause (IntSet.singleton l))
fromClause :: Clause -> Formula
fromClause c = Formula { formulaSet = Seq.singleton c }
formulaNot :: Literal
-> Literal
-> Formula
{-# inlineable formulaNot #-}
formulaNot (Literal out) (Literal inp) = formulaFromList cls
where
cls = [ [-out, -inp], [out, inp] ]
formulaAnd :: Literal
-> [Literal]
-> Formula
{-# inlineable formulaAnd #-}
formulaAnd (Literal out) inpLs = formulaFromList cls
where
cls = (out : map negate inps) : map (\inp -> [-out, inp]) inps
inps = map literalId inpLs
formulaOr :: Literal
-> [Literal]
-> Formula
{-# inlineable formulaOr #-}
formulaOr (Literal out) inpLs = formulaFromList cls
where
cls = (-out : inps)
: map (\inp -> [out, -inp]) inps
inps = map literalId inpLs
formulaXor :: Literal
-> Literal
-> Literal
-> Formula
{-# inlineable formulaXor #-}
formulaXor (Literal out) (Literal inpA) (Literal inpB) = formulaFromList cls
where
cls = [ [-out, -inpA, -inpB]
, [-out, inpA, inpB]
, [ out, -inpA, inpB]
, [ out, inpA, -inpB]
]
formulaMux :: Literal
-> Literal
-> Literal
-> Literal
-> Formula
{-# inlineable formulaMux #-}
formulaMux (Literal x) (Literal f) (Literal t) (Literal s) =
formulaFromList cls
where
cls = [ [-s, -t, x], [ s, -f, x], [-t, -f, x]
, [-s, t, -x], [ s, f, -x], [ t, f, -x]
]
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS (Literal x) (Literal a) (Literal b) (Literal c) =
formulaFromList cls
where
cls =
[ [ a, b, c, -x], [-a, -b, -c, x]
, [ a, -b, -c, -x], [-a, b, c, x]
, [-a, b, -c, -x], [ a, -b, c, x]
, [-a, -b, c, -x], [ a, b, -c, x]
]
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC (Literal x) (Literal a) (Literal b) (Literal c) =
formulaFromList cls
where
cls =
[ [ -b, -c, x], [b, c, -x]
, [ -a, -c, x], [a, c, -x]
, [ -a, -b, x], [a, b, -x]
]
formulaFromList :: [[Int]] -> Formula
{-# inline formulaFromList #-}
formulaFromList = foldMap ( fromClause . Clause . IntSet.fromList )