Copyright | (c) Masahiro Sakai 2016 |
---|---|
License | BSD-style |
Maintainer | masahiro.sakai@gmail.com |
Stability | experimental |
Safe Haskell | None |
Language | Haskell2010 |
- data BV
- bv2nat :: Integral a => BV -> a
- nat2bv :: IsBV a => Int -> Integer -> a
- fromAscBits :: IsBV a => [Bool] -> a
- fromDescBits :: IsBV a => [Bool] -> a
- toAscBits :: BV -> [Bool]
- toDescBits :: BV -> [Bool]
- class Monoid a => IsBV a where
- data Var = Var {}
- data Expr
- data Op1
- data Op2
- repeat :: Monoid m => Int -> m -> m
- zeroExtend :: IsBV a => Int -> a -> a
- signExtend :: IsBV a => Int -> a -> a
- data Atom = Rel (OrdRel Expr) Bool
- class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where
- type ComparisonResult a
- module ToySolver.Data.OrdRel
- type Model = (Vector BV, Map BV BV, Map BV BV)
- evalExpr :: Model -> Expr -> BV
- evalAtom :: Model -> Atom -> Bool
BitVector values
fromAscBits :: IsBV a => [Bool] -> a Source #
fromDescBits :: IsBV a => [Bool] -> a Source #
toDescBits :: BV -> [Bool] Source #
class Monoid a => IsBV a where Source #
width, extract, fromBV, bvnot, bvand, bvor, bvxor, bvneg, bvadd, bvmul, bvudiv, bvurem, bvsdiv, bvsrem, bvsmod, bvshl, bvlshr, bvashr, bvcomp
extract :: Int -> Int -> a -> a Source #
bvnand :: a -> a -> a Source #
bvxnor :: a -> a -> a Source #
bvudiv :: a -> a -> a Source #
bvurem :: a -> a -> a Source #
bvsdiv :: a -> a -> a Source #
bvsrem :: a -> a -> a Source #
bvsmod :: a -> a -> a Source #
bvlshr :: a -> a -> a Source #
BitVector language
zeroExtend :: IsBV a => Int -> a -> a Source #
signExtend :: IsBV a => Int -> a -> a Source #
class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where Source #
type ComparisonResult a Source #
module ToySolver.Data.OrdRel