module Satchmo.Binary.Op.Common
( iszero
, equals, lt, le, ge, eq, gt
, full_adder, half_adder
, select
, max, min, maximum
)
where
import Prelude hiding ( and, or, not, compare, max, min, maximum )
import qualified Prelude
import qualified Satchmo.Code as C
import Satchmo.Boolean
(MonadSAT, Boolean, Booleans
, fun2, fun3, and, or, not, xor, assertOr, assert, boolean)
import qualified Satchmo.Boolean as B
import Satchmo.Binary.Data (Number, number, make, bits, width)
import Control.Monad ( forM, foldM )
import Control.Monad ( forM )
iszero :: (MonadSAT m) => Number -> m Boolean
iszero :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
iszero Number
a = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
a forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make []
equals :: (MonadSAT m) => Number -> Number -> m Boolean
equals :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
a Number
b = do
let m :: Int
m = forall a. Ord a => a -> a -> a
Prelude.min ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
let ( [Boolean]
a1, [Boolean]
a2 ) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
m forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
let ( [Boolean]
b1, [Boolean]
b2 ) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
m forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b
[Boolean]
common <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( forall a b. [a] -> [b] -> [(a, b)]
zip [Boolean]
a1 [Boolean]
b1 ) forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) Boolean
x Boolean
y
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ [Boolean]
common forall a. [a] -> [a] -> [a]
++ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not ( [Boolean]
a2 forall a. [a] -> [a] -> [a]
++ [Boolean]
b2 )
equals' :: (MonadSAT m) => Booleans -> Booleans -> m Boolean
equals' :: forall (m :: * -> *).
MonadSAT m =>
[Boolean] -> [Boolean] -> m Boolean
equals' [] [] = forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
equals' (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = do
Boolean
z <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) Boolean
x Boolean
y
Boolean
rest <- forall (m :: * -> *).
MonadSAT m =>
[Boolean] -> [Boolean] -> m Boolean
equals' [Boolean]
xs [Boolean]
ys
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
z, Boolean
rest ]
equals' [Boolean]
xs [] = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not [Boolean]
xs
equals' [] [Boolean]
ys = forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
not [Boolean]
ys
le,lt,ge,gt,eq :: MonadSAT m => Number -> Number -> m Boolean
le :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le Number
x Number
y = do (Boolean
l,Boolean
e) <- forall (m :: * -> *).
MonadSAT m =>
Number -> Number -> m (Boolean, Boolean)
compare Number
x Number
y ; forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean
l,Boolean
e]
lt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
x Number
y = do (Boolean
l,Boolean
e) <- forall (m :: * -> *).
MonadSAT m =>
Number -> Number -> m (Boolean, Boolean)
compare Number
x Number
y ; forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
l
ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge Number
x Number
y = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
le Number
y Number
x
gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt Number
x Number
y = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
y Number
x
eq :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
eq = forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals
max :: MonadSAT m => Number -> Number -> m Number
max :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
max Number
a Number
b = do
Number
c <- forall (m :: * -> *). MonadSAT m => Int -> m Number
number forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
Boolean
ca <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
c Number
a
Boolean
cb <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
c Number
b
Boolean
g <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt Number
a Number
b
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
g , Boolean
ca ]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean
g , Boolean
cb ]
forall (m :: * -> *) a. Monad m => a -> m a
return Number
c
min :: MonadSAT m => Number -> Number -> m Number
min :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
min Number
a Number
b = do
Number
c <- forall (m :: * -> *). MonadSAT m => Int -> m Number
number forall a b. (a -> b) -> a -> b
$ forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
Boolean
ca <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
c Number
a
Boolean
cb <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
equals Number
c Number
b
Boolean
g <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
lt Number
a Number
b
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
g , Boolean
ca ]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [ Boolean
g , Boolean
cb ]
forall (m :: * -> *) a. Monad m => a -> m a
return Number
c
maximum :: [Number] -> m Number
maximum (Number
x:[Number]
xs) = forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
max Number
x [Number]
xs
select :: MonadSAT m => Boolean -> Number -> m Number
select :: forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
select Boolean
flag Number
a = do
[Boolean]
bs <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( Number -> [Boolean]
bits Number
a ) forall a b. (a -> b) -> a -> b
$ \ Boolean
b -> forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
flag, Boolean
b ]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
bs
compare :: MonadSAT m => Number -> Number
-> m ( Boolean, Boolean )
compare :: forall (m :: * -> *).
MonadSAT m =>
Number -> Number -> m (Boolean, Boolean)
compare Number
a Number
b = forall (m :: * -> *).
MonadSAT m =>
[Boolean] -> [Boolean] -> m (Boolean, Boolean)
compare' ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )
compare' :: (MonadSAT m) => Booleans
-> Booleans
-> m ( Boolean, Boolean )
compare' :: forall (m :: * -> *).
MonadSAT m =>
[Boolean] -> [Boolean] -> m (Boolean, Boolean)
compare' [] [] = do
Boolean
f <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
Boolean
t <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
f, Boolean
t )
compare' (Boolean
x:[Boolean]
xs) (Boolean
y:[Boolean]
ys) = do
Boolean
l <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not Boolean
x, Boolean
y ]
Boolean
e <- forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
xor [ Boolean
x, Boolean
y ]
( Boolean
ll, Boolean
ee ) <- forall (m :: * -> *).
MonadSAT m =>
[Boolean] -> [Boolean] -> m (Boolean, Boolean)
compare' [Boolean]
xs [Boolean]
ys
Boolean
lee <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [Boolean
l,Boolean
ee]
Boolean
l' <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean
ll, Boolean
lee ]
Boolean
e' <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
e, Boolean
ee ]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
l', Boolean
e' )
compare' [Boolean]
xs [] = do
Boolean
x <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean]
xs
Boolean
never <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
never, Boolean -> Boolean
not Boolean
x )
compare' [] [Boolean]
ys = do
Boolean
y <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean]
ys
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
y, Boolean -> Boolean
not Boolean
y )
full_adder :: (MonadSAT m)
=> Boolean -> Boolean -> Boolean
-> m ( Boolean , Boolean )
full_adder :: forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder = forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder_0
full_adder_1 :: Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder_1 Boolean
p1 Boolean
p2 Boolean
p3 = do
Boolean
p4 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean ; Boolean
p5 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p3, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean
p4, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean
p2, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean
p3, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean -> Boolean
not Boolean
p4, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p2, Boolean -> Boolean
not Boolean
p3, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p2, Boolean
p4, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p2, Boolean
p3, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p2, Boolean -> Boolean
not Boolean
p4, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p3, Boolean
p4, Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p3, Boolean -> Boolean
not Boolean
p4, Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean -> Boolean
not Boolean
p3, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean
p3, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean
p2, Boolean -> Boolean
not Boolean
p3, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean
p2, Boolean
p3, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean -> Boolean
not Boolean
p3, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean
p3, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean
p2, Boolean -> Boolean
not Boolean
p3, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean
p2, Boolean
p3, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
p4, Boolean
p5 )
full_adder_0 :: Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder_0 Boolean
p1 Boolean
p2 Boolean
p3 = do
Boolean
p4 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean ; Boolean
p5 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p2,Boolean
p4,Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p2,Boolean -> Boolean
not Boolean
p4,Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean -> Boolean
not Boolean
p3,Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean -> Boolean
not Boolean
p2,Boolean -> Boolean
not Boolean
p3,Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean -> Boolean
not Boolean
p2,Boolean
p3,Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean
p2,Boolean
p3,Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean
p3,Boolean -> Boolean
not Boolean
p5]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean -> Boolean
not Boolean
p2,Boolean -> Boolean
not Boolean
p3,Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean
p2,Boolean -> Boolean
not Boolean
p3,Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean
p2,Boolean
p3,Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
p4, Boolean
p5 )
full_adder_plain :: Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder_plain Boolean
a Boolean
b Boolean
c = do
let s :: a -> a -> a -> Int
s a
x a
y a
z = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Enum a => a -> Int
fromEnum [a
x,a
y,a
z]
Boolean
r <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool -> Bool)
-> Boolean -> Boolean -> Boolean -> m Boolean
fun3 ( \ Bool
x Bool
y Bool
z -> forall a. Integral a => a -> Bool
odd forall a b. (a -> b) -> a -> b
$ forall {a}. Enum a => a -> a -> a -> Int
s Bool
x Bool
y Bool
z ) Boolean
a Boolean
b Boolean
c
Boolean
d <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool -> Bool)
-> Boolean -> Boolean -> Boolean -> m Boolean
fun3 ( \ Bool
x Bool
y Bool
z -> Int
1 forall a. Ord a => a -> a -> Bool
< forall {a}. Enum a => a -> a -> a -> Int
s Bool
x Bool
y Bool
z ) Boolean
a Boolean
b Boolean
c
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r, Boolean
d )
full_adder_from_half :: Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder_from_half Boolean
a Boolean
b Boolean
c = do
(Boolean
p,Boolean
q) <- forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_plain Boolean
a Boolean
b
(Boolean
r,Boolean
s) <- forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_plain Boolean
p Boolean
c
Boolean
qs <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean
q,Boolean
s]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r, Boolean
qs )
half_adder :: (MonadSAT m)
=> Boolean -> Boolean
-> m ( Boolean, Boolean )
half_adder :: forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder = forall {m :: * -> *}.
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_plain
half_adder_1 :: Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_1 Boolean
p1 Boolean
p2 = do
Boolean
p3 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean ; Boolean
p4 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p2, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p3, Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean -> Boolean
not Boolean
p3]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean
p2, Boolean
p3]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p1, Boolean
p3, Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean -> Boolean
not Boolean
p2, Boolean
p3]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean
p1, Boolean
p2, Boolean -> Boolean
not Boolean
p3]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assert [Boolean -> Boolean
not Boolean
p2, Boolean
p3, Boolean
p4]
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean
p3,Boolean
p4)
half_adder_0 :: Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_0 Boolean
p1 Boolean
p2 = do
Boolean
p3 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean ; Boolean
p4 <- forall (m :: * -> *). MonadSAT m => m Boolean
boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p2,Boolean
p3,Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p2,Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean
p3,Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean -> Boolean
not Boolean
p1,Boolean -> Boolean
not Boolean
p2,Boolean -> Boolean
not Boolean
p3]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean -> Boolean
not Boolean
p4]
forall (m :: * -> *). MonadSAT m => [Boolean] -> m ()
assertOr [Boolean
p1,Boolean
p2,Boolean -> Boolean
not Boolean
p3]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
p3, Boolean
p4 )
half_adder_plain :: Boolean -> Boolean -> m (Boolean, Boolean)
half_adder_plain Boolean
a Boolean
b = do
let s :: a -> a -> Int
s a
x a
y = forall (t :: * -> *) a. (Foldable t, Num a) => t a -> a
sum forall a b. (a -> b) -> a -> b
$ forall a b. (a -> b) -> [a] -> [b]
map forall a. Enum a => a -> Int
fromEnum [a
x,a
y]
Boolean
r <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 ( \ Bool
x Bool
y -> forall a. Integral a => a -> Bool
odd forall a b. (a -> b) -> a -> b
$ forall {a}. Enum a => a -> a -> Int
s Bool
x Bool
y ) Boolean
a Boolean
b
Boolean
d <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
a, Boolean
b ]
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r, Boolean
d )