Satchmo.Integer

Documentation

data Number

Instances

Decode m Boolean Bool => Decode m Number Integer

make :: [Boolean] -> Number

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

declare a number variable (bit width)

constant

Arguments

:: MonadSAT m

=> Int

bit width

-> Integer

value

-> m Number

declare a number constant

decode :: (Decode m Boolean Bool, Integral b) => b -> Number -> m Integer

bits :: Number -> [Boolean]

lsb first, using two's complement

width :: Number -> Int

sign :: Number -> Boolean

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

negate. Unsatisfiable if value is lowest negatve.

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

sub :: MonadSAT m => Number -> Number -> m Number

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

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

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

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