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.

- restricted :: MonadSAT m => Int -> Number -> m Number
- add :: MonadSAT m => Number -> Number -> m Number
- times :: MonadSAT m => Number -> Number -> m Number
- data Number
- bits :: Number -> [Boolean]
- make :: [Boolean] -> Number
- width :: Number -> Int
- number :: MonadSAT m => Int -> m Number
- constant :: MonadSAT m => Integer -> m Number
- module Satchmo.Binary.Op.Common

# Documentation

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

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

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

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

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

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

module Satchmo.Binary.Op.Common