SMTLib1.QF_BV

Documentation

tBitVec :: Integer -> Sort

isBitVec :: Sort -> Maybe Integer

bit0 :: Term

BitVec[1]

bit1 :: Term

BitVec[1]

concat :: Term -> Term -> Term

m

-> [n] -> [m+n]

extract :: Integer -> Integer -> Term -> Term

bvnot :: Term -> Term

bvand :: Term -> Term -> Term

bvor :: Term -> Term -> Term

bvneg :: Term -> Term

bvadd :: Term -> Term -> Term

bvmul :: Term -> Term -> Term

bvudiv :: Term -> Term -> Term

bvurem :: Term -> Term -> Term

bvshl :: Term -> Term -> Term

bvlshr :: Term -> Term -> Term

bv :: Integer -> Integer -> Term

bvnand :: Term -> Term -> Term

bvnor :: Term -> Term -> Term

bvxor :: Term -> Term -> Term

bvxnor :: Term -> Term -> Term

bvcomp :: Term -> Term -> Term

bvsub :: Term -> Term -> Term

bvsdiv :: Term -> Term -> Term

bvsrem :: Term -> Term -> Term

bvsmod :: Term -> Term -> Term

bvashr :: Term -> Term -> Term

repeat :: Integer -> Term -> Term

zero_extend :: Integer -> Term -> Term

sign_extend :: Integer -> Term -> Term

rotate_left :: Integer -> Term -> Term

rotate_right :: Integer -> Term -> Term

bvule :: Term -> Term -> Formula

bvugt :: Term -> Term -> Formula

bvuge :: Term -> Term -> Formula

bvslt :: Term -> Term -> Formula

bvsle :: Term -> Term -> Formula

bvsgt :: Term -> Term -> Formula

bvsge :: Term -> Term -> Formula