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 Satchmo.Counting

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
    -- equals' ( bits a ) ( bits b )
    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

-- | i flag is True, then the number itself, and zero otherwise.
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 ) -- ^ (less, equals)

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 ) -- ^ (result, carry)
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 ) -- ^ (result, carry)
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
    -- d <- fun2 ( \ x y -> 1   < s x y ) a b
    Boolean
d <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
a, Boolean
b ] -- makes three clauses (not four)
    forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r, Boolean
d )