{-# language MultiParamTypeClasses #-}
module Satchmo.Binary.Op.Fixed
( restricted
, add, times, dot_product, dot_product'
, module Satchmo.Binary.Data
, module Satchmo.Binary.Op.Common
, restrictedTimes
)
where
import Prelude hiding ( and, or, not, min, max )
import qualified Prelude
import Control.Monad (foldM)
import qualified Satchmo.Code as C
import Satchmo.Boolean
import Satchmo.Binary.Data
import Satchmo.Binary.Op.Common
import qualified Satchmo.Binary.Op.Times as T
import qualified Satchmo.Binary.Op.Flexible as Flexible
import Satchmo.Counting
import Control.Monad ( forM, when )
import Data.Map ( Map )
import qualified Data.Map as M
restricted :: (MonadSAT m) => Int -> Number -> m Number
restricted :: forall (m :: * -> *). MonadSAT m => Int -> Number -> m Number
restricted Int
w Number
a = do
let ( [Boolean]
low, [Boolean]
high ) = Int -> [Boolean] -> ([Boolean], [Boolean])
forall a. Int -> [a] -> ([a], [a])
splitAt Int
w ([Boolean] -> ([Boolean], [Boolean]))
-> [Boolean] -> ([Boolean], [Boolean])
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
[m ()] -> m [()]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
forall (m :: * -> *) a. Monad m => [m a] -> m [a]
sequence ([m ()] -> m [()]) -> [m ()] -> m [()]
forall a b. (a -> b) -> a -> b
$ do Boolean
x <- [Boolean]
high ; m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
x ]
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]
low
add :: (MonadSAT m) => Number -> Number -> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b = do
Boolean
false <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
let w :: Int
w = Int -> Int -> Int
forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
[Boolean]
zs <- Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
false ( Number -> [Boolean]
bits Number
a ) ( Number -> [Boolean]
bits Number
b )
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
add_with_carry :: (MonadSAT m) => Int -> Boolean -> Booleans -> Booleans -> m Booleans
add_with_carry :: forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
c [Boolean]
xxs [Boolean]
yys = case ( [Boolean]
xxs, [Boolean]
yys ) of
([Boolean], [Boolean])
_ | Int
w Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
0 -> do
[m ()] -> m ()
forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ ([m ()] -> m ()) -> [m ()] -> m ()
forall a b. (a -> b) -> a -> b
$ do Boolean
p <- Boolean
c Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: [Boolean]
xxs [Boolean] -> [Boolean] -> [Boolean]
forall a. [a] -> [a] -> [a]
++ [Boolean]
yys ; m () -> [m ()]
forall a. a -> [a]
forall (m :: * -> *) a. Monad m => a -> m a
return (m () -> [m ()]) -> m () -> [m ()]
forall a b. (a -> b) -> a -> b
$ [Boolean] -> m ()
forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
p ]
[Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return []
( [] , [] ) -> [Boolean] -> m [Boolean]
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return [ Boolean
c ]
( [], Boolean
y : [Boolean]
ys) -> do
(Boolean
r,Boolean
d) <- Boolean -> Boolean -> m (Boolean, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder Boolean
c Boolean
y
[Boolean]
rest <- Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Boolean
d [] [Boolean]
ys
[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
r Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: [Boolean]
rest
( Boolean
x : [Boolean]
xs, [] ) -> Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry Int
w Boolean
c [Boolean]
yys [Boolean]
xxs
(Boolean
x : [Boolean]
xs, Boolean
y:[Boolean]
ys) -> do
(Boolean
r,Boolean
d) <- Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder Boolean
c Boolean
x Boolean
y
[Boolean]
rest <- Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wInt -> Int -> Int
forall a. Num a => a -> a -> a
-Int
1) Boolean
d [Boolean]
xs [Boolean]
ys
[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
r Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: [Boolean]
rest
times :: (MonadSAT m) => Number -> Number -> m Number
times :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
times Number
a Number
b = do
let w :: Int
w = Int -> Int -> Int
forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
Maybe Int -> Number -> Number -> m Number
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
T.times (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
w) Number
a Number
b
dot_product :: (MonadSAT m)
=> Int -> [ Number ] -> [ Number ] -> m Number
dot_product :: forall (m :: * -> *).
MonadSAT m =>
Int -> [Number] -> [Number] -> m Number
dot_product Int
w [Number]
xs [Number]
ys = do
Maybe Int -> [Number] -> [Number] -> m Number
forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> [Number] -> [Number] -> m Number
T.dot_product (Int -> Maybe Int
forall a. a -> Maybe a
Just Int
w) [Number]
xs [Number]
ys
dot_product' :: [Number] -> [Number] -> m Number
dot_product' [Number]
xs [Number]
ys = do
let l :: Number -> Int
l = [Boolean] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length ([Boolean] -> Int) -> (Number -> [Boolean]) -> Number -> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
bits
w :: Int
w = [Int] -> Int
forall a. Ord a => [a] -> a
forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum ([Int] -> Int) -> [Int] -> Int
forall a b. (a -> b) -> a -> b
$ Int
0 Int -> [Int] -> [Int]
forall a. a -> [a] -> [a]
: (Number -> Int) -> [Number] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
l ( [Number]
xs [Number] -> [Number] -> [Number]
forall a. [a] -> [a] -> [a]
++ [Number]
ys )
Int -> [Number] -> [Number] -> m Number
forall (m :: * -> *).
MonadSAT m =>
Int -> [Number] -> [Number] -> m Number
dot_product Int
w [Number]
xs [Number]
ys
restrictedAdd :: (MonadSAT m) => Number -> Number -> m Number
restrictedAdd :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedAdd Number
a Number
b = do
Boolean
zero <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
([Boolean]
result, Boolean
_) <- Boolean -> [Boolean] -> [Boolean] -> m ([Boolean], Boolean)
forall (m :: * -> *).
MonadSAT m =>
Boolean -> [Boolean] -> [Boolean] -> m ([Boolean], Boolean)
Flexible.add_with_carry Boolean
zero (Number -> [Boolean]
bits Number
a) (Number -> [Boolean]
bits Number
b)
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]
result
restrictedShift :: (MonadSAT m) => Number -> m Number
restrictedShift :: forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
a = do
Boolean
zero <- Bool -> m Boolean
forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
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] -> Number) -> [Boolean] -> Number
forall a b. (a -> b) -> a -> b
$ Boolean
zero Boolean -> [Boolean] -> [Boolean]
forall a. a -> [a] -> [a]
: (Int -> [Boolean] -> [Boolean]
forall a. Int -> [a] -> [a]
take (Number -> Int
width Number
a Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1) ([Boolean] -> [Boolean]) -> [Boolean] -> [Boolean]
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a)
restrictedTimes :: (MonadSAT m) => Number -> Number -> m Number
restrictedTimes :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedTimes Number
as Number
bs = do
(Number, Number)
result <- ((Number, Number) -> Boolean -> m (Number, Number))
-> (Number, Number) -> [Boolean] -> m (Number, Number)
forall (t :: * -> *) (m :: * -> *) b a.
(Foldable t, Monad m) =>
(b -> a -> m b) -> b -> t a -> m b
foldM (\(Number
as',Number
sum) Boolean
b -> do
Number
summand <- Boolean -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
Flexible.times1 Boolean
b Number
as'
Number
sum' <- Number
sum Number -> Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
`restrictedAdd` Number
summand
Number
nextAs' <- Number -> m Number
forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
as'
(Number, Number) -> m (Number, Number)
forall a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Number
nextAs', Number
sum')
) (Number
as, [Boolean] -> Number
make []) ([Boolean] -> m (Number, Number))
-> [Boolean] -> m (Number, Number)
forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
bs
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
$ (Number, Number) -> Number
forall a b. (a, b) -> b
snd (Number, Number)
result