Copyright	(c) Masahiro Sakai 2016
License	BSD-style
Maintainer	masahiro.sakai@gmail.com
Stability	experimental
Safe Haskell	None
Language	Haskell2010

ToySolver.BitVector.Base

Contents

BitVector values
BitVector language
Orphan instances

Description

Synopsis

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
- width :: a -> Int
- extract :: Int -> Int -> a -> a
- fromBV :: BV -> a
- bvnot :: a -> a
- bvand :: a -> a -> a
- bvor :: a -> a -> a
- bvxor :: a -> a -> a
- bvnand :: a -> a -> a
- bvnor :: a -> a -> a
- bvxnor :: a -> a -> a
- bvneg :: a -> a
- bvadd :: a -> a -> a
- bvsub :: a -> a -> a
- bvmul :: a -> a -> a
- bvudiv :: a -> a -> a
- bvurem :: a -> a -> a
- bvsdiv :: a -> a -> a
- bvsrem :: a -> a -> a
- bvsmod :: a -> a -> a
- bvshl :: a -> a -> a
- bvlshr :: a -> a -> a
- bvashr :: a -> a -> a
- bvcomp :: a -> a -> a
data Var = Var {
- varWidth :: !Int
- varId :: !Int
}
data Expr
- = EConst BV
- | EVar Var
- | EOp1 Op1 Expr
- | EOp2 Op2 Expr Expr
data Op1
- = OpExtract !Int !Int
- | OpNot
- | OpNeg
data Op2
- = OpConcat
- | OpAnd
- | OpOr
- | OpXOr
- | OpComp
- | OpAdd
- | OpMul
- | OpUDiv
- | OpURem
- | OpSDiv
- | OpSRem
- | OpSMod
- | OpShl
- | OpLShr
- | OpAShr
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
- bvule, bvult, bvuge, bvugt, bvsle, bvslt, bvsge, bvsgt :: a -> a -> 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

data BV Source #

Instances

Eq BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: BV -> BV -> Bool # (/=) :: BV -> BV -> Bool #
Ord BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: BV -> BV -> Ordering # (<) :: BV -> BV -> Bool # (<=) :: BV -> BV -> Bool # (>) :: BV -> BV -> Bool # (>=) :: BV -> BV -> Bool # max :: BV -> BV -> BV # min :: BV -> BV -> BV #
Show BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> BV -> ShowS # show :: BV -> String # showList :: [BV] -> ShowS #
Semigroup BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods (<>) :: BV -> BV -> BV # sconcat :: NonEmpty BV -> BV # stimes :: Integral b => b -> BV -> BV #
Monoid BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods mempty :: BV # mappend :: BV -> BV -> BV # mconcat :: [BV] -> BV #
Bits BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.&.) :: BV -> BV -> BV # (.\|.) :: BV -> BV -> BV # xor :: BV -> BV -> BV # complement :: BV -> BV # shift :: BV -> Int -> BV # rotate :: BV -> Int -> BV # zeroBits :: BV # bit :: Int -> BV # setBit :: BV -> Int -> BV # clearBit :: BV -> Int -> BV # complementBit :: BV -> Int -> BV # testBit :: BV -> Int -> Bool # bitSizeMaybe :: BV -> Maybe Int # bitSize :: BV -> Int # isSigned :: BV -> Bool # shiftL :: BV -> Int -> BV # unsafeShiftL :: BV -> Int -> BV # shiftR :: BV -> Int -> BV # unsafeShiftR :: BV -> Int -> BV # rotateL :: BV -> Int -> BV # rotateR :: BV -> Int -> BV # popCount :: BV -> Int #
BVComparison BV Source #
Instance details Defined in ToySolver.BitVector.Base Associated Types type ComparisonResult BV :: Type Source # Methods bvule :: BV -> BV -> ComparisonResult BV Source # bvult :: BV -> BV -> ComparisonResult BV Source # bvuge :: BV -> BV -> ComparisonResult BV Source # bvugt :: BV -> BV -> ComparisonResult BV Source # bvsle :: BV -> BV -> ComparisonResult BV Source # bvslt :: BV -> BV -> ComparisonResult BV Source # bvsge :: BV -> BV -> ComparisonResult BV Source # bvsgt :: BV -> BV -> ComparisonResult BV Source #
IsBV BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods width :: BV -> Int Source # extract :: Int -> Int -> BV -> BV Source # fromBV :: BV -> BV Source # bvnot :: BV -> BV Source # bvand :: BV -> BV -> BV Source # bvor :: BV -> BV -> BV Source # bvxor :: BV -> BV -> BV Source # bvnand :: BV -> BV -> BV Source # bvnor :: BV -> BV -> BV Source # bvxnor :: BV -> BV -> BV Source # bvneg :: BV -> BV Source # bvadd :: BV -> BV -> BV Source # bvsub :: BV -> BV -> BV Source # bvmul :: BV -> BV -> BV Source # bvudiv :: BV -> BV -> BV Source # bvurem :: BV -> BV -> BV Source # bvsdiv :: BV -> BV -> BV Source # bvsrem :: BV -> BV -> BV Source # bvsmod :: BV -> BV -> BV Source # bvshl :: BV -> BV -> BV Source # bvlshr :: BV -> BV -> BV Source # bvashr :: BV -> BV -> BV Source # bvcomp :: BV -> BV -> BV Source #
IsEqRel BV Bool Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.==.) :: BV -> BV -> Bool Source # (./=.) :: BV -> BV -> Bool Source #
type ComparisonResult BV Source #
Instance details Defined in ToySolver.BitVector.Base type ComparisonResult BV = Bool

bv2nat :: Integral a => BV -> a Source #

nat2bv :: IsBV a => Int -> Integer -> a Source #

fromAscBits :: IsBV a => [Bool] -> a Source #

fromDescBits :: IsBV a => [Bool] -> a Source #

toAscBits :: BV -> [Bool] Source #

toDescBits :: BV -> [Bool] Source #

class Monoid a => IsBV a where Source #

Minimal complete definition

width, extract, fromBV, bvnot, bvand, bvor, bvxor, bvneg, bvadd, bvmul, bvudiv, bvurem, bvsdiv, bvsrem, bvsmod, bvshl, bvlshr, bvashr, bvcomp

Methods

width :: a -> Int Source #

extract :: Int -> Int -> a -> a Source #

fromBV :: BV -> a Source #

bvnot :: a -> a Source #

bvand :: a -> a -> a Source #

bvor :: a -> a -> a Source #

bvxor :: a -> a -> a Source #

bvnand :: a -> a -> a Source #

bvnor :: a -> a -> a Source #

bvxnor :: a -> a -> a Source #

bvneg :: a -> a Source #

bvadd :: a -> a -> a Source #

bvsub :: a -> a -> a Source #

bvmul :: 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 #

bvshl :: a -> a -> a Source #

bvlshr :: a -> a -> a Source #

bvashr :: a -> a -> a Source #

bvcomp :: a -> a -> a Source #

Instances

IsBV Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods width :: Expr -> Int Source # extract :: Int -> Int -> Expr -> Expr Source # fromBV :: BV -> Expr Source # bvnot :: Expr -> Expr Source # bvand :: Expr -> Expr -> Expr Source # bvor :: Expr -> Expr -> Expr Source # bvxor :: Expr -> Expr -> Expr Source # bvnand :: Expr -> Expr -> Expr Source # bvnor :: Expr -> Expr -> Expr Source # bvxnor :: Expr -> Expr -> Expr Source # bvneg :: Expr -> Expr Source # bvadd :: Expr -> Expr -> Expr Source # bvsub :: Expr -> Expr -> Expr Source # bvmul :: Expr -> Expr -> Expr Source # bvudiv :: Expr -> Expr -> Expr Source # bvurem :: Expr -> Expr -> Expr Source # bvsdiv :: Expr -> Expr -> Expr Source # bvsrem :: Expr -> Expr -> Expr Source # bvsmod :: Expr -> Expr -> Expr Source # bvshl :: Expr -> Expr -> Expr Source # bvlshr :: Expr -> Expr -> Expr Source # bvashr :: Expr -> Expr -> Expr Source # bvcomp :: Expr -> Expr -> Expr Source #
IsBV BV Source #
Instance details Defined in ToySolver.BitVector.Base Methods width :: BV -> Int Source # extract :: Int -> Int -> BV -> BV Source # fromBV :: BV -> BV Source # bvnot :: BV -> BV Source # bvand :: BV -> BV -> BV Source # bvor :: BV -> BV -> BV Source # bvxor :: BV -> BV -> BV Source # bvnand :: BV -> BV -> BV Source # bvnor :: BV -> BV -> BV Source # bvxnor :: BV -> BV -> BV Source # bvneg :: BV -> BV Source # bvadd :: BV -> BV -> BV Source # bvsub :: BV -> BV -> BV Source # bvmul :: BV -> BV -> BV Source # bvudiv :: BV -> BV -> BV Source # bvurem :: BV -> BV -> BV Source # bvsdiv :: BV -> BV -> BV Source # bvsrem :: BV -> BV -> BV Source # bvsmod :: BV -> BV -> BV Source # bvshl :: BV -> BV -> BV Source # bvlshr :: BV -> BV -> BV Source # bvashr :: BV -> BV -> BV Source # bvcomp :: BV -> BV -> BV Source #

BitVector language

data Var Source #

Constructors

Var
Fields varWidth :: !Int varId :: !Int

Instances

Eq Var Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: Var -> Var -> Bool # (/=) :: Var -> Var -> Bool #
Ord Var Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: Var -> Var -> Ordering # (<) :: Var -> Var -> Bool # (<=) :: Var -> Var -> Bool # (>) :: Var -> Var -> Bool # (>=) :: Var -> Var -> Bool # max :: Var -> Var -> Var # min :: Var -> Var -> Var #
Show Var Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> Var -> ShowS # show :: Var -> String # showList :: [Var] -> ShowS #

data Expr Source #

Constructors

EConst BV
EVar Var
EOp1 Op1 Expr
EOp2 Op2 Expr Expr

Instances

Eq Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: Expr -> Expr -> Bool # (/=) :: Expr -> Expr -> Bool #
Ord Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: Expr -> Expr -> Ordering # (<) :: Expr -> Expr -> Bool # (<=) :: Expr -> Expr -> Bool # (>) :: Expr -> Expr -> Bool # (>=) :: Expr -> Expr -> Bool # max :: Expr -> Expr -> Expr # min :: Expr -> Expr -> Expr #
Show Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> Expr -> ShowS # show :: Expr -> String # showList :: [Expr] -> ShowS #
Semigroup Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods (<>) :: Expr -> Expr -> Expr # sconcat :: NonEmpty Expr -> Expr # stimes :: Integral b => b -> Expr -> Expr #
Monoid Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods mempty :: Expr # mappend :: Expr -> Expr -> Expr # mconcat :: [Expr] -> Expr #
Bits Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.&.) :: Expr -> Expr -> Expr # (.\|.) :: Expr -> Expr -> Expr # xor :: Expr -> Expr -> Expr # complement :: Expr -> Expr # shift :: Expr -> Int -> Expr # rotate :: Expr -> Int -> Expr # zeroBits :: Expr # bit :: Int -> Expr # setBit :: Expr -> Int -> Expr # clearBit :: Expr -> Int -> Expr # complementBit :: Expr -> Int -> Expr # testBit :: Expr -> Int -> Bool # bitSizeMaybe :: Expr -> Maybe Int # bitSize :: Expr -> Int # isSigned :: Expr -> Bool # shiftL :: Expr -> Int -> Expr # unsafeShiftL :: Expr -> Int -> Expr # shiftR :: Expr -> Int -> Expr # unsafeShiftR :: Expr -> Int -> Expr # rotateL :: Expr -> Int -> Expr # rotateR :: Expr -> Int -> Expr # popCount :: Expr -> Int #
BVComparison Expr Source #
Instance details Defined in ToySolver.BitVector.Base Associated Types type ComparisonResult Expr :: Type Source # Methods bvule :: Expr -> Expr -> ComparisonResult Expr Source # bvult :: Expr -> Expr -> ComparisonResult Expr Source # bvuge :: Expr -> Expr -> ComparisonResult Expr Source # bvugt :: Expr -> Expr -> ComparisonResult Expr Source # bvsle :: Expr -> Expr -> ComparisonResult Expr Source # bvslt :: Expr -> Expr -> ComparisonResult Expr Source # bvsge :: Expr -> Expr -> ComparisonResult Expr Source # bvsgt :: Expr -> Expr -> ComparisonResult Expr Source #
IsBV Expr Source #
Instance details Defined in ToySolver.BitVector.Base Methods width :: Expr -> Int Source # extract :: Int -> Int -> Expr -> Expr Source # fromBV :: BV -> Expr Source # bvnot :: Expr -> Expr Source # bvand :: Expr -> Expr -> Expr Source # bvor :: Expr -> Expr -> Expr Source # bvxor :: Expr -> Expr -> Expr Source # bvnand :: Expr -> Expr -> Expr Source # bvnor :: Expr -> Expr -> Expr Source # bvxnor :: Expr -> Expr -> Expr Source # bvneg :: Expr -> Expr Source # bvadd :: Expr -> Expr -> Expr Source # bvsub :: Expr -> Expr -> Expr Source # bvmul :: Expr -> Expr -> Expr Source # bvudiv :: Expr -> Expr -> Expr Source # bvurem :: Expr -> Expr -> Expr Source # bvsdiv :: Expr -> Expr -> Expr Source # bvsrem :: Expr -> Expr -> Expr Source # bvsmod :: Expr -> Expr -> Expr Source # bvshl :: Expr -> Expr -> Expr Source # bvlshr :: Expr -> Expr -> Expr Source # bvashr :: Expr -> Expr -> Expr Source # bvcomp :: Expr -> Expr -> Expr Source #
IsEqRel Expr Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.==.) :: Expr -> Expr -> Atom Source # (./=.) :: Expr -> Expr -> Atom Source #
type ComparisonResult Expr Source #
Instance details Defined in ToySolver.BitVector.Base type ComparisonResult Expr = Atom

data Op1 Source #

Constructors

OpExtract !Int !Int
OpNot
OpNeg

Instances

Eq Op1 Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: Op1 -> Op1 -> Bool # (/=) :: Op1 -> Op1 -> Bool #
Ord Op1 Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: Op1 -> Op1 -> Ordering # (<) :: Op1 -> Op1 -> Bool # (<=) :: Op1 -> Op1 -> Bool # (>) :: Op1 -> Op1 -> Bool # (>=) :: Op1 -> Op1 -> Bool # max :: Op1 -> Op1 -> Op1 # min :: Op1 -> Op1 -> Op1 #
Show Op1 Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> Op1 -> ShowS # show :: Op1 -> String # showList :: [Op1] -> ShowS #

data Op2 Source #

Constructors

OpConcat
OpAnd
OpOr
OpXOr
OpComp
OpAdd
OpMul
OpUDiv
OpURem
OpSDiv
OpSRem
OpSMod
OpShl
OpLShr
OpAShr

Instances

Bounded Op2 Source #
Instance details Defined in ToySolver.BitVector.Base Methods minBound :: Op2 # maxBound :: Op2 #
Enum Op2 Source #
Instance details Defined in ToySolver.BitVector.Base Methods succ :: Op2 -> Op2 # pred :: Op2 -> Op2 # toEnum :: Int -> Op2 # fromEnum :: Op2 -> Int # enumFrom :: Op2 -> [Op2] # enumFromThen :: Op2 -> Op2 -> [Op2] # enumFromTo :: Op2 -> Op2 -> [Op2] # enumFromThenTo :: Op2 -> Op2 -> Op2 -> [Op2] #
Eq Op2 Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: Op2 -> Op2 -> Bool # (/=) :: Op2 -> Op2 -> Bool #
Ord Op2 Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: Op2 -> Op2 -> Ordering # (<) :: Op2 -> Op2 -> Bool # (<=) :: Op2 -> Op2 -> Bool # (>) :: Op2 -> Op2 -> Bool # (>=) :: Op2 -> Op2 -> Bool # max :: Op2 -> Op2 -> Op2 # min :: Op2 -> Op2 -> Op2 #
Show Op2 Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> Op2 -> ShowS # show :: Op2 -> String # showList :: [Op2] -> ShowS #

repeat :: Monoid m => Int -> m -> m Source #

zeroExtend :: IsBV a => Int -> a -> a Source #

signExtend :: IsBV a => Int -> a -> a Source #

data Atom Source #

Constructors

Rel (OrdRel Expr) Bool

Instances

Eq Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods (==) :: Atom -> Atom -> Bool # (/=) :: Atom -> Atom -> Bool #
Ord Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods compare :: Atom -> Atom -> Ordering # (<) :: Atom -> Atom -> Bool # (<=) :: Atom -> Atom -> Bool # (>) :: Atom -> Atom -> Bool # (>=) :: Atom -> Atom -> Bool # max :: Atom -> Atom -> Atom # min :: Atom -> Atom -> Atom #
Show Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods showsPrec :: Int -> Atom -> ShowS # show :: Atom -> String # showList :: [Atom] -> ShowS #
Complement Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods notB :: Atom -> Atom Source #
IsEqRel Expr Atom Source #
Instance details Defined in ToySolver.BitVector.Base Methods (.==.) :: Expr -> Expr -> Atom Source # (./=.) :: Expr -> Expr -> Atom Source #

class (IsBV a, IsEqRel a (ComparisonResult a), Complement (ComparisonResult a)) => BVComparison a where Source #

Minimal complete definition

(bvule | bvult), (bvsle | bvslt)

Associated Types

type ComparisonResult a Source #

Methods

bvule :: a -> a -> ComparisonResult a Source #

bvult :: a -> a -> ComparisonResult a Source #

bvuge :: a -> a -> ComparisonResult a Source #

bvugt :: a -> a -> ComparisonResult a Source #

bvsle :: a -> a -> ComparisonResult a Source #

bvslt :: a -> a -> ComparisonResult a Source #

bvsge :: a -> a -> ComparisonResult a Source #

bvsgt :: a -> a -> ComparisonResult a Source #

Instances

BVComparison Expr Source #
Instance details Defined in ToySolver.BitVector.Base Associated Types type ComparisonResult Expr :: Type Source # Methods bvule :: Expr -> Expr -> ComparisonResult Expr Source # bvult :: Expr -> Expr -> ComparisonResult Expr Source # bvuge :: Expr -> Expr -> ComparisonResult Expr Source # bvugt :: Expr -> Expr -> ComparisonResult Expr Source # bvsle :: Expr -> Expr -> ComparisonResult Expr Source # bvslt :: Expr -> Expr -> ComparisonResult Expr Source # bvsge :: Expr -> Expr -> ComparisonResult Expr Source # bvsgt :: Expr -> Expr -> ComparisonResult Expr Source #
BVComparison BV Source #
Instance details Defined in ToySolver.BitVector.Base Associated Types type ComparisonResult BV :: Type Source # Methods bvule :: BV -> BV -> ComparisonResult BV Source # bvult :: BV -> BV -> ComparisonResult BV Source # bvuge :: BV -> BV -> ComparisonResult BV Source # bvugt :: BV -> BV -> ComparisonResult BV Source # bvsle :: BV -> BV -> ComparisonResult BV Source # bvslt :: BV -> BV -> ComparisonResult BV Source # bvsge :: BV -> BV -> ComparisonResult BV Source # bvsgt :: BV -> BV -> ComparisonResult BV Source #

module ToySolver.Data.OrdRel

type Model = (Vector BV, Map BV BV, Map BV BV) Source #

evalExpr :: Model -> Expr -> BV Source #

evalAtom :: Model -> Atom -> Bool Source #

Orphan instances

IsEqRel BV Bool Source #
Instance details Methods (.==.) :: BV -> BV -> Bool Source # (./=.) :: BV -> BV -> Bool Source #