| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Satchmo.Binary.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
- restricted :: MonadSAT m => Int -> Number -> m Number
- add :: MonadSAT m => Number -> Number -> m Number
- times :: MonadSAT m => Number -> Number -> m Number
- dot_product :: MonadSAT m => Int -> [Number] -> [Number] -> m Number
- dot_product' :: 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
- constantWidth :: MonadSAT m => Int -> Integer -> m Number
- fromBinary :: [Bool] -> Integer
- toBinary :: Integer -> [Bool]
- toBinaryWidth :: Int -> Integer -> [Bool]
- module Satchmo.Binary.Op.Common
- restrictedTimes :: MonadSAT m => Number -> Number -> m Number
Documentation
restricted :: MonadSAT m => Int -> Number -> m Number Source #
give only lower k bits, upper bits must be zero, (else unsatisfiable)
add :: MonadSAT m => Number -> Number -> m Number Source #
result bit width is max of argument bit widths. if overflow occurs, then formula is unsatisfiable.
times :: MonadSAT m => Number -> Number -> m Number Source #
result bit width is at most max of argument bit widths. if overflow occurs, then formula is unsatisfiable.
Instances
| Constant Number Source # | |
| Create Number Source # | |
| Numeric Number Source # | |
Defined in Satchmo.Binary.Numeric Methods equal :: MonadSAT m => Number -> Number -> m Boolean Source # greater_equal :: MonadSAT m => Number -> Number -> m Boolean Source # plus :: MonadSAT m => Number -> Number -> m Number Source # minus :: MonadSAT m => Number -> Number -> m Number Source # times :: MonadSAT m => Number -> Number -> m Number Source # | |
| (Monad m, Decode m Boolean Bool) => Decode m Number Integer Source # | |
constantWidth :: MonadSAT m => Int -> Integer -> m Number Source #
constantWidth w declares a number constant using at least w bits
fromBinary :: [Bool] -> Integer Source #
toBinaryWidth :: Int -> Integer -> [Bool] Source #
toBinaryWidth w converts to binary using at least w bits
module Satchmo.Binary.Op.Common