-- 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.1

module SMTLib1
newtype Name
N :: String -> Name
data Ident
I :: Name -> [Integer] -> Ident
data Quant
Exists :: Quant
Forall :: Quant
data Conn
Not :: Conn
Implies :: Conn
And :: Conn
Or :: Conn
Xor :: Conn
Iff :: Conn
IfThenElse :: Conn
data Formula
FTrue :: Formula
FFalse :: Formula
FPred :: Ident -> [Term] -> Formula
FVar :: Name -> Formula
Conn :: Conn -> [Formula] -> Formula
Quant :: Quant -> [Binder] -> Formula -> Formula
Let :: Name -> Term -> Formula -> Formula
FLet :: Name -> Formula -> Formula -> Formula
FAnnot :: Formula -> [Annot] -> Formula
type Sort = Ident
data Binder
Bind :: Name -> Sort -> Binder
[bindVar] :: Binder -> Name
[bindSort] :: Binder -> Sort
data Term
Var :: Name -> Term
App :: Ident -> [Term] -> Term
Lit :: Literal -> Term
ITE :: Formula -> Term -> Term -> Term
TAnnot :: Term -> [Annot] -> Term
data Literal
LitNum :: Integer -> Literal
LitFrac :: Rational -> Literal
LitStr :: String -> Literal
data Annot
Attr :: Name -> Maybe String -> Annot
[attrName] :: Annot -> Name
[attrVal] :: Annot -> Maybe String
data FunDecl
FunDecl :: Ident -> [Sort] -> Sort -> [Annot] -> FunDecl
[funName] :: FunDecl -> Ident
[funArgs] :: FunDecl -> [Sort]
[funRes] :: FunDecl -> Sort
[funAnnots] :: FunDecl -> [Annot]
data PredDecl
PredDecl :: Ident -> [Sort] -> [Annot] -> PredDecl
[predName] :: PredDecl -> Ident
[predArgs] :: PredDecl -> [Sort]
[predAnnots] :: PredDecl -> [Annot]
data Status
Sat :: Status
Unsat :: Status
Unknown :: Status
data Command
CmdLogic :: Ident -> Command
CmdAssumption :: Formula -> Command
CmdFormula :: Formula -> Command
CmdStatus :: Status -> Command
CmdExtraSorts :: [Sort] -> Command
CmdExtraFuns :: [FunDecl] -> Command
CmdExtraPreds :: [PredDecl] -> Command
CmdNotes :: String -> Command
CmdAnnot :: Annot -> Command
data Script
Script :: Ident -> [Command] -> Script
[scrName] :: Script -> Ident
[scrCommands] :: Script -> [Command]
(===) :: Term -> Term -> Formula
(=/=) :: Term -> Term -> Formula

-- | For <a>Int</a>
(.<.) :: Term -> Term -> Formula

-- | For <a>Int</a>
(.>.) :: Term -> Term -> Formula
tInt :: Sort
funDef :: Ident -> [Sort] -> Sort -> Command
constDef :: Ident -> Sort -> Command
logic :: Ident -> Command
assume :: Formula -> Command
goal :: Formula -> Command
class PP t
pp :: PP t => t -> Doc

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

module SMTLib2.Array
tArray :: Type -> Type -> Type
select :: Expr -> Expr -> Expr
store :: 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.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.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 GHC.Base.Functor SMTLib2.Compat1.Trans
instance GHC.Base.Applicative SMTLib2.Compat1.Trans

module SMTLib2.Int
tInt :: Type
num :: Integral a => a -> Expr
nNeg :: Expr -> Expr
nSub :: Expr -> Expr -> Expr
nAdd :: Expr -> Expr -> Expr
nMul :: Expr -> Expr -> Expr
nDiv :: Expr -> Expr -> Expr
nMod :: Expr -> Expr -> Expr
nAbs :: Expr -> Expr
nLeq :: Expr -> Expr -> Expr
nLt :: Expr -> Expr -> Expr
nGeq :: Expr -> Expr -> Expr
nGt :: Expr -> Expr -> Expr

module SMTLib2
newtype Script
Script :: [Command] -> Script
data Binder
Bind :: Name -> Type -> Binder
[bindVar] :: Binder -> Name
[bindType] :: Binder -> Type
data Defn
Defn :: Name -> Expr -> Defn
[defVar] :: Defn -> Name
[defExpr] :: Defn -> Expr
data Type
TApp :: Ident -> [Type] -> Type
TVar :: Name -> Type
data Expr
Lit :: Literal -> Expr
App :: Ident -> Maybe Type -> [Expr] -> Expr
Quant :: Quant -> [Binder] -> Expr -> Expr
Let :: [Defn] -> Expr -> Expr
Annot :: Expr -> [Attr] -> Expr
newtype Name
N :: String -> Name
data Ident
I :: Name -> [Integer] -> Ident
data Quant
Exists :: Quant
Forall :: Quant
data Literal

-- | value, width (in bits)
LitBV :: Integer -> Integer -> Literal
LitNum :: Integer -> Literal
LitFrac :: Rational -> Literal
LitStr :: String -> Literal
data Attr
Attr :: Name -> Maybe AttrVal -> Attr
[attrName] :: Attr -> Name
[attrVal] :: Attr -> Maybe AttrVal
type AttrVal = Expr
data Command
CmdSetLogic :: Name -> Command
CmdSetOption :: Option -> Command
CmdSetInfo :: Attr -> Command
CmdDeclareType :: Name -> Integer -> Command
CmdDefineType :: Name -> [Name] -> Type -> Command
CmdDeclareConst :: Name -> Type -> Command
CmdDeclareFun :: Name -> [Type] -> Type -> Command
CmdDefineFun :: Name -> [Binder] -> Type -> Expr -> Command
CmdPush :: Integer -> Command
CmdPop :: Integer -> Command
CmdAssert :: Expr -> Command
CmdCheckSat :: Command
CmdGetAssertions :: Command
CmdGetValue :: [Expr] -> Command
CmdGetProof :: Command
CmdGetUnsatCore :: Command
CmdGetInfo :: InfoFlag -> Command
CmdGetOption :: Name -> Command
CmdComment :: String -> Command
CmdExit :: Command
data Option
OptPrintSuccess :: Bool -> Option
OptExpandDefinitions :: Bool -> Option
OptInteractiveMode :: Bool -> Option
OptProduceProofs :: Bool -> Option
OptProduceUnsatCores :: Bool -> Option
OptProduceModels :: Bool -> Option
OptProduceAssignments :: Bool -> Option
OptRegularOutputChannel :: String -> Option
OptDiagnosticOutputChannel :: String -> Option
OptRandomSeed :: Integer -> Option
OptVerbosity :: Integer -> Option
OptAttr :: Attr -> Option
data InfoFlag
InfoAllStatistics :: InfoFlag
InfoErrorBehavior :: InfoFlag
InfoName :: InfoFlag
InfoAuthors :: InfoFlag
InfoVersion :: InfoFlag
InfoStatus :: InfoFlag
InfoReasonUnknown :: InfoFlag
InfoAttr :: Attr -> InfoFlag
app :: Ident -> [Expr] -> Expr
class PP t
pp :: PP t => t -> Doc