smtLib-1.0.8: A library for working with the SMTLIB format.

Safe Haskell | Safe
Language | Haskell98

SMTLib1.QF_BV

Synopsis

- tBitVec :: Integer -> Sort
- isBitVec :: Sort -> Maybe Integer
- bit0 :: Term
- bit1 :: Term
- concat :: Term -> Term -> Term
- 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

# Documentation

tBitVec :: Integer -> Sort Source #

isBitVec :: Sort -> Maybe Integer Source #

bit0 :: Term Source #

BitVec[1]

bit1 :: Term Source #

BitVec[1]

concat :: Term -> Term -> Term Source #

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

extract :: Integer -> Integer -> Term -> Term Source #

bvnot :: Term -> Term Source #

bvand :: Term -> Term -> Term Source #

bvor :: Term -> Term -> Term Source #

bvneg :: Term -> Term Source #

bvadd :: Term -> Term -> Term Source #

bvmul :: Term -> Term -> Term Source #

bvudiv :: Term -> Term -> Term Source #

bvurem :: Term -> Term -> Term Source #

bvshl :: Term -> Term -> Term Source #

bvlshr :: Term -> Term -> Term Source #

bv :: Integer -> Integer -> Term Source #

bvnand :: Term -> Term -> Term Source #

bvnor :: Term -> Term -> Term Source #

bvxor :: Term -> Term -> Term Source #

bvxnor :: Term -> Term -> Term Source #

bvcomp :: Term -> Term -> Term Source #

bvsub :: Term -> Term -> Term Source #

bvsdiv :: Term -> Term -> Term Source #

bvsrem :: Term -> Term -> Term Source #

bvsmod :: Term -> Term -> Term Source #

bvashr :: Term -> Term -> Term Source #

repeat :: Integer -> Term -> Term Source #

zero_extend :: Integer -> Term -> Term Source #

sign_extend :: Integer -> Term -> Term Source #

rotate_left :: Integer -> Term -> Term Source #

rotate_right :: Integer -> Term -> Term Source #

bvule :: Term -> Term -> Formula Source #

bvugt :: Term -> Term -> Formula Source #

bvuge :: Term -> Term -> Formula Source #

bvslt :: Term -> Term -> Formula Source #

bvsle :: Term -> Term -> Formula Source #

bvsgt :: Term -> Term -> Formula Source #

bvsge :: Term -> Term -> Formula Source #