Module Language.SMTLIB.Parser

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

Summary of exported operations:

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

Exported datatypes:


SMTParser

Type synonym: SMTParser a = Parser Token a


Exported operations:

parseCmdRsps :: String -> Either String [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