module Ersatz.Bit
( Bit(..)
, assert
, Boolean(..)
) where
import Prelude hiding ((&&),(||),not,and,or)
import qualified Prelude
import Control.Applicative
import Data.Traversable (Traversable, traverse)
import Data.Typeable
import Ersatz.Decoding
import Ersatz.Encoding
import Ersatz.Monad
import Ersatz.Internal.Circuit
import Ersatz.Internal.Formula
import Ersatz.Internal.Literal
import Ersatz.Internal.StableName
import Ersatz.Solution
import Ersatz.Variable
import GHC.Generics
import System.IO.Unsafe
infixr 3 &&, &&#
infixr 2 ||, ||#
infixr 0 ==>, ==>#
newtype Bit = Bit (Circuit Bit)
deriving (Show, Typeable)
instance Boolean Bit where
bool True = true
bool False = false
true = Bit (Var (lit True))
false = Bit (Var (lit False))
Bit (And as) && Bit (And bs) = and (as ++ bs)
Bit (And as) && b = and (as ++ [b])
a && Bit (And bs) = and (a : bs)
a && b = and [a,b]
Bit (Or as) || Bit (Or bs) = or (as ++ bs)
Bit (Or as) || b = or (as ++ [b])
a || Bit (Or bs) = or (a : bs)
a || b = or [a,b]
x ==> y = not x || y
not (Bit (Not c)) = c
not (Bit (Var b)) = Bit (Var (negateLit b))
not c = Bit (Not c)
a `xor` b = Bit (Xor a b)
and xs = Bit (And xs)
or xs = Bit (Or xs)
choose f t s = Bit (Mux f t s)
instance Variable Bit where
exists = Bit . Var <$> exists
forall = Bit . Var <$> forall
instance Decoding Bit where
type Decoded Bit = Bool
decode sol b@(Bit c)
= solutionStableName sol (unsafePerformIO (makeStableName' b))
<|> case c of
And cs -> andMaybeBools $ decode sol <$> cs
Or cs -> orMaybeBools $ decode sol <$> cs
Xor x y -> xor <$> decode sol x <*> decode sol y
Mux cf ct cp -> do
p <- decode sol cp
decode sol $ if p then ct else cf
Not c' -> not <$> decode sol c'
Var l -> decode sol l
where
andMaybeBools :: [Maybe Bool] -> Maybe Bool
andMaybeBools mbs
| any not knowns = Just False
| null unknowns = Just True
| otherwise = Nothing
where
(unknowns, knowns) = partitionMaybes mbs
orMaybeBools :: [Maybe Bool] -> Maybe Bool
orMaybeBools mbs
| or knowns = Just True
| null unknowns = Just False
| otherwise = Nothing
where
(unknowns, knowns) = partitionMaybes mbs
partitionMaybes :: [Maybe a] -> ([()], [a])
partitionMaybes = foldr go ([],[])
where
go Nothing ~(ns, js) = (():ns, js)
go (Just a) ~(ns, js) = (ns, a:js)
instance Encoding Bit where
type Encoded Bit = Bool
encode = bool
assert :: MonadSAT m => Bit -> m ()
assert b = do
l <- runBit b
assertFormula (formulaLiteral l)
runBit :: MonadSAT m => Bit -> m Literal
runBit (Bit (Not c)) = negateLiteral <$> runBit c
runBit (Bit (Var (Lit l))) = return l
runBit b@(Bit c) = generateLiteral b $ \out ->
assertFormula =<< case c of
And bs -> formulaAnd out <$> traverse runBit bs
Or bs -> formulaOr out <$> traverse runBit bs
Xor x y -> formulaXor out <$> runBit x <*> runBit y
Mux x y p -> formulaMux out <$> runBit x <*> runBit y <*> runBit p
Var (Bool False) -> return $ formulaLiteral (negateLiteral out)
Var (Bool True) -> return $ formulaLiteral out
Not _ -> error "Unreachable"
Var (Lit _) -> error "Unreachable"
class GBoolean f where
gbool :: Bool -> f a
(&&#) :: f a -> f a -> f a
(||#) :: f a -> f a -> f a
(==>#) :: f a -> f a -> f a
gnot :: f a -> f a
gand :: [f a] -> f a
gor :: [f a] -> f a
gxor :: f a -> f a -> f a
instance GBoolean U1 where
gbool _ = U1
U1 &&# U1 = U1
U1 ||# U1 = U1
U1 ==># U1 = U1
gnot U1 = U1
gand _ = U1
gor _ = U1
gxor _ _ = U1
instance (GBoolean f, GBoolean g) => GBoolean (f :*: g) where
gbool x = gbool x :*: gbool x
(a :*: b) &&# (c :*: d) = (a &&# c) :*: (b &&# d)
(a :*: b) ||# (c :*: d) = (a ||# c) :*: (b ||# d)
(a :*: b) ==># (c :*: d) = (a ==># c) :*: (b ==># d)
gnot (a :*: b) = gnot a :*: gnot b
gand xs = gand (map (\(x :*: _) -> x) xs) :*: gand (map (\(_ :*: x) -> x) xs)
gor xs = gor (map (\(x :*: _) -> x) xs) :*: gor (map (\(_ :*: x) -> x) xs)
gxor (a :*: b) (c :*: d) = gxor a c :*: gxor b d
instance Boolean a => GBoolean (K1 i a) where
gbool = K1 . bool
K1 a &&# K1 b = K1 (a && b)
K1 a ||# K1 b = K1 (a || b)
K1 a ==># K1 b = K1 (a ==> b)
gnot (K1 a) = K1 (not a)
gand as = K1 (and (map (\(K1 a) -> a) as))
gor as = K1 (or (map (\(K1 a) -> a) as))
gxor (K1 a) (K1 b) = K1 (xor a b)
instance GBoolean a => GBoolean (M1 i c a) where
gbool = M1 . gbool
M1 a &&# M1 b = M1 (a &&# b)
M1 a ||# M1 b = M1 (a ||# b)
M1 a ==># M1 b = M1 (a ==># b)
gnot (M1 a) = M1 (gnot a)
gand as = M1 (gand (map (\(M1 a) -> a) as))
gor as = M1 (gor (map (\(M1 a) -> a) as))
gxor (M1 a) (M1 b) = M1 (gxor a b)
class Boolean t where
bool :: Bool -> t
default bool :: (Generic t, GBoolean (Rep t)) => Bool -> t
bool = to . gbool
true :: t
true = bool True
false :: t
false = bool False
(&&) :: t -> t -> t
default (&&) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
x && y = to (from x &&# from y)
(||) :: t -> t -> t
default (||) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
x || y = to (from x ||# from y)
(==>) :: t -> t -> t
default (==>) :: (Generic t, GBoolean (Rep t)) => t -> t -> t
x ==> y = to (from x ==># from y)
not :: t -> t
default not :: (Generic t, GBoolean (Rep t)) => t -> t
not = to . gnot . from
and :: [t] -> t
default and :: (Generic t, GBoolean (Rep t)) => [t] -> t
and = to . gand . map from
or :: [t] -> t
default or :: (Generic t, GBoolean (Rep t)) => [t] -> t
or = to . gor . map from
nand :: [t] -> t
nand = not . and
nor :: [t] -> t
nor = not . or
xor :: t -> t -> t
default xor :: (Generic t, GBoolean (Rep t)) => t -> t -> t
xor x y = to (from x `gxor` from y)
choose :: t
-> t
-> t
-> t
choose f t s = (f && not s) || (t && s)
instance Boolean Bool where
bool = id
true = True
false = False
(&&) = (Prelude.&&)
(||) = (Prelude.||)
x ==> y = not x || y
not = Prelude.not
and = Prelude.and
or = Prelude.or
False `xor` False = False
False `xor` True = True
True `xor` False = True
True `xor` True = False
choose f _ False = f
choose _ t True = t