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


-- | Haskell library for easy interaction with SMT-LIB 2 compliant solvers.
--   
--   Hsmtl provides functions to interact with several smt solvers using
--   SMT-LIB 2. The current suported solvers are Alt-Ergo, Cvc4, MathSat,
--   Yices, Z3. Additional solvers can be used if they are SMT-LIB 2
--   compliant. More information and tutorials can be found in
--   <a>https://github.com/MfesGA/Hsmtlib</a>
@package Hsmtlib
@version 0.2.0.6

module Hsmtlib.Solvers.Cmd.Parser.Syntax
data SpecConstant
SpecConstantNumeral :: Integer -> SpecConstant
SpecConstantDecimal :: String -> SpecConstant
SpecConstantHexadecimal :: String -> SpecConstant
SpecConstantBinary :: String -> SpecConstant
SpecConstantString :: String -> SpecConstant
data Sexpr
SexprSpecConstant :: SpecConstant -> Sexpr
SexprSymbol :: String -> Sexpr
SexprKeyword :: String -> Sexpr
SexprSxp :: [Sexpr] -> Sexpr
data Identifier
ISymbol :: String -> Identifier
I_Symbol :: String -> [String] -> Identifier
data Sort
SortId :: Identifier -> Sort
SortIdentifiers :: Identifier -> [Sort] -> Sort
data AttrValue
AttrValueConstant :: SpecConstant -> AttrValue
AttrValueSymbol :: String -> AttrValue
AttrValueSexpr :: [Sexpr] -> AttrValue
data Attribute
Attribute :: String -> Attribute
AttributeVal :: String -> AttrValue -> Attribute
data QualIdentifier
QIdentifier :: Identifier -> QualIdentifier
QIdentifierAs :: Identifier -> Sort -> QualIdentifier
data VarBinding
VB :: String -> Term -> VarBinding
data SortedVar
SV :: String -> Sort -> SortedVar
data Term
TermSpecConstant :: SpecConstant -> Term
TermQualIdentifier :: QualIdentifier -> Term
TermQualIdentifierT :: QualIdentifier -> [Term] -> Term
TermLet :: [VarBinding] -> Term -> Term
TermForall :: [SortedVar] -> Term -> Term
TermExists :: [SortedVar] -> Term -> Term
TermAnnot :: Term -> [Attribute] -> Term
data GenResponse
Unsupported :: GenResponse
Success :: GenResponse
Error :: String -> GenResponse
data ErrorBehavior
ImmediateExit :: ErrorBehavior
ContinuedExecution :: ErrorBehavior
data ReasonUnknown
Memout :: ReasonUnknown
Incomplete :: ReasonUnknown
data CheckSatResponse
Sat :: CheckSatResponse
Unsat :: CheckSatResponse
Unknown :: CheckSatResponse
type GetInfoResponse = [InfoResponse]
data InfoResponse
ResponseErrorBehavior :: ErrorBehavior -> InfoResponse
ResponseName :: String -> InfoResponse
ResponseAuthors :: String -> InfoResponse
ResponseVersion :: String -> InfoResponse
ResponseReasonUnknown :: ReasonUnknown -> InfoResponse
ResponseAttribute :: Attribute -> InfoResponse
type GetAssertionsResponse = [Term]
type GetProofResponse = Sexpr
type GetUnsatCoreResponse = [String]
data ValuationPair
ValuationPair :: Term -> Term -> ValuationPair
type GetValueResponse = [ValuationPair]
data TValuationPair
TValuationPair :: String -> Bool -> TValuationPair
type GetAssignmentResponse = [TValuationPair]
type GetOptionResponse = AttrValue
data CmdResponse
CmdGenResponse :: GenResponse -> CmdResponse
CmdGetInfoResponse :: GetInfoResponse -> CmdResponse
CmdCheckSatResponse :: CheckSatResponse -> CmdResponse
CmdGetAssertionResponse :: GetAssignmentResponse -> CmdResponse
CmdGetProofResponse :: GetProofResponse -> CmdResponse
CmdGetUnsatCoreResoponse :: GetUnsatCoreResponse -> CmdResponse
CmdGetValueResponse :: GetValueResponse -> CmdResponse
CmdGetAssigmnentResponse :: TValuationPair -> CmdResponse
CmdGetOptionResponse :: GetOptionResponse -> CmdResponse
instance Show SpecConstant
instance Show Sexpr
instance Show Identifier
instance Show Sort
instance Show AttrValue
instance Show Attribute
instance Show QualIdentifier
instance Show SortedVar
instance Show Term
instance Show VarBinding
instance Show GenResponse
instance Show ErrorBehavior
instance Show ReasonUnknown
instance Show CheckSatResponse
instance Show InfoResponse
instance Show ValuationPair
instance Show TValuationPair
instance Show CmdResponse

module Hsmtlib.Solvers.Cmd.Parser.Parsers
(<:>) :: Applicative f => f a -> f [a] -> f [a]
(<++>) :: Applicative f => f [a] -> f [a] -> f [a]
aspO :: ParsecT String u Identity Char
aspC :: ParsecT String u Identity Char
aspUS :: ParsecT String u Identity Char
numeral :: ParsecT String u Identity String
decimal :: ParsecT String u Identity String
zeros :: ParsecT String u Identity String
dot :: ParsecT String u Identity String
hexadecimal :: ParsecT String u Identity String
binary :: ParsecT String u Identity String
bin :: ParsecT String u Identity Char
str :: ParsecT String u Identity String
symbol :: ParsecT String u Identity String
quotedSymbol :: ParsecT String u Identity String
simpleSymbol :: ParsecT String u Identity String
spcSymb :: ParsecT String u Identity Char
keyword :: ParsecT String u Identity String
reservedWords :: ParsecT String u Identity String
bValue :: ParsecT String u Identity Bool
parseNumeral :: ParsecT String u Identity SpecConstant
parseDecimal :: ParsecT String u Identity SpecConstant
parseHexadecimal :: ParsecT String u Identity SpecConstant
parseBinary :: ParsecT String u Identity SpecConstant
parseString :: ParsecT String u Identity SpecConstant
parseSpecConstant :: ParsecT String u Identity SpecConstant
parseSexprConstant :: ParsecT String u Identity Sexpr
parseSexprSymbol :: ParsecT String u Identity Sexpr
parseSexprKeyword :: ParsecT String u Identity Sexpr
parseSexprS :: ParsecT String u Identity Sexpr
parseSexpr' :: ParsecT String u Identity Sexpr
parseSexpr :: ParsecT String u Identity [Sexpr]
parseIdentifier :: ParsecT String u Identity Identifier
parseOnlySymbol :: ParsecT String u Identity Identifier
parseNSymbol :: ParsecT String u Identity Identifier
parseSort :: ParsecT String u Identity [Sort]
parseSort' :: ParsecT String u Identity Sort
parseIdentifierS :: ParsecT String u Identity Sort
parseIdentifierSort :: ParsecT String u Identity Sort
parseAttributeValue :: ParsecT String u Identity AttrValue
parseAVSC :: ParsecT String u Identity AttrValue
parseAVS :: ParsecT String u Identity AttrValue
parseAVSexpr :: ParsecT String u Identity AttrValue
parseAttribute :: ParsecT String u Identity Attribute
parseQualIdentifier :: ParsecT String u Identity QualIdentifier
parseQID :: ParsecT String u Identity QualIdentifier
parseQIAs :: ParsecT String u Identity QualIdentifier
parseVarBinding :: ParsecT String u Identity VarBinding
parseSortedVar :: ParsecT String u Identity SortedVar
parseTerm :: ParsecT String u Identity Term
parseTSPC :: ParsecT String u Identity Term
parseTQID :: ParsecT String u Identity Term
parseTQIT :: ParsecT String u Identity Term
parseTermLet :: ParsecT String u Identity Term
parseTermFA :: ParsecT String u Identity Term
parseTermEX :: ParsecT String u Identity Term
parseTermAnnot :: ParsecT String u Identity Term
parseCmdGenResponse :: ParsecT String u Identity CmdResponse
parseCmdGenRepError :: ParsecT String u Identity CmdResponse
parseCmdGetInfoResponse :: ParsecT String u Identity CmdResponse
parseGetInfoResponse :: ParsecT String u Identity [InfoResponse]
parseInfoResponse :: ParsecT String u Identity InfoResponse
parseResponseName :: ParsecT String u Identity InfoResponse
parseResponseErrorBehavior :: ParsecT String u Identity InfoResponse
parseErrorBehavior :: ParsecT String u Identity ErrorBehavior
parseResponseAuthors :: ParsecT String u Identity InfoResponse
parseResponseVersion :: ParsecT String u Identity InfoResponse
parseResponseReasonUnknown :: ParsecT String u Identity InfoResponse
parseResponseAttribute :: ParsecT String u Identity InfoResponse
parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse
parseGetAssertionResponse :: ParsecT String u Identity [Term]
parseGetProofResponse :: ParsecT String u Identity Sexpr
parseGetUnsatCoreResp :: ParsecT String u Identity [String]
parseGetValueResponse :: ParsecT String u Identity [ValuationPair]
parseValuationPair :: ParsecT String u Identity ValuationPair
parseTValuationPair :: ParsecT String u Identity TValuationPair
parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair]
parseGetOptionResponse :: ParsecT String u Identity AttrValue
parseReasonUnknown :: ParsecT String u Identity ReasonUnknown
main :: IO a

module Hsmtlib.Solvers.Cmd.Parser.Visualizers
spaces' :: Int -> Int -> String
spaces :: Int -> String
branch' :: Int -> String
branchAr' :: Int -> String
fbranch :: Int -> String -> String -> String
branch :: String -> (Int -> a -> String) -> Int -> a -> String
nLines :: String -> Int
mLines :: String -> Int -> String
showValuationPair :: Int -> ValuationPair -> String
showSpecConstant :: SpecConstant -> String
aTup :: String -> Int -> [a] -> (Int -> a -> String) -> String
dTup :: String -> Int -> String -> a -> (Int -> a -> String) -> String
tup :: String -> Int -> a -> b -> (Int -> a -> String) -> (Int -> b -> String) -> String
tupArray :: String -> Int -> a -> [b] -> (Int -> a -> String) -> (Int -> b -> String) -> String
showQualIdentifier :: Int -> QualIdentifier -> String
showSort :: Int -> Sort -> String
showIdentifier :: Int -> Identifier -> String
showTerm :: Int -> Term -> String
showVarBinding :: Int -> VarBinding -> String
showSortedVar :: Int -> SortedVar -> String
showAttribute :: Int -> Attribute -> String
showAttrValue :: Int -> AttrValue -> String
showSexpr :: Int -> Sexpr -> String


-- | The following module contains method that facilitate the comunication
--   with the SMTSolvers.
module Hsmtlib.Solvers.Cmd.ProcCom.Process

-- | Creates a Process ready to be executed.
beginProcess :: CmdPath -> Args -> IO Process

-- | Sends the desired input to the process std_in and then reads from std
--   out. Working smt with this method: - z3 - mathSat - cvc4
send :: Process -> String -> IO String

-- | Sends the signal to terminate to the running process.
endProcess :: Process -> IO ExitCode

-- | It's the same function as readProcess.
--   <a>http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html</a>
sendContext :: CmdPath -> Args -> Context -> IO String

-- | Calls readProcess and pass as arguments the arguments given plus the
--   name of the file with the context. An empty String is passed to the
--   std_in.
--   
--   It's the same function as readProcess. readProcess:
--   <a>http://hackage.haskell.org/package/process-1.1.0.1/docs/System-Process.html</a>
sendScript :: CmdPath -> Args -> FilePath -> IO String

-- | Type returned by CreateProcess
type Process = (Maybe Handle, Maybe Handle, Maybe Handle, ProcessHandle)

-- | Path to the process
type CmdPath = String

-- | Argumants passed to process
type Args = [String]

module Hsmtlib.Solvers.Cmd.BatchCmd
executeBatch :: CmdPath -> Args -> String -> [Command] -> IO String


-- | This module has most types,data and functions that a user might need
--   to utilize the library.
module Hsmtlib.Solver

-- | Logics that can be passed to the start of the solver
data Logic
AUFLIA :: Logic
AUFLIRA :: Logic
AUFNIRA :: Logic
LRA :: Logic
QF_ABV :: Logic
QF_AUFBV :: Logic
QF_AUFLIA :: Logic
QF_AX :: Logic
QF_BV :: Logic
QF_IDL :: Logic
QF_LIA :: Logic
QF_LRA :: Logic
QF_NIA :: Logic
QF_NRA :: Logic
QF_RDL :: Logic
QF_UF :: Logic
QF_UFBV :: Logic
QF_UFIDL :: Logic
QF_UFLIA :: Logic
QF_UFLRA :: Logic
QF_UFNRA :: Logic
UFLRA :: Logic
UFNIA :: Logic

-- | Solvers that are currently supported.
data Solvers
Z3 :: Solvers
Cvc4 :: Solvers
Yices :: Solvers
Mathsat :: Solvers
Altergo :: Solvers
Boolector :: Solvers

-- | Response from most commands that do not demand a feedback from the
--   solver, e.g: setLogic,push,pop...
data GenResult

-- | The command was successfully sent to the solver.
Success :: GenResult

-- | The solver does not support the command.
Unsupported :: GenResult

-- | Some error occurred in the solver. | Some error occurred parsing the
--   response from the solver.
Error :: String -> GenResult
GUError :: String -> GenResult

-- | Response from the command checkSat.
data SatResult

-- | The solver has found a model.
Sat :: SatResult

-- | The solver has established there is no model.
Unsat :: SatResult

-- | The search for a model was inconclusive. Some error occurred parsing
--   the response from the solver.
Unknown :: SatResult
SUError :: String -> SatResult

-- | Response from the command getValue
data GValResult

-- | Name of the variable or function and result.
Res :: String -> Value -> GValResult

-- | The result of arrays
VArrays :: Arrays -> GValResult

-- | Multiple results from multiple requestes.
Results :: [GValResult] -> GValResult

-- | Some error occurred parsing the response from the solver.
GVUError :: String -> GValResult

-- | When the value of an array or several values from diferent arrays are
--   requested with getValue then the value returned is a Map where the
--   value ís the name of the array, and the value is also a map. This
--   inner map has as value the position of the array and returned value.
--   Only integers are supported as values of arrays.
type Arrays = Map String (Map String Integer)

-- | The type returned by getValue on constants or functions.
data Value
VInt :: Integer -> Value
VRatio :: Rational -> Value
VBool :: Bool -> Value
VHex :: String -> Value

-- | Avaliable modes to use a solver.
data Mode
Online :: Mode
Script :: Mode
Batch :: Mode

-- | Alternative configuration of a solver which can be passed in the
--   function startSolver in <tt>Main</tt>
data SolverConfig
Config :: String -> [String] -> SolverConfig
path :: SolverConfig -> String
args :: SolverConfig -> [String]

-- | Solver data type that has all the functions.
data Solver
Solver :: (Name -> IO GenResult) -> (Option -> IO GenResult) -> (Attr -> IO GenResult) -> (Name -> Integer -> IO GenResult) -> (Name -> [Name] -> Type -> IO GenResult) -> (Name -> [Type] -> Type -> IO GenResult) -> (Name -> [Binder] -> Type -> Expr -> IO GenResult) -> (Integer -> IO GenResult) -> (Integer -> IO GenResult) -> (Expr -> IO GenResult) -> IO SatResult -> IO String -> ([Expr] -> IO GValResult) -> IO String -> IO String -> (InfoFlag -> IO String) -> (Name -> IO String) -> IO String -> Solver
setLogic :: Solver -> Name -> IO GenResult
setOption :: Solver -> Option -> IO GenResult
setInfo :: Solver -> Attr -> IO GenResult
declareType :: Solver -> Name -> Integer -> IO GenResult
defineType :: Solver -> Name -> [Name] -> Type -> IO GenResult
declareFun :: Solver -> Name -> [Type] -> Type -> IO GenResult
defineFun :: Solver -> Name -> [Binder] -> Type -> Expr -> IO GenResult
push :: Solver -> Integer -> IO GenResult
pop :: Solver -> Integer -> IO GenResult
assert :: Solver -> Expr -> IO GenResult
checkSat :: Solver -> IO SatResult
getAssertions :: Solver -> IO String
getValue :: Solver -> [Expr] -> IO GValResult
getProof :: Solver -> IO String
getUnsatCore :: Solver -> IO String
getInfo :: Solver -> InfoFlag -> IO String
getOption :: Solver -> Name -> IO String
exit :: Solver -> IO String
BSolver :: ([Command] -> IO String) -> Solver
executeBatch :: Solver -> [Command] -> IO String
instance Show Logic
instance Show GenResult
instance Eq GenResult
instance Show SatResult
instance Show Value
instance Show GValResult


-- | This Module provide auxiliar functions that simplify writing
--   expressions to send to the solver.
module Hsmtlib.HighLevel

-- | This function hides the application of a function on the SMT syntax
--   receives the name of the function and the args and gives the
--   corresponding SMT2Lib syntax.
functionArg :: Name -> [Expr] -> Expr

-- | This function hides the application of a constant function on the SMT
--   syntax receives the name of the function and gives the corresponding
--   SMT2Lib syntax, the function must be already declared using
--   declareFun.
constant :: String -> Expr

-- | This function hides the application of distinct on the SMT syntax
--   receives the solver and a list of the expressions which must be
--   distinct and gives the corresponding SMT2Lib syntax.
assertDistinct :: Solver -> [Expr] -> IO GenResult

-- | This function hides Integers on the SMT syntax receives a integer and
--   gives the corresponding SMT2Lib syntax.
literal :: Int -> Expr

-- | This function allows the user to given a list of expressions make a
--   assert of them giving the SMTLib2 syntax corespondant (auxiliary
--   function for maping).
mapAssert :: Solver -> [Expr] -> IO ()

-- | This function when giving a solver and a function that gives an Expr
--   and a list of the input type of that function, asserts the map of
--   expressions its particulary useful to say that some set variables are
--   all for example greater than zero.
maping :: Solver -> (a -> Expr) -> [a] -> IO ()

-- | This function hides the name creation on the SMT syntax receives a
--   string and gives the corresponding SMT2Lib syntax for declaring a
--   function.
declFun :: Solver -> String -> [Type] -> Type -> IO GenResult
defFun :: Solver -> String -> [Binder] -> Type -> Expr -> IO GenResult

-- | This function binds a name to a type, and returns a Binder.
bind :: String -> Type -> Binder

-- | This function hides Constants implemnted as functions without
--   arguments on the SMT syntax receives a String and a type and gives the
--   corresponding SMT2Lib syntax for declaring a constant function.
declConst :: Solver -> String -> Type -> IO GenResult

-- | This function hides Constants implemnted as functions without
--   arguments on the SMT syntax receives a String and a type and gives the
--   corresponding SMT2Lib syntax for declaring a constant function.
mapDeclConst :: Solver -> [String] -> Type -> IO ()

-- | This function hides the way to access an array (Hammered version) on
--   the SMT syntax receives a integer and gives the corresponding SMT2Lib
--   syntax.
getPos :: Show a => Solver -> String -> a -> IO GValResult

-- | This function hides the Name Type in the declare type comand
declType :: Solver -> String -> Integer -> IO GenResult

-- | This function simplifies the command to set the option to Produce
--   Models.
produceModels :: Solver -> IO GenResult

-- | This function simplifies the command to set the option to Interactive
--   Mode.
interactiveMode :: Solver -> IO GenResult

module Hsmtlib.Solvers.Cmd.Parser.CmdResult
genResponse :: String -> GenResult
checkSatResponse :: String -> SatResult
getValueResponse :: String -> GValResult
getVR' :: [GValResult] -> GValResult
getValResponse :: [ValuationPair] -> [GValResult]
valErrors' :: [ValuationPair] -> [Maybe GValResult] -> [GValResult]
joinArrays :: [Maybe GValResult] -> [GValResult]
joinArrays' :: GValResult -> [Maybe GValResult] -> [GValResult]
checkGVal :: GValResult -> Maybe GValResult -> GValResult
getValResponses :: [ValuationPair] -> [Maybe GValResult]
getGValResult :: ValuationPair -> Maybe GValResult

-- | Retrives the value of a BitVector. Works with: - Z3.
getBitVec :: ValuationPair -> Maybe GValResult
getBitVec' :: Maybe String -> Maybe String -> Maybe GValResult

-- | Retrives the value of a function. Works with: - Z3.
getFun :: ValuationPair -> Maybe GValResult
getFun' :: Maybe String -> Maybe Value -> Maybe GValResult

-- | Retrives the value of a variable. Works with: - Z3.
getVar :: ValuationPair -> Maybe GValResult
getVar' :: Maybe String -> Maybe Integer -> Maybe GValResult

-- | Retrives the value of an array. Works with: - Z3.
getArray :: ValuationPair -> Maybe GValResult
getArray' :: Maybe String -> Maybe Integer -> Maybe String -> Maybe Integer -> Maybe Arrays
isArray :: ValuationPair -> Maybe Bool

-- | Verifies if the string correspond to a certain notation that indicates
--   that is an Array. For example Z3 would have the keyword select
--   therefor it's an array. If it isn't an array then returns nothing
isArray' :: String -> Maybe Bool

-- | Retrives the name of the array. Works with: - Z3.
arrayName :: ValuationPair -> Maybe String

-- | Retrives the position of the array if it is an Integer. Works with: -
--   Z3.
arrayIntPos :: ValuationPair -> Maybe Integer

-- | Retrives the position of the array if it is a String. Works with: -
--   Z3.
arrayVarPos :: ValuationPair -> Maybe String

-- | Retrives the value of an array. Works with: - Z3.
arrayVal :: ValuationPair -> Maybe Integer

-- | Retrive the name of a variable. Works with: - Z3.
getVarName :: ValuationPair -> Maybe String

-- | Retrive the variable of a variable. Works with: - Z3.
getVarValue :: ValuationPair -> Maybe Integer

-- | Retrives the name of a function. Works with: - Z3
getFunName :: ValuationPair -> Maybe String

-- | Retrives the result of a function if it is a Integer. Works with: -
--   Z3.
getFunResult :: ValuationPair -> Maybe Value
getFunResultBool :: ValuationPair -> Maybe Value
getFunResultInt :: ValuationPair -> Maybe Value
(<#>) :: Functor m => (b -> c) -> (a -> m b) -> a -> m c
toBool :: String -> Maybe Bool
getFunResultInt' :: ValuationPair -> Maybe Integer
getFunResultBool' :: ValuationPair -> Maybe String

-- | Retrives the result of a bitvector. Works with: - Z3
getHexVal :: ValuationPair -> Maybe String

-- | Returns the first term of a valuation pair.
fstTerm :: ValuationPair -> Maybe Term

-- | Returns the second term of a valuation pair.
sndTerm :: ValuationPair -> Maybe Term

-- | Returns the list of terms from TermQualIdeintifierT
sndTermQualIdentierT :: Term -> Maybe [Term]
fstTermQualIdentierT :: Term -> Maybe QualIdentifier
termQualIdentifier :: Term -> Maybe QualIdentifier
getTermSpecConstant :: Term -> Maybe SpecConstant
qIdentifier :: QualIdentifier -> Maybe Identifier
symbol :: Identifier -> Maybe String
numeral :: SpecConstant -> Maybe Integer
hex :: SpecConstant -> Maybe String


-- | Module with the functions used in online Mode.
module Hsmtlib.Solvers.Cmd.OnlineCmd
onlineFun :: Process -> Command -> IO String
onlineGenResponse :: Process -> Command -> IO GenResult
onlineCheckSatResponse :: Process -> Command -> IO SatResult
onlineGetValueResponse :: Process -> Command -> IO GValResult
onlineSetLogic :: Process -> Name -> IO GenResult
onlineSetOption :: Process -> Option -> IO GenResult
onlineSetInfo :: Process -> Attr -> IO GenResult
onlineDeclareType :: Process -> Name -> Integer -> IO GenResult
onlineDefineType :: Process -> Name -> [Name] -> Type -> IO GenResult
onlineDeclareFun :: Process -> Name -> [Type] -> Type -> IO GenResult
onlineDefineFun :: Process -> Name -> [Binder] -> Type -> Expr -> IO GenResult
onlinePush :: Process -> Integer -> IO GenResult
onlinePop :: Process -> Integer -> IO GenResult
onlineAssert :: Process -> Expr -> IO GenResult
onlineCheckSat :: Process -> IO SatResult
onlineGetAssertions :: Process -> IO String
onlineGetValue :: Process -> [Expr] -> IO GValResult
onlineGetProof :: Process -> IO String
onlineGetUnsatCore :: Process -> IO String
onlineGetInfo :: Process -> InfoFlag -> IO String
onlineGetOption :: Process -> Name -> IO String
onlineExit :: Process -> IO String


-- | Module with the functions used in script Mode.
module Hsmtlib.Solvers.Cmd.ScriptCmd
data ScriptConf
ScriptConf :: Handle -> CmdPath -> Args -> FilePath -> ScriptConf
sHandle :: ScriptConf -> Handle
sCmdPath :: ScriptConf -> CmdPath
sArgs :: ScriptConf -> Args
sFilePath :: ScriptConf -> FilePath
writeToScript :: ScriptConf -> Command -> IO ()
scriptFun :: ScriptConf -> Command -> IO String
scriptFunExec :: ScriptConf -> Command -> IO String
scriptGenResponse :: ScriptConf -> Command -> IO GenResult
scriptCheckSatResponse :: ScriptConf -> Command -> IO SatResult
scriptGetValueResponse :: ScriptConf -> Command -> IO GValResult
scriptSetLogic :: ScriptConf -> Name -> IO GenResult
scriptSetOption :: ScriptConf -> Option -> IO GenResult
scriptSetInfo :: ScriptConf -> Attr -> IO GenResult
scriptDeclareType :: ScriptConf -> Name -> Integer -> IO GenResult
scriptDefineType :: ScriptConf -> Name -> [Name] -> Type -> IO GenResult
scriptDeclareFun :: ScriptConf -> Name -> [Type] -> Type -> IO GenResult
scriptDefineFun :: ScriptConf -> Name -> [Binder] -> Type -> Expr -> IO GenResult
scriptPush :: ScriptConf -> Integer -> IO GenResult
scriptPop :: ScriptConf -> Integer -> IO GenResult
scriptAssert :: ScriptConf -> Expr -> IO GenResult
scriptCheckSat :: ScriptConf -> IO SatResult
scriptGetAssertions :: ScriptConf -> IO String
scriptGetValue :: ScriptConf -> [Expr] -> IO GValResult
scriptGetProof :: ScriptConf -> IO String
scriptGetUnsatCore :: ScriptConf -> IO String
scriptGetInfo :: ScriptConf -> InfoFlag -> IO String
scriptGetOption :: ScriptConf -> Name -> IO String
scriptExit :: ScriptConf -> IO String


-- | Module wich has the standard configuration for all altergo Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.Altergo

-- | Function that initialyzes a altergo Solver. It Receives a Mode, an SMT
--   Logic, it can receive a diferent configuration for the solver and an
--   anternative path to create the script in Script Mode.
--   
--   In Online Mode if a FilePath is passed then it's ignored.
startAltErgo :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Module wich has the standard configuration for all boolector Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.Boolector

-- | Function that initialyzes a boolector Solver. It Receives a Mode, an
--   SMT Logic, it can receive a diferent configuration for the solver and
--   an anternative path to create the script in Script Mode.
--   
--   In Online Mode if a FilePath is passed then it's ignored.
startBoolector :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Module wich has the standard configuration for all Cvc4 Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.Cvc4

-- | Function that initialyzes a Cvc4 Solver. It Receives a Mode, an SMT
--   Logic, it can receive a diferent configuration for the solver and an
--   anternative path to create the script in Script Mode.
--   
--   In Context and Online Mode if a FilePath is passed then it's ignored.
startCvc4 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Module wich has the standard configuration for all mathSat Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.MathSAT

-- | Function that initialyzes a mathSat Solver. It Receives a Mode, an SMT
--   Logic, it can receive a diferent configuration for the solver and an
--   anternative path to create the script in Script Mode.
--   
--   In Online Mode if a FilePath is passed then it's ignored.
startMathSat :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Module wich has the standard configuration for all Yices Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.Yices

-- | Function that initialyzes a Yices Solver. It Receives a Mode, an SMT
--   Logic, it can receive a diferent configuration for the solver and an
--   anternative path to create the script in Script Mode.
--   
--   In Online Mode if a FilePath is passed then it's ignored.
startYices :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Module wich has the standard configuration for all Z3 Modes and
--   provides the initilizing function.
module Hsmtlib.Solvers.Z3

-- | Function that initialyzes a Z3 Solver. It Receives a Mode, an SMT
--   Logic, it can receive a diferent configuration for the solver and an
--   anternative path to create the script in Script Mode.
--   
--   In Online Mode if a FilePath is passed then it's ignored.
startZ3 :: Mode -> String -> Maybe SolverConfig -> Maybe FilePath -> IO Solver


-- | Main module which provides the function to initialize a Solver.
module Hsmtlib

-- | The function to initialialyze a solver. The solver can be initialized
--   with a desired configuration, or a diferent Path to keep the script in
--   Script Mode, if Nothing is passed then it will use the default
--   settings.
--   
--   There are two <a>Mode</a>s of operation for the solvers, Online and
--   Script.
--   
--   In online Mode a solver is created and kept running. Commands are sent
--   via pipe one by one and every time one is sent it also reads the
--   answer of the solver.
--   
--   In script <a>Mode</a> a file is created in a desired file path, if
--   Nothing is passed then its created in the current directory with the
--   name temp.smt2. If a file already exists then it's overwriten.
--   
--   The functions in this mode (Script) behave in the following manner: If
--   it's a funcion where something is declared, for example declareFun or
--   assert then it's only writen to the file. In functions where some
--   feedback is expected such as checkSat, this are writen to the file, a
--   solver is created and the file is given to solver, and it waits for
--   the result. The result is the result of the last function.
startSolver :: Solvers -> Mode -> Logic -> Maybe SolverConfig -> Maybe String -> IO Solver
