SMTLib2.BitVector

Documentation

tBitVec :: Integer -> Type

bv :: Integer -> Integer -> Expr

concat :: Expr -> Expr -> Expr

extract :: Integer -> Integer -> Expr -> Expr

bvnot :: Expr -> Expr

bvand :: Expr -> Expr -> Expr

bvor :: Expr -> Expr -> Expr

bvneg :: Expr -> Expr

bvadd :: Expr -> Expr -> Expr

bvmul :: Expr -> Expr -> Expr

bvudiv :: Expr -> Expr -> Expr

bvurem :: Expr -> Expr -> Expr

bvshl :: Expr -> Expr -> Expr

bvlshr :: Expr -> Expr -> Expr

bvult :: Expr -> Expr -> Expr

bvnand :: Expr -> Expr -> Expr

bvnor :: Expr -> Expr -> Expr

bvxor :: Expr -> Expr -> Expr

bvxnor :: Expr -> Expr -> Expr

bvcomp :: Expr -> Expr -> Expr

bvsub :: Expr -> Expr -> Expr

bvsdiv :: Expr -> Expr -> Expr

bvsrem :: Expr -> Expr -> Expr

bvsmod :: Expr -> Expr -> Expr

bvashr :: Expr -> Expr -> Expr

repeat :: Integer -> Expr -> Expr -> Expr

zero_extend :: Integer -> Expr -> Expr

sign_extend :: Integer -> Expr -> Expr

rotate_left :: Integer -> Expr -> Expr

rotate_right :: Integer -> Expr -> Expr

bvule :: Expr -> Expr -> Expr

bvugt :: Expr -> Expr -> Expr

bvuge :: Expr -> Expr -> Expr

bvslt :: Expr -> Expr -> Expr

bvsle :: Expr -> Expr -> Expr

bvsgt :: Expr -> Expr -> Expr

bvsge :: Expr -> Expr -> Expr