satchmo- SAT encoding monad

Safe HaskellNone



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.



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