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 = (Boolean -> Boolean) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
B.not ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
Boolean
o <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
True
( [Boolean]
zs, Boolean
c ) <- [Boolean] -> Boolean -> m ([Boolean], Boolean)
forall {m :: * -> *}.
MonadSAT m =>
[Boolean] -> Boolean -> m ([Boolean], Boolean)
increment [Boolean]
ys Boolean
o
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean]
ys, Boolean -> Boolean
B.not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
zs ]
Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
zs
increment :: [Boolean] -> Boolean -> m ([Boolean], Boolean)
increment [] Boolean
z = ([Boolean], Boolean) -> m ([Boolean], Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( [], Boolean
z )
increment (Boolean
y:[Boolean]
ys) Boolean
z = do
( Boolean
r, Boolean
d ) <- Boolean -> Boolean -> m (Boolean, Boolean)
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
([Boolean], Boolean) -> m ([Boolean], Boolean)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return ( Boolean
r Boolean -> [Boolean] -> [Boolean]
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 = Int -> Int -> Int
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 <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
B.constant Bool
False
( [Boolean]
zs, Boolean
cout ) <-
Boolean -> [Boolean] -> [Boolean] -> m ([Boolean], Boolean)
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 <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
b)
Boolean
sac <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
c)
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert [ Boolean -> Boolean
B.not Boolean
sab , Boolean
sac ]
Number -> m Number
forall a. a -> m a
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
(m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.sub"
Number
c <- Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> m Number
negate Number
b
Number -> Number -> m Number
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 ([Boolean] -> Number) -> [Boolean] -> Number
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 = Int -> Int -> Int
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 <- Overflow -> Maybe Int -> [Boolean] -> [Boolean] -> m [Boolean]
forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
T.times' Overflow
T.Ignore (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
w) (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
Boolean
nza <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a ; Boolean
nzb <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b
Boolean
result_should_be_nonzero <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
nza, Boolean
nzb ]
Boolean
result_is_nonzero <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [Boolean]
cs
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
result_should_be_nonzero, Boolean
result_is_nonzero ]
[Boolean]
xs <- [Boolean] -> (Boolean -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Number -> [Boolean]
bits Number
a) ((Boolean -> m Boolean) -> m [Boolean])
-> (Boolean -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ Boolean
x -> (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Boolean
x (Number -> Boolean
sign Number
a)
[Boolean]
ys <- [Boolean] -> (Boolean -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM (Number -> [Boolean]
bits Number
b) ((Boolean -> m Boolean) -> m [Boolean])
-> (Boolean -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ Boolean
y -> (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=) Boolean
y (Number -> Boolean
sign Number
b)
[(Int, Boolean)] -> ((Int, Boolean) -> m [()]) -> m [[()]]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [Boolean] -> [(Int, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2] [Boolean]
xs) (((Int, Boolean) -> m [()]) -> m [[()]])
-> ((Int, Boolean) -> m [()]) -> m [[()]]
forall a b. (a -> b) -> a -> b
$ \ (Int
i,Boolean
x) ->
[(Int, Boolean)] -> ((Int, Boolean) -> m ()) -> m [()]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([Int] -> [Boolean] -> [(Int, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0..Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
2] [Boolean]
ys) (((Int, Boolean) -> m ()) -> m [()])
-> ((Int, Boolean) -> m ()) -> m [()]
forall a b. (a -> b) -> a -> b
$ \ (Int
j,Boolean
y) ->
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
jInt -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>=Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
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 <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(/=) (Number -> Boolean
sign Number
a) (Number -> Boolean
sign Number
b)
Boolean
ok <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) Boolean
s (Number -> Boolean
sign Number
c)
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assert [ Boolean -> Boolean
not Boolean
result_is_nonzero, Boolean
ok ]
Number -> m Number
forall a. a -> m a
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
(m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.times"
let w :: Int
w = Number -> Int
width Number
a
[Boolean]
cs <- Overflow -> Maybe Int -> [Boolean] -> [Boolean] -> m [Boolean]
forall {m :: * -> *} {a}.
(Num a, Enum a, MonadSAT m, Ord a) =>
Overflow -> Maybe a -> [Boolean] -> [Boolean] -> m [Boolean]
T.times' Overflow
T.Ignore (Int -> Maybe Int
forall a. a -> Maybe a
Just (Int
2Int -> Int -> Int
forall 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) = Int -> [Boolean] -> ([Boolean], [Boolean])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
w [Boolean]
cs
Boolean
allone <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and [Boolean]
large ; Boolean
allzero <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
B.and ( (Boolean -> Boolean) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> [a] -> [b]
map Boolean -> Boolean
B.not [Boolean]
large )
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert [ Boolean
allone, Boolean
allzero ]
Boolean
e <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
B.fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) ([Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last [Boolean]
small) ([Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
head [Boolean]
large)
[Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
B.assert[Boolean
e]
Number -> m Number
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number -> m Number) -> Number -> m Number
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 [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ Int -> Boolean -> [Boolean]
forall a. Int -> a -> [a]
replicate (Int
w Int -> Int -> Int
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 <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or ([Boolean] -> m Boolean) -> [Boolean] -> m Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> [Boolean]
forall a. HasCallStack => [a] -> [a]
init ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
n
[Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
ok, Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
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
Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> m Boolean) -> Boolean -> m Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
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
Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Boolean -> m Boolean) -> Boolean -> m Boolean
forall a b. (a -> b) -> a -> b
$ Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
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
Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ( Number -> Int
width Number
a Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Number -> Int
width Number
b )
(m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ [Char] -> m ()
forall a. HasCallStack => [Char] -> a
error [Char]
"Satchmo.Integer.Op.eq"
[Boolean]
eqs <- [(Boolean, Boolean)]
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ( [Boolean] -> [Boolean] -> [(Boolean, Boolean)]
forall a b. [a] -> [b] -> [(a, b)]
zip ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b ) )
(((Boolean, Boolean) -> m Boolean) -> m [Boolean])
-> ((Boolean, Boolean) -> m Boolean) -> m [Boolean]
forall a b. (a -> b) -> a -> b
$ \ (Boolean
x,Boolean
y) -> (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) Boolean
x Boolean
y
[Boolean] -> m Boolean
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 <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a, [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b ]
Boolean
same <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) ( [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
Boolean
g <- Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.gt ( [Boolean] -> Number
F.make ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Number
F.make ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
diff
, [Boolean] -> m Boolean
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 <- [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean -> Boolean
not (Boolean -> Boolean) -> Boolean -> Boolean
forall a b. (a -> b) -> a -> b
$ [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a, [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b ]
Boolean
same <- (Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
forall (m :: * -> *).
MonadSAT m =>
(Bool -> Bool -> Bool) -> Boolean -> Boolean -> m Boolean
fun2 Bool -> Bool -> Bool
forall a. Eq a => a -> a -> Bool
(==) ( [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Boolean
forall a. HasCallStack => [a] -> a
last ([Boolean] -> Boolean) -> [Boolean] -> Boolean
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
Boolean
g <- Number -> Number -> m Boolean
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Boolean
F.ge ( [Boolean] -> Number
F.make ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a )
( [Boolean] -> Number
F.make ([Boolean] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
b )
([Boolean] -> m Boolean) -> [m Boolean] -> m Boolean
forall (m :: * -> *) a b. Monad m => ([a] -> m b) -> [m a] -> m b
monadic [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
or [ Boolean -> m Boolean
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return Boolean
diff
, [Boolean] -> m Boolean
forall (m :: * -> *). MonadSAT m => [Boolean] -> m Boolean
and [ Boolean
same, Boolean
g ]
]