{-# language MultiParamTypeClasses #-}

-- | operations with fixed bit width.
-- still they are non-overflowing:
-- if overflow occurs, the constraints are not satisfiable.
-- the bit width of the result of binary operations
-- is the max of the bit width of the inputs.

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

-- | give only lower k bits, upper bits must be zero,
-- (else unsatisfiable)
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 ) = forall a. Int -> [a] -> ([a], [a])
splitAt Int
w forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a
    forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence forall a b. (a -> b) -> a -> b
$ do Boolean
x <- [Boolean]
high ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
x ]
    forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
low

-- | result bit width is max of argument bit widths.
-- if overflow occurs, then formula is unsatisfiable.
add :: (MonadSAT m) => Number -> Number -> m Number
add :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
add Number
a Number
b = do
    Boolean
false <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
    let w :: Int
w = forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b )
    [Boolean]
zs <- 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 )
    forall (m :: * -> *) a. Monad m => a -> m a
return 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 forall a. Ord a => a -> a -> Bool
<= Int
0 -> do
        forall (t :: * -> *) (m :: * -> *) a.
(Foldable t, Monad m) =>
t (m a) -> m ()
sequence_ forall a b. (a -> b) -> a -> b
$ do Boolean
p <- Boolean
c forall a. a -> [a] -> [a]
: [Boolean]
xxs forall a. [a] -> [a] -> [a]
++ [Boolean]
yys ; forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall {m :: * -> *}. MonadSAT m => [Boolean] -> m ()
assertOr [ Boolean -> Boolean
not Boolean
p ]
        forall (m :: * -> *) a. Monad m => a -> m a
return []
    ( [] , [] ) -> forall (m :: * -> *) a. Monad m => a -> m a
return [ Boolean
c ]
    ( [], Boolean
y : [Boolean]
ys) -> do
        (Boolean
r,Boolean
d) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> m (Boolean, Boolean)
half_adder Boolean
c Boolean
y
        [Boolean]
rest <- forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wforall a. Num a => a -> a -> a
-Int
1) Boolean
d [] [Boolean]
ys
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rest
    ( Boolean
x : [Boolean]
xs, [] ) -> 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) <- forall (m :: * -> *).
MonadSAT m =>
Boolean -> Boolean -> Boolean -> m (Boolean, Boolean)
full_adder Boolean
c Boolean
x Boolean
y
        [Boolean]
rest <- forall (m :: * -> *).
MonadSAT m =>
Int -> Boolean -> [Boolean] -> [Boolean] -> m [Boolean]
add_with_carry (Int
wforall a. Num a => a -> a -> a
-Int
1) Boolean
d [Boolean]
xs [Boolean]
ys
        forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ Boolean
r forall a. a -> [a] -> [a]
: [Boolean]
rest

-- | result bit width is at most max of argument bit widths.
-- if overflow occurs, then formula is unsatisfiable.
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 = forall a. Ord a => a -> a -> a
Prelude.max ( Number -> Int
width Number
a ) ( Number -> Int
width Number
b ) 
    forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> Number -> Number -> m Number
T.times (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
    forall (m :: * -> *).
MonadSAT m =>
Maybe Int -> [Number] -> [Number] -> m Number
T.dot_product (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 = forall (t :: * -> *) a. Foldable t => t a -> Int
length forall b c a. (b -> c) -> (a -> b) -> a -> c
. Number -> [Boolean]
bits
        w :: Int
w = forall (t :: * -> *) a. (Foldable t, Ord a) => t a -> a
Prelude.maximum forall a b. (a -> b) -> a -> b
$ Int
0 forall a. a -> [a] -> [a]
: forall a b. (a -> b) -> [a] -> [b]
map Number -> Int
l ( [Number]
xs forall a. [a] -> [a] -> [a]
++ [Number]
ys )
    forall (m :: * -> *).
MonadSAT m =>
Int -> [Number] -> [Number] -> m Number
dot_product Int
w [Number]
xs [Number]
ys    


-- Ignores overflows
restrictedAdd :: (MonadSAT m) => Number -> Number -> m Number
restrictedAdd :: forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
restrictedAdd Number
a Number
b = do
  Boolean
zero <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
  ([Boolean]
result, 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)
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make [Boolean]
result

-- Ignores overflows
restrictedShift :: (MonadSAT m) => Number -> m Number
restrictedShift :: forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
a = do
  Boolean
zero <- forall (m :: * -> *). MonadSAT m => Bool -> m Boolean
Satchmo.Boolean.constant Bool
False
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ [Boolean] -> Number
make forall a b. (a -> b) -> a -> b
$ Boolean
zero forall a. a -> [a] -> [a]
: (forall a. Int -> [a] -> [a]
take (Number -> Int
width Number
a forall a. Num a => a -> a -> a
- Int
1) forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
a)

-- Ignores overflows
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 <- 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 <- forall (m :: * -> *). MonadSAT m => Boolean -> Number -> m Number
Flexible.times1 Boolean
b Number
as'
                       Number
sum' <- Number
sum forall (m :: * -> *). MonadSAT m => Number -> Number -> m Number
`restrictedAdd` Number
summand
                       Number
nextAs' <- forall (m :: * -> *). MonadSAT m => Number -> m Number
restrictedShift Number
as'
                       forall (m :: * -> *) a. Monad m => a -> m a
return (Number
nextAs', Number
sum')
                  ) (Number
as, [Boolean] -> Number
make []) forall a b. (a -> b) -> a -> b
$ Number -> [Boolean]
bits Number
bs
  forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. (a, b) -> b
snd (Number, Number)
result