-- | all operations have fixed bit length,
-- and are unsatisfiable in case of overflows.

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. Unsatisfiable if value is lowest negatve.
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

-- | inefficient (used double-bit width computation)
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 ]
	       ]