This module provides parser functions for the SMT-LIB language. Currently there are only parsers for a subset of the language, namely command responses.
Author: Jan Tikovsky
Version: October 2017
parseCmdRsps
:: String -> Either String [CmdResponse]
|
parseResponse
:: Parser Token CmdResponse
|
parseGetAssertionsRsp
:: Parser Token CmdResponse
parser for get-assertions-response |
parseGetAssignmentRsp
:: Parser Token CmdResponse
parser for get-assignment-response |
parseTValPair
:: Parser Token (String,Bool)
parser for a t-valuation pair |
parseGetInfoRsp
:: Parser Token CmdResponse
parser for get-info-response |
parseInfoRsp
:: Parser Token InfoRsp
parser for an info response |
parseErrorBehavior
:: Parser Token ErrorBehavior
parser for error behavior |
parseReasonUnknown
:: Parser Token ReasonUnknown
parser for reason unknown |
parseGetModelRsp
:: Parser Token CmdResponse
parser for a get-model-response |
parseModelRsp
:: Parser Token ModelRsp
parser for a model response |
parseFunDef
:: Parser Token FunDef
parser for a function definition |
parseFunDec
:: Parser Token FunDec
parser for a function declaration |
parseGetValueRsp
:: Parser Token CmdResponse
parser for a get-value-response |
parseErrorRsp
:: Parser Token CmdResponse
parser for an error response |
parseBool
:: Parser Token Bool
parser for a boolean value |
parseNum
:: Parser Token Int
parser for a numeral |
parseStr
:: Parser Token String
parser for a string |
parseSym
:: Parser Token String
parser for a symbol |
parseValPair
:: Parser Token (Term,Term)
parser for a valuation pair |
parseTerm
:: Parser Token Term
parser for terms |
parseParenTerm
:: Parser Token Term
parser for parenthesized terms |
parseVarBind
:: Parser Token (String,Term)
parser for let bindings |
parseSortedVar
:: Parser Token SortedVar
parser for sorted variables |
parseAttribute
:: Parser Token Attribute
parser for attributes |
parseAttrValue
:: Parser Token AttrValue
parser for an attribute value |
parseSExpr
:: Parser Token SExpr
parser for SExpr
|
parseQIdent
:: Parser Token QIdent
parser for qualified identifiers |
parseSort
:: Parser Token Sort
parser for sorts |
Type synonym: SMTParser a = Parser Token a
|
parser for get-assertions-response |
parser for get-assignment-response |
parser for a t-valuation pair |
parser for get-info-response |
parser for an info response |
parser for error behavior |
parser for reason unknown |
parser for a get-model-response |
parser for a model response |
parser for a function definition |
parser for a function declaration |
parser for a get-value-response |
parser for an error response |
parser for a valuation pair |
parser for parenthesized terms |
parser for let bindings |
parser for sorted variables |
parser for attributes |
parser for an attribute value |
parser for |
parser for qualified identifiers |