{-# LANGUAGE CPP #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE TypeFamilies #-}
{-# 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 { Clause -> IntSet
clauseSet :: IntSet }
deriving (Clause -> Clause -> Bool
(Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool) -> Eq Clause
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Clause -> Clause -> Bool
$c/= :: Clause -> Clause -> Bool
== :: Clause -> Clause -> Bool
$c== :: Clause -> Clause -> Bool
Eq, Eq Clause
Eq Clause
-> (Clause -> Clause -> Ordering)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Bool)
-> (Clause -> Clause -> Clause)
-> (Clause -> Clause -> Clause)
-> Ord Clause
Clause -> Clause -> Bool
Clause -> Clause -> Ordering
Clause -> Clause -> Clause
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Clause -> Clause -> Clause
$cmin :: Clause -> Clause -> Clause
max :: Clause -> Clause -> Clause
$cmax :: Clause -> Clause -> Clause
>= :: Clause -> Clause -> Bool
$c>= :: Clause -> Clause -> Bool
> :: Clause -> Clause -> Bool
$c> :: Clause -> Clause -> Bool
<= :: Clause -> Clause -> Bool
$c<= :: Clause -> Clause -> Bool
< :: Clause -> Clause -> Bool
$c< :: Clause -> Clause -> Bool
compare :: Clause -> Clause -> Ordering
$ccompare :: Clause -> Clause -> Ordering
$cp1Ord :: Eq Clause
Ord, Typeable)
clauseLiterals :: Clause -> [Literal]
clauseLiterals :: Clause -> [Literal]
clauseLiterals (Clause IntSet
is) = Int -> Literal
Literal (Int -> Literal) -> [Int] -> [Literal]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> IntSet -> [Int]
IntSet.toList IntSet
is
instance Semigroup Clause where
Clause IntSet
x <> :: Clause -> Clause -> Clause
<> Clause IntSet
y = IntSet -> Clause
Clause (IntSet
x IntSet -> IntSet -> IntSet
forall a. Semigroup a => a -> a -> a
<> IntSet
y)
instance Monoid Clause where
mempty :: Clause
mempty = IntSet -> Clause
Clause IntSet
forall a. Monoid a => a
mempty
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
fromLiteral :: Literal -> Clause
fromLiteral :: Literal -> Clause
fromLiteral Literal
l = Clause :: IntSet -> Clause
Clause { clauseSet :: IntSet
clauseSet = Int -> IntSet
IntSet.singleton (Int -> IntSet) -> Int -> IntSet
forall a b. (a -> b) -> a -> b
$ Literal -> Int
literalId Literal
l }
newtype Formula = Formula { Formula -> Seq Clause
formulaSet :: Seq Clause }
deriving (Formula -> Formula -> Bool
(Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool) -> Eq Formula
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: Formula -> Formula -> Bool
$c/= :: Formula -> Formula -> Bool
== :: Formula -> Formula -> Bool
$c== :: Formula -> Formula -> Bool
Eq, Eq Formula
Eq Formula
-> (Formula -> Formula -> Ordering)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Bool)
-> (Formula -> Formula -> Formula)
-> (Formula -> Formula -> Formula)
-> Ord Formula
Formula -> Formula -> Bool
Formula -> Formula -> Ordering
Formula -> Formula -> Formula
forall a.
Eq a
-> (a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Formula -> Formula -> Formula
$cmin :: Formula -> Formula -> Formula
max :: Formula -> Formula -> Formula
$cmax :: Formula -> Formula -> Formula
>= :: Formula -> Formula -> Bool
$c>= :: Formula -> Formula -> Bool
> :: Formula -> Formula -> Bool
$c> :: Formula -> Formula -> Bool
<= :: Formula -> Formula -> Bool
$c<= :: Formula -> Formula -> Bool
< :: Formula -> Formula -> Bool
$c< :: Formula -> Formula -> Bool
compare :: Formula -> Formula -> Ordering
$ccompare :: Formula -> Formula -> Ordering
$cp1Ord :: Eq Formula
Ord, Typeable)
instance Semigroup Formula where
Formula Seq Clause
x <> :: Formula -> Formula -> Formula
<> Formula Seq Clause
y = Seq Clause -> Formula
Formula (Seq Clause
x Seq Clause -> Seq Clause -> Seq Clause
forall a. Semigroup a => a -> a -> a
<> Seq Clause
y)
instance Monoid Formula where
mempty :: Formula
mempty = Seq Clause -> Formula
Formula Seq Clause
forall a. Monoid a => a
mempty
#if !(MIN_VERSION_base(4,11,0))
mappend = (<>)
#endif
instance Show Formula where
showsPrec :: Int -> Formula -> ShowS
showsPrec Int
p = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
2) (ShowS -> ShowS) -> (Formula -> ShowS) -> Formula -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id
([ShowS] -> ShowS) -> (Formula -> [ShowS]) -> Formula -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
showString String
" & ") ([ShowS] -> [ShowS]) -> (Formula -> [ShowS]) -> Formula -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Clause -> ShowS) -> [Clause] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Clause -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
3)
([Clause] -> [ShowS])
-> (Formula -> [Clause]) -> Formula -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Seq Clause -> [Clause]
forall (t :: * -> *) a. Foldable t => t a -> [a]
Data.Foldable.toList (Seq Clause -> [Clause])
-> (Formula -> Seq Clause) -> Formula -> [Clause]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Formula -> Seq Clause
formulaSet
instance Show Clause where
showsPrec :: Int -> Clause -> ShowS
showsPrec Int
p = Bool -> ShowS -> ShowS
showParen (Int
p Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
1) (ShowS -> ShowS) -> (Clause -> ShowS) -> Clause -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (ShowS -> ShowS -> ShowS) -> ShowS -> [ShowS] -> ShowS
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ShowS -> ShowS -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.) ShowS
forall a. a -> a
id
([ShowS] -> ShowS) -> (Clause -> [ShowS]) -> Clause -> ShowS
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ShowS -> [ShowS] -> [ShowS]
forall a. a -> [a] -> [a]
List.intersperse (String -> ShowS
showString String
" | ") ([ShowS] -> [ShowS]) -> (Clause -> [ShowS]) -> Clause -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int -> ShowS) -> [Int] -> [ShowS]
forall a b. (a -> b) -> [a] -> [b]
map (Int -> Int -> ShowS
forall a. Show a => Int -> a -> ShowS
showsPrec Int
2)
([Int] -> [ShowS]) -> (Clause -> [Int]) -> Clause -> [ShowS]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> [Int]
IntSet.toList (IntSet -> [Int]) -> (Clause -> IntSet) -> Clause -> [Int]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Clause -> IntSet
clauseSet
formulaEmpty :: Formula
formulaEmpty :: Formula
formulaEmpty = Formula
forall a. Monoid a => a
mempty
formulaLiteral :: Literal -> Formula
formulaLiteral :: Literal -> Formula
formulaLiteral (Literal Int
l) = Clause -> Formula
fromClause (IntSet -> Clause
Clause (Int -> IntSet
IntSet.singleton Int
l))
fromClause :: Clause -> Formula
fromClause :: Clause -> Formula
fromClause Clause
c = Formula :: Seq Clause -> Formula
Formula { formulaSet :: Seq Clause
formulaSet = Clause -> Seq Clause
forall a. a -> Seq a
Seq.singleton Clause
c }
formulaNot :: Literal
-> Literal
-> Formula
{-# inlineable formulaNot #-}
formulaNot :: Literal -> Literal -> Formula
formulaNot (Literal Int
out) (Literal Int
inp) = [[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls = [ [-Int
out, -Int
inp], [Int
out, Int
inp] ]
formulaAnd :: Literal
-> [Literal]
-> Formula
{-# inlineable formulaAnd #-}
formulaAnd :: Literal -> [Literal] -> Formula
formulaAnd (Literal Int
out) [Literal]
inpLs = [[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls = (Int
out Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Int -> Int) -> [Int] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Int -> Int
forall a. Num a => a -> a
negate [Int]
inps) [Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
: (Int -> [Int]) -> [Int] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
inp -> [-Int
out, Int
inp]) [Int]
inps
inps :: [Int]
inps = (Literal -> Int) -> [Literal] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Int
literalId [Literal]
inpLs
formulaOr :: Literal
-> [Literal]
-> Formula
{-# inlineable formulaOr #-}
formulaOr :: Literal -> [Literal] -> Formula
formulaOr (Literal Int
out) [Literal]
inpLs = [[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls = (-Int
out Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: [Int]
inps)
[Int] -> [[Int]] -> [[Int]]
forall a. a -> [a] -> [a]
: (Int -> [Int]) -> [Int] -> [[Int]]
forall a b. (a -> b) -> [a] -> [b]
map (\Int
inp -> [Int
out, -Int
inp]) [Int]
inps
inps :: [Int]
inps = (Literal -> Int) -> [Literal] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Literal -> Int
literalId [Literal]
inpLs
formulaXor :: Literal
-> Literal
-> Literal
-> Formula
{-# inlineable formulaXor #-}
formulaXor :: Literal -> Literal -> Literal -> Formula
formulaXor (Literal Int
out) (Literal Int
inpA) (Literal Int
inpB) = [[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls = [ [-Int
out, -Int
inpA, -Int
inpB]
, [-Int
out, Int
inpA, Int
inpB]
, [ Int
out, -Int
inpA, Int
inpB]
, [ Int
out, Int
inpA, -Int
inpB]
]
formulaMux :: Literal
-> Literal
-> Literal
-> Literal
-> Formula
{-# inlineable formulaMux #-}
formulaMux :: Literal -> Literal -> Literal -> Literal -> Formula
formulaMux (Literal Int
x) (Literal Int
f) (Literal Int
t) (Literal Int
s) =
[[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls = [ [-Int
s, -Int
t, Int
x], [ Int
s, -Int
f, Int
x], [-Int
t, -Int
f, Int
x]
, [-Int
s, Int
t, -Int
x], [ Int
s, Int
f, -Int
x], [ Int
t, Int
f, -Int
x]
]
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAS (Literal Int
x) (Literal Int
a) (Literal Int
b) (Literal Int
c) =
[[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls =
[ [ Int
a, Int
b, Int
c, -Int
x], [-Int
a, -Int
b, -Int
c, Int
x]
, [ Int
a, -Int
b, -Int
c, -Int
x], [-Int
a, Int
b, Int
c, Int
x]
, [-Int
a, Int
b, -Int
c, -Int
x], [ Int
a, -Int
b, Int
c, Int
x]
, [-Int
a, -Int
b, Int
c, -Int
x], [ Int
a, Int
b, -Int
c, Int
x]
]
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC :: Literal -> Literal -> Literal -> Literal -> Formula
formulaFAC (Literal Int
x) (Literal Int
a) (Literal Int
b) (Literal Int
c) =
[[Int]] -> Formula
formulaFromList [[Int]]
cls
where
cls :: [[Int]]
cls =
[ [ -Int
b, -Int
c, Int
x], [Int
b, Int
c, -Int
x]
, [ -Int
a, -Int
c, Int
x], [Int
a, Int
c, -Int
x]
, [ -Int
a, -Int
b, Int
x], [Int
a, Int
b, -Int
x]
]
formulaFromList :: [[Int]] -> Formula
{-# inline formulaFromList #-}
formulaFromList :: [[Int]] -> Formula
formulaFromList = ([Int] -> Formula) -> [[Int]] -> Formula
forall (t :: * -> *) m a.
(Foldable t, Monoid m) =>
(a -> m) -> t a -> m
foldMap ( Clause -> Formula
fromClause (Clause -> Formula) -> ([Int] -> Clause) -> [Int] -> Formula
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IntSet -> Clause
Clause (IntSet -> Clause) -> ([Int] -> IntSet) -> [Int] -> Clause
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Int] -> IntSet
IntSet.fromList )