smtLib-1.0.7: 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