Satchmo.Binary.Op.Fixed

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.

Documentation

restricted :: MonadSAT m => Int -> Number -> m Number

give only lower k bits, upper bits must be zero, (else unsatisfiable)

add :: MonadSAT m => Number -> Number -> m Number

result bit width is max of argument bit widths. if overflow occurs, then formula is unsatisfiable.

times :: MonadSAT m => Number -> Number -> m Number

result bit width is at most max of argument bit widths. if overflow occurs, then formula is unsatisfiable.

dot_product :: MonadSAT m => Int -> [Number] -> [Number] -> m Number

dot_product' :: MonadSAT m => [Number] -> [Number] -> m Number

data Number

Instances

Numeric Number

Create Number

Constant Number

Decode m Boolean Bool => Decode m Number Integer

bits :: Number -> [Boolean]

make :: [Boolean] -> Number

width :: Number -> Int

number :: MonadSAT m => Int -> m Number

declare a number variable (bit width)

constant :: MonadSAT m => Integer -> m Number

Declare a number constant

constantWidth :: MonadSAT m => Int -> Integer -> m Number

constantWidth w declares a number constant using at least w bits

fromBinary :: [Bool] -> Integer

toBinary :: Integer -> [Bool]

toBinaryWidth :: Int -> Integer -> [Bool]

toBinaryWidth w converts to binary using at least w bits

module Satchmo.Binary.Op.Common

restrictedTimes :: MonadSAT m => Number -> Number -> m Number