-- Hoogle documentation, generated by Haddock -- See Hoogle, http://www.haskell.org/hoogle/ -- | Library for parsing SMTLIB2 -- @package SmtLib @version 0.1.0.0 -- | This module contains The syntax to create commands and responses. module Smtlib.Syntax.Syntax type Source = [Command] data Command SetLogic :: String -> Command SetOption :: Option -> Command SetInfo :: Attribute -> Command DeclareSort :: String -> Int -> Command DefineSort :: String -> [String] -> Sort -> Command DeclareFun :: String -> [Sort] -> Sort -> Command DefineFun :: String -> [SortedVar] -> Sort -> Term -> Command Push :: Int -> Command Pop :: Int -> Command Assert :: Term -> Command CheckSat :: Command GetAssertions :: Command GetProof :: Command GetUnsatCore :: Command GetValue :: [Term] -> Command GetAssignment :: Command GetOption :: String -> Command GetInfo :: InfoFlags -> Command Exit :: Command data Option PrintSucess :: Bool -> Option ExpandDefinitions :: Bool -> Option InteractiveMode :: Bool -> Option ProduceProofs :: Bool -> Option ProduceUnsatCores :: Bool -> Option ProduceModels :: Bool -> Option ProduceAssignments :: Bool -> Option RegularOutputChannel :: String -> Option DiagnosticOutputChannel :: String -> Option RandomSeed :: Int -> Option Verbosity :: Int -> Option OptionAttr :: Attribute -> Option data InfoFlags ErrorBehavior :: InfoFlags Name :: InfoFlags Authors :: InfoFlags Version :: InfoFlags Status :: InfoFlags ReasonUnknown :: InfoFlags AllStatistics :: InfoFlags InfoFlags :: String -> InfoFlags 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 VarBinding VB :: String -> Term -> VarBinding data SortedVar SV :: String -> Sort -> SortedVar data QualIdentifier QIdentifier :: Identifier -> QualIdentifier QIdentifierAs :: Identifier -> Sort -> QualIdentifier data AttrValue AttrValueConstant :: SpecConstant -> AttrValue AttrValueSymbol :: String -> AttrValue AttrValueSexpr :: [Sexpr] -> AttrValue data Attribute Attribute :: String -> Attribute AttributeVal :: String -> AttrValue -> Attribute data Identifier ISymbol :: String -> Identifier I_Symbol :: String -> [Int] -> Identifier data Sort SortId :: Identifier -> Sort SortIdentifiers :: Identifier -> [Sort] -> Sort 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 CmdResponse CmdGenResponse :: GenResponse -> CmdResponse CmdGetInfoResponse :: GetInfoResponse -> CmdResponse CmdCheckSatResponse :: CheckSatResponse -> CmdResponse CmdGetAssertionsResponse :: GetAssertionsResponse -> CmdResponse CmdGetAssignmentResponse :: GetAssignmentResponse -> CmdResponse CmdGetProofResponse :: GetProofResponse -> CmdResponse CmdGetUnsatCoreResponse :: GetUnsatCoreResponse -> CmdResponse CmdGetValueResponse :: GetValueResponse -> CmdResponse CmdGetOptionResponse :: GetOptionResponse -> CmdResponse 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 instance Show InfoFlags instance Eq InfoFlags instance Show Identifier instance Eq Identifier instance Show Sort instance Eq Sort instance Show QualIdentifier instance Eq QualIdentifier instance Show SortedVar instance Eq SortedVar instance Show SpecConstant instance Eq SpecConstant instance Show Sexpr instance Eq Sexpr instance Show AttrValue instance Eq AttrValue instance Show Attribute instance Eq Attribute instance Show Term instance Eq Term instance Show VarBinding instance Eq VarBinding instance Show Option instance Eq Option instance Show Command instance Eq Command instance Show GenResponse instance Eq GenResponse instance Show ErrorBehavior instance Eq ErrorBehavior instance Show ReasonUnknown instance Eq ReasonUnknown instance Show CheckSatResponse instance Eq CheckSatResponse instance Show InfoResponse instance Eq InfoResponse instance Show ValuationPair instance Eq ValuationPair instance Show TValuationPair instance Eq TValuationPair instance Show CmdResponse instance Eq CmdResponse -- | Functions to print the syntax as a SMTLib. module Smtlib.Syntax.ShowSL joinA :: ShowSL a => [a] -> String joinNs :: [Int] -> String class ShowSL a showSL :: ShowSL a => a -> String instance ShowSL TValuationPair instance ShowSL ValuationPair instance ShowSL InfoResponse instance ShowSL CheckSatResponse instance ShowSL ReasonUnknown instance ShowSL ErrorBehavior instance ShowSL GenResponse instance ShowSL CmdResponse instance ShowSL Sexpr instance ShowSL SpecConstant instance ShowSL Sort instance ShowSL Identifier instance ShowSL Attribute instance ShowSL AttrValue instance ShowSL QualIdentifier instance ShowSL SortedVar instance ShowSL VarBinding instance ShowSL Term instance ShowSL InfoFlags instance ShowSL Option instance ShowSL Command -- | This module contains some auxiliar parsers, used to parse commands or -- responses. module Smtlib.Parsers.CommonParsers (<:>) :: Applicative f => f a -> f [a] -> f [a] (<++>) :: Applicative f => f [a] -> f [a] -> f [a] parseBool :: ParsecT String u Identity Bool numeral :: ParsecT String u Identity String num :: 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 strChar :: ParsecT String u Identity Char 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 aspO :: ParsecT String u Identity Char aspC :: ParsecT String u Identity Char aspUS :: ParsecT String u Identity Char true :: ParsecT String u Identity String false :: ParsecT String u Identity String emptySpace :: ParsecT String u Identity String reservedWords :: ParsecT String u Identity String 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 parseSortedVar :: ParsecT String u Identity SortedVar parseQualIdentifier :: ParsecT String u Identity QualIdentifier parseQID :: ParsecT String u Identity QualIdentifier parseQIAs :: ParsecT String u Identity QualIdentifier parseVarBinding :: ParsecT String u Identity VarBinding 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 parseKeyAttribute :: ParsecT String u Identity Attribute parseKeyAttAttribute :: ParsecT String u Identity Attribute parseSort :: ParsecT String u Identity Sort parseIdentifierS :: ParsecT String u Identity Sort parseIdentifierSort :: ParsecT String u Identity Sort parseIdentifier :: ParsecT String u Identity Identifier parseOnlySymbol :: ParsecT String u Identity Identifier parseNSymbol :: ParsecT String u Identity Identifier parseSexprConstant :: ParsecT String u Identity Sexpr parseSexprSymbol :: ParsecT String u Identity Sexpr parseSexprKeyword :: ParsecT String u Identity Sexpr parseAtomSexpr :: ParsecT String u Identity Sexpr parseListSexpr :: ParsecT String u Identity Sexpr parseSexpr :: ParsecT String u Identity Sexpr parseSpecConstant :: ParsecT String u Identity SpecConstant 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 -- | This module contains all the required individual parsers for each -- reasponse to a Smtlib command, plus one parser to parse every result, -- parseCmdResult. module Smtlib.Parsers.ResponseParsers parseCmdResult :: ParsecT String u Identity CmdResponse parseCmdGenResponse :: ParsecT String u Identity CmdResponse parseGenResponse :: ParsecT String u Identity GenResponse parseSuccess :: ParsecT String u Identity GenResponse parseUnsupported :: ParsecT String u Identity GenResponse parseGenError :: ParsecT String u Identity GenResponse 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 parseRReasonUnknown :: ParsecT String u Identity ReasonUnknown parseResponseAttribute :: ParsecT String u Identity InfoResponse parseCmdCheckSatResponse :: ParsecT String u Identity CmdResponse parseCheckSatResponse :: ParsecT String u Identity CheckSatResponse parseCmdGetAssertions :: ParsecT String u Identity CmdResponse parseGetAssertionsResponse :: ParsecT String u Identity [Term] parseCmdGetProof :: ParsecT String u Identity CmdResponse parseGetProofResponse :: ParsecT String u Identity Sexpr parseCmdGetUnsatCore :: ParsecT String u Identity CmdResponse parseGetUnsatCoreResp :: ParsecT String u Identity [String] parseCmdGetValueResponse :: ParsecT String u Identity CmdResponse parseGetValueResponse :: ParsecT String u Identity [ValuationPair] parseValuationPair :: ParsecT String u Identity ValuationPair parseCmdGetAssignment :: ParsecT String u Identity CmdResponse parseGetAssignmentResp :: ParsecT String u Identity [TValuationPair] parseTValuationPair :: ParsecT String u Identity TValuationPair parseCmdGetOptionResponse :: ParsecT String u Identity CmdResponse parseGetOptionResponse :: ParsecT String u Identity AttrValue -- | This module contains all the required individual parsers for each -- Smtlib command, plus one parser to parse an entire SMTLib2 file, -- parseSource. module Smtlib.Parsers.CommandsParsers parseSource :: ParsecT String u Identity Source parseCommand :: ParsecT String u Identity Command parseSetLogic :: ParsecT String u Identity Command parseSetOption :: ParsecT String u Identity Command parseSetInfo :: ParsecT String u Identity Command parseDeclareSort :: ParsecT String u Identity Command parseDefineSort :: ParsecT String u Identity Command parseDeclareFun :: ParsecT String u Identity Command parseDefineFun :: ParsecT String u Identity Command parsePush :: ParsecT String u Identity Command parsePop :: ParsecT String u Identity Command parseAssert :: ParsecT String u Identity Command parseCheckSat :: ParsecT String u Identity Command parseGetAssertions :: ParsecT String u Identity Command parseGetProof :: ParsecT String u Identity Command parseGetUnsatCore :: ParsecT String u Identity Command parseGetValue :: ParsecT String u Identity Command parseGetAssignment :: ParsecT String u Identity Command parseGetOption :: ParsecT String u Identity Command parseGetInfo :: ParsecT String u Identity Command parseExit :: ParsecT String u Identity Command parseOption :: ParsecT String u Identity Option parsePrintSuccess :: ParsecT String u Identity Option parseExpandDefinitions :: ParsecT String u Identity Option parseInteractiveMode :: ParsecT String u Identity Option parseProduceProofs :: ParsecT String u Identity Option parseProduceUnsatCores :: ParsecT String u Identity Option parseProduceModels :: ParsecT String u Identity Option parseProduceAssignments :: ParsecT String u Identity Option parseRegularOutputChannel :: ParsecT String u Identity Option parseDiagnosticOutputChannel :: ParsecT String u Identity Option parseRandomSeed :: ParsecT String u Identity Option parseVerbosity :: ParsecT String u Identity Option parseOptionAttribute :: ParsecT String u Identity Option parseInfoFlags :: ParsecT String u Identity InfoFlags parseErrorBehaviour :: ParsecT String u Identity InfoFlags parseName :: ParsecT String u Identity InfoFlags parseAuthors :: ParsecT String u Identity InfoFlags parseVersion :: ParsecT String u Identity InfoFlags parseStatus :: ParsecT String u Identity InfoFlags parseReasonUnknown :: ParsecT String u Identity InfoFlags parseAllStatistics :: ParsecT String u Identity InfoFlags parseInfoKeyword :: ParsecT String u Identity InfoFlags