module Satchmo.Integer.Op
( negate, add, sub, times
, gt, ge, eq
)
where
import Satchmo.Integer.Data
import Prelude hiding ( and, or, not, negate )
import Satchmo.Boolean hiding ( constant )
import qualified Satchmo.Boolean as B
import qualified Satchmo.Binary.Op.Common as C
import qualified Satchmo.Binary.Op.Flexible as F
import qualified Satchmo.Binary.Op.Times as T
import Control.Monad ( forM, when )
negate :: MonadSAT m
=> Number -> m Number
negate :: forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
n = do
let ys :: [Boolean]
ys = forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
B.not forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
Boolean
o <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
( [Boolean]
zs, Boolean
c ) <- forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> Boolean -> m ([Boolean], Boolean)
increment [Boolean]
ys Boolean
o
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ [Boolean]
ys, Boolean -> Boolean
B.not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last [Boolean]
zs ]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs
increment :: [Boolean] -> Boolean -> m ([Boolean], Boolean)
increment [] Boolean
z = forall (m :: * -> *) a. Monad m => a -> m a
return ( [], Boolean
z )
increment (Boolean
y:[Boolean]
ys) Boolean
z = do
( Boolean
r, Boolean
d ) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
C.half_adder Boolean
y Boolean
z
( [Boolean]
rs, Boolean
c ) <- [Boolean] -> Boolean -> m ([Boolean], Boolean)
increment [Boolean]
ys Boolean
d
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rs, Boolean
c )
add :: MonadSAT m
=> Number -> Number
-> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a0 Number
b0 = do
let w :: Int
w = forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a0) (Number -> Int
width Number
b0)
a :: Number
a = Int -> Number -> Number
sextn Int
w Number
a0 ; b :: Number
b = Int -> Number -> Number
sextn Int
w Number
b0
Boolean
cin <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
( [Boolean]
zs, Boolean
cout ) <-
forall (m :: * -> *).
MonadSAT m =>
Boolean -> [Boolean] -> [Boolean] -> m ([Boolean], Boolean)
F.add_with_carry Boolean
cin ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )
let c :: Number
c = [Boolean] -> Number
make [Boolean]
zs
Boolean
sab <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 forall a. Eq a => a -> a -> Bool
(==) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
b)
Boolean
sac <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 forall a. Eq a => a -> a -> Bool
(==) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
c)
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert [ Boolean -> Boolean
B.not Boolean
sab , Boolean
sac ]
forall (m :: * -> *) a. Monad m => a -> m a
return Number
c
sub :: MonadSAT m
=> Number -> Number
-> m Number
sub :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
sub Number
a Number
b = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.sub"
Number
c <- forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
b
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
c
sextn :: Int -> Number -> Number
sextn Int
w Number
n = [Boolean] -> Number
make forall a b. (a -> b) -> a -> b
$ Number -> Int -> [Boolean]
sext Number
n Int
w
times :: MonadSAT m
=> Number -> Number
-> m Number
times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times Number
a0 Number
b0 = do
let w :: Int
w = forall a. Ord a => a -> a -> a
max (Number -> Int
width Number
a0) (Number -> Int
width Number
b0)
a :: Number
a = Int -> Number -> Number
sextn Int
w Number
a0 ; b :: Number
b = Int -> Number -> Number
sextn Int
w Number
b0
[Boolean]
cs <- forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
T.times' Overflow
T.Ignore (forall a. a -> Maybe a
Just Int
w) (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
Boolean
nza <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a ; Boolean
nzb <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b
Boolean
result_should_be_nonzero <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
nza, Boolean
nzb ]
Boolean
result_is_nonzero <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean]
cs
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
result_should_be_nonzero, Boolean
result_is_nonzero ]
[Boolean]
xs <- 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
x -> forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(/=) Boolean
x (Number -> Boolean
sign Number
a)
[Boolean]
ys <- forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Number -> [Boolean]
bits Number
b) forall a b. (a -> b) -> a -> b
$ \ Boolean
y -> forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(/=) Boolean
y (Number -> Boolean
sign Number
b)
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 [Int
0..Int
wforall a. Num a => a -> a -> a
-Int
2] [Boolean]
xs) forall a b. (a -> b) -> a -> b
$ \ (Int
i,Boolean
x) ->
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 [Int
0..Int
wforall a. Num a => a -> a -> a
-Int
2] [Boolean]
ys) forall a b. (a -> b) -> a -> b
$ \ (Int
j,Boolean
y) ->
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
iforall a. Num a => a -> a -> a
+Int
jforall a. Ord a => a -> a -> Bool
>=Int
wforall a. Num a => a -> a -> a
-Int
1) forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
x, Boolean -> Boolean
not Boolean
y ]
let c :: Number
c = [Boolean] -> Number
make [Boolean]
cs
Boolean
s <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(/=) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
b)
Boolean
ok <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) Boolean
s (Number -> Boolean
sign Number
c)
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
result_is_nonzero, Boolean
ok ]
forall (m :: * -> *) a. Monad m => a -> m a
return Number
c
times_model :: MonadSAT m
=> Number -> Number
-> m Number
times_model :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times_model Number
a Number
b = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.times"
let w :: Int
w = Number -> Int
width Number
a
[Boolean]
cs <- forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
T.times' Overflow
T.Ignore (forall a. a -> Maybe a
Just (Int
2forall a. Num a => a -> a -> a
*Int
w)) (Number -> Int -> [Boolean]
sext Number
a Int
w) (Number -> Int -> [Boolean]
sext Number
b Int
w)
let ([Boolean]
small, [Boolean]
large) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
w [Boolean]
cs
Boolean
allone <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean]
large ; Boolean
allzero <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and ( forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
B.not [Boolean]
large )
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert [ Boolean
allone, Boolean
allzero ]
Boolean
e <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 forall a. Eq a => a -> a -> Bool
(==) (forall a. [a] -> a
last [Boolean]
small) (forall a. [a] -> a
head [Boolean]
large)
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert[Boolean
e]
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
small
sext :: Number -> Int -> [Boolean]
sext Number
a Int
w = Number -> [Boolean]
bits Number
a forall a. [a] -> [a] -> [a]
++ forall a. Int -> a -> [a]
replicate (Int
w forall a. Num a => a -> a -> a
- Number -> Int
width Number
a) (Number -> Boolean
sign Number
a)
positive :: MonadSAT m
=> Number
-> m Boolean
positive :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
positive Number
n = do
Boolean
ok <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or forall a b. (a -> b) -> a -> b
$ forall a. [a] -> [a]
init forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
ok, Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n ]
negative :: MonadSAT m
=> Number
-> m Boolean
negative :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
negative Number
n = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
nonnegative :: MonadSAT m
=> Number
-> m Boolean
nonnegative :: forall (m :: * -> *). MonadSAT m => Number -> m Boolean
nonnegative Number
n = do
forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
eq :: MonadSAT m
=> Number -> Number
-> m Boolean
eq :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
eq Number
a Number
b = do
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
forall a b. (a -> b) -> a -> b
$ forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.eq"
[Boolean]
eqs <- 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 ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b ) )
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 [Boolean]
eqs
gt :: MonadSAT m
=> Number -> Number
-> m Boolean
gt :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
gt Number
a Number
b = do
Boolean
diff <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a, forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b ]
Boolean
same <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) ( forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
Boolean
g <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.gt ( [Boolean] -> Number
F.make forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Number
F.make forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
diff
, forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
same, Boolean
g ]
]
ge :: MonadSAT m
=> Number -> Number
-> m Boolean
ge :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
ge Number
a Number
b = do
Boolean
diff <- forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not forall a b. (a -> b) -> a -> b
$ forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a, forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b ]
Boolean
same <- forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 forall a. Eq a => a -> a -> Bool
(==) ( forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( forall a. [a] -> a
last forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
Boolean
g <- forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.ge ( [Boolean] -> Number
F.make forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Number
F.make forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
diff
, forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
same, Boolean
g ]
]