Satchmo.BinaryTwosComplement.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

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

subtract :: MonadSAT m => Number -> Number -> m Number

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

increment :: MonadSAT m => Number -> m Number

negate :: MonadSAT m => Number -> m Number

linear :: MonadSAT m => Number -> Number -> Number -> m Number

data Number

Instances

Numeric Number

Create Number

Constant Number

Decode m Boolean Bool => Decode m Number Integer

bits :: Number -> [Boolean]

fromBooleans :: [Boolean] -> Number

Make a number from its binary representation

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

Get a number variable of given bit width

toUnsigned :: Number -> Number

Convert to unsigned number (see Satchmo.Binary.Op.Flexible)

fromUnsigned :: Number -> Number

Convert from unsigned number (see Satchmo.Binary.Op.Flexible). The result is interpreted as a positive or negative number, depending on its most significant bit.

width :: Number -> Int

Get bit width

isNull :: Number -> Bool

isNull n == True if width n == 0

msb :: Number -> Boolean

Most significant bit

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

Get a number constant

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

constantWidth w declares a number constant using at least w bits

equals :: MonadSAT m => Number -> Number -> m Boolean

eq :: MonadSAT m => Number -> Number -> m Boolean

lt :: MonadSAT m => Number -> Number -> m Boolean

le :: MonadSAT m => Number -> Number -> m Boolean

ge :: MonadSAT m => Number -> Number -> m Boolean

gt :: MonadSAT m => Number -> Number -> m Boolean

positive :: MonadSAT m => Number -> m Boolean

negative :: MonadSAT m => Number -> m Boolean

nonNegative :: MonadSAT m => Number -> m Boolean