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

restricted :: Int -> Number -> SAT Number

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

add :: Number -> Number -> SAT Number

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

times :: Number -> Number -> SAT Number

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

data Number

Instances

Decode Number Integer

bits :: Number -> [Boolean]

make :: [Boolean] -> Number

width :: Number -> Int

number :: Int -> SAT Number

declare a number variable (bit width)

constant :: Integer -> SAT Number

declare a number constant

equals :: Number -> Number -> SAT Boolean

iszero :: Number -> SAT Boolean