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

Safe HaskellNone

SMTLib1.QF_BV

Synopsis

Documentation

bit0 :: TermSource

BitVec[1]

bit1 :: TermSource

BitVec[1]

concat :: Term -> Term -> TermSource

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

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

bvnot :: Term -> TermSource

bvand :: Term -> Term -> TermSource

bvor :: Term -> Term -> TermSource

bvneg :: Term -> TermSource

bvadd :: Term -> Term -> TermSource

bvmul :: Term -> Term -> TermSource

bvudiv :: Term -> Term -> TermSource

bvurem :: Term -> Term -> TermSource

bvshl :: Term -> Term -> TermSource

bvlshr :: Term -> Term -> TermSource

bv :: Integer -> Integer -> TermSource

bvnand :: Term -> Term -> TermSource

bvnor :: Term -> Term -> TermSource

bvxor :: Term -> Term -> TermSource

bvxnor :: Term -> Term -> TermSource

bvcomp :: Term -> Term -> TermSource

bvsub :: Term -> Term -> TermSource

bvsdiv :: Term -> Term -> TermSource

bvsrem :: Term -> Term -> TermSource

bvsmod :: Term -> Term -> TermSource

bvashr :: Term -> Term -> TermSource

repeat :: Integer -> Term -> TermSource

zero_extend :: Integer -> Term -> TermSource

sign_extend :: Integer -> Term -> TermSource

rotate_left :: Integer -> Term -> TermSource

rotate_right :: Integer -> Term -> TermSource

bvule :: Term -> Term -> FormulaSource

bvugt :: Term -> Term -> FormulaSource

bvuge :: Term -> Term -> FormulaSource

bvslt :: Term -> Term -> FormulaSource

bvsle :: Term -> Term -> FormulaSource

bvsgt :: Term -> Term -> FormulaSource

bvsge :: Term -> Term -> FormulaSource