-- Hoogle documentation, generated by Haddock
-- See Hoogle, http://www.haskell.org/hoogle/


-- | A library for working with the SMTLIB format.
--   
--   A library for working with the SMTLIB format.
@package smtLib
@version 1.0

module SMTLib2.Core
tBool :: Type
true :: Expr
false :: Expr
not :: Expr -> Expr
(==>) :: Expr -> Expr -> Expr
and :: Expr -> Expr -> Expr
or :: Expr -> Expr -> Expr
xor :: Expr -> Expr -> Expr
(===) :: Expr -> Expr -> Expr
(=/=) :: Expr -> Expr -> Expr
ite :: Expr -> Expr -> Expr -> Expr

module SMTLib2.BitVector
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

module SMTLib2.Array
tArray :: Type -> Type -> Type
select :: Expr -> Expr -> Expr
store :: Expr -> Expr -> Expr -> Expr

module SMTLib2

module SMTLib2.Compat1
data Trans a
OK :: a -> Trans a
Fail :: Doc -> Trans a
toMaybe :: Trans a -> Maybe a
toEither :: Trans a -> Either Doc a
err :: Doc -> Trans a
name :: Name -> Name
ident :: Ident -> Ident
quant :: Quant -> Quant
binder :: Binder -> Binder
sort :: Sort -> Type
literal :: Literal -> Literal
term :: Term -> Trans Expr
formula :: Formula -> Trans Expr
annot :: Annot -> Trans Attr
command :: Command -> Trans [Command]
script :: Script -> Trans Script
instance Applicative Trans
instance Functor Trans

module SMTLib1

module SMTLib1.QF_BV
tBitVec :: Integer -> Sort
isBitVec :: Sort -> Maybe Integer

-- | BitVec[1]
bit0 :: Term

-- | BitVec[1]
bit1 :: Term

-- | <ul>
--   <li><i>m</i> -&gt; [n] -&gt; [m+n]</li>
--   </ul>
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

module SMTLib1.QF_AUFBV

-- | 'tArray i n' is an array indexed by bitvectors of widht <tt>i</tt>,
--   and storing bitvectors of width <tt>n</tt>.
tArray :: Integer -> Integer -> Sort

-- | <pre>
--   select array index
--   </pre>
select :: Term -> Term -> Term

-- | <pre>
--   store array index value
--   </pre>
store :: Term -> Term -> Term -> Term