Safe Haskell	None
Language	Haskell98

Language.Fixpoint.Smt.Bitvector

Contents

Constructor
Sizes
Operators
BitVector Sort Constructor
BitVector Expression Constructor
BitVector Type Constructor

Synopsis

data Bv = Bv !BvSize !String
data BvSize
- = S32
- | S64
data BvOp
- = BvAnd
- | BvOr
mkSort :: BvSize -> Sort
eOp :: BvOp -> [Expr] -> Expr
bvTyCon :: FTycon

Constructor

data Bv Source #

Constructors

Bv !BvSize !String

Instances

Expression Bv Source #	Construct an `Expr` using a raw string, e.g. (Bv S32 "#x02000000")
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods expr :: Bv -> Expr Source #

Sizes

data BvSize Source #

Constructors

S32
S64

Instances

Eq BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods (==) :: BvSize -> BvSize -> Bool # (/=) :: BvSize -> BvSize -> Bool #
Data BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BvSize -> c BvSize # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BvSize # toConstr :: BvSize -> Constr # dataTypeOf :: BvSize -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BvSize) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvSize) # gmapT :: (forall b. Data b => b -> b) -> BvSize -> BvSize # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvSize -> r # gmapQ :: (forall d. Data d => d -> u) -> BvSize -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BvSize -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BvSize -> m BvSize # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BvSize -> m BvSize # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BvSize -> m BvSize #
Ord BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods compare :: BvSize -> BvSize -> Ordering # (<) :: BvSize -> BvSize -> Bool # (<=) :: BvSize -> BvSize -> Bool # (>) :: BvSize -> BvSize -> Bool # (>=) :: BvSize -> BvSize -> Bool # max :: BvSize -> BvSize -> BvSize # min :: BvSize -> BvSize -> BvSize #
Show BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods showsPrec :: Int -> BvSize -> ShowS # show :: BvSize -> String # showList :: [BvSize] -> ShowS #
Generic BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Associated Types type Rep BvSize :: Type -> Type # Methods from :: BvSize -> Rep BvSize x # to :: Rep BvSize x -> BvSize #
type Rep BvSize Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector type Rep BvSize = D1 (MetaData "BvSize" "Language.Fixpoint.Smt.Bitvector" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "S32" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "S64" PrefixI False) (U1 :: Type -> Type))

Operators

data BvOp Source #

Constructors

BvAnd
BvOr

Instances

Eq BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods (==) :: BvOp -> BvOp -> Bool # (/=) :: BvOp -> BvOp -> Bool #
Data BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b) -> (forall g. g -> c g) -> BvOp -> c BvOp # gunfold :: (forall b r. Data b => c (b -> r) -> c r) -> (forall r. r -> c r) -> Constr -> c BvOp # toConstr :: BvOp -> Constr # dataTypeOf :: BvOp -> DataType # dataCast1 :: Typeable t => (forall d. Data d => c (t d)) -> Maybe (c BvOp) # dataCast2 :: Typeable t => (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c BvOp) # gmapT :: (forall b. Data b => b -> b) -> BvOp -> BvOp # gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r # gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> BvOp -> r # gmapQ :: (forall d. Data d => d -> u) -> BvOp -> [u] # gmapQi :: Int -> (forall d. Data d => d -> u) -> BvOp -> u # gmapM :: Monad m => (forall d. Data d => d -> m d) -> BvOp -> m BvOp # gmapMp :: MonadPlus m => (forall d. Data d => d -> m d) -> BvOp -> m BvOp # gmapMo :: MonadPlus m => (forall d. Data d => d -> m d) -> BvOp -> m BvOp #
Ord BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods compare :: BvOp -> BvOp -> Ordering # (<) :: BvOp -> BvOp -> Bool # (<=) :: BvOp -> BvOp -> Bool # (>) :: BvOp -> BvOp -> Bool # (>=) :: BvOp -> BvOp -> Bool # max :: BvOp -> BvOp -> BvOp # min :: BvOp -> BvOp -> BvOp #
Show BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Methods showsPrec :: Int -> BvOp -> ShowS # show :: BvOp -> String # showList :: [BvOp] -> ShowS #
Generic BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector Associated Types type Rep BvOp :: Type -> Type # Methods from :: BvOp -> Rep BvOp x # to :: Rep BvOp x -> BvOp #
type Rep BvOp Source #
Instance details Defined in Language.Fixpoint.Smt.Bitvector type Rep BvOp = D1 (MetaData "BvOp" "Language.Fixpoint.Smt.Bitvector" "liquid-fixpoint-0.8.0.2-EGSzGwrlcJrCaUaEYLNzOY" False) (C1 (MetaCons "BvAnd" PrefixI False) (U1 :: Type -> Type) :+: C1 (MetaCons "BvOr" PrefixI False) (U1 :: Type -> Type))

BitVector Sort Constructor

mkSort :: BvSize -> Sort Source #

Construct the bitvector Sort from its BvSize

BitVector Expression Constructor

eOp :: BvOp -> [Expr] -> Expr Source #

Apply some bitvector operator to a list of arguments

BitVector Type Constructor

bvTyCon :: FTycon Source #