Safe Haskell	None
Language	Haskell98

Satchmo.BinaryTwosComplement.Op.Fixed

Description

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.

Synopsis

Documentation

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

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

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

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

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

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

data Number Source

Instances

Numeric Number
Create Number
Constant Number
Decode m Boolean Bool => Decode m Number Integer

bits :: Number -> [Boolean] Source

fromBooleans :: [Boolean] -> Number Source

Make a number from its binary representation

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

Get a number variable of given bit width

toUnsigned :: Number -> Number Source

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

fromUnsigned :: Number -> Number Source

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 Source

Get bit width

isNull :: Number -> Bool Source

isNull n == True if width n == 0

msb :: Number -> Boolean Source

Most significant bit

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

Get a number constant

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

constantWidth w declares a number constant using at least w bits

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

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

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

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

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

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

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

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

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