Language.SMT2.Parser

• Module : Language.SMT2.Parser
• Description : SMT language parser
• Maintainer : [e-mail]
• Stability : experimental

Utils

commonly used combinators

parseString :: Parser a -> Text -> Either ParseError a

parseStringEof :: Parser a -> Text -> Either ParseError a

parseFileMsg :: Parser a -> Text -> Either Text a

parse from a file string, may have leading & trailing spaces and comments

parseCommentFreeFileMsg :: Parser a -> Text -> Either Text a

parse from a comment-free file string

stripSpaces :: GenParser st a -> GenParser st a

strip away the leading and trailing spaces

removeComment :: Text -> Text

remove comments

Lexicons (Sec. 3.1)

Parsers for lexicons.

For a numeral, a decimal, or a string literal, the parsed result is the same. For a hexadecimal or a binary, the result is stripped with marks (#x and #b).

numeral :: GenParser st Numeral

decimal :: GenParser st Decimal

hexadecimal :: GenParser st Hexadecimal

binary :: GenParser st Binary

stringLiteral :: GenParser st StringLiteral

reservedWord :: GenParser st ReservedWord

accept all reserved words, the exact content should be checked later in the parsing procedure

symbol :: GenParser st Symbol

enclosing a simple symbol in vertical bars does not produce a new symbol, e.g. abc and |abc| are the same symbol this is guaranteed by removing the bars

keyword :: GenParser st Keyword

S-expressions (Sec. 3.2)

slist :: GenParser st SList

specConstant :: GenParser st SpecConstant

a constant must be followed by a space to delimit the end

sexpr :: GenParser st SExpr

Identifiers (Sec 3.3)

index :: GenParser st Index

identifier :: GenParser st Identifier

Attributes (Sec. 3.4)

attributeValue :: GenParser st AttributeValue

attribute :: GenParser st Attribute

Sorts (Sec 3.5)

sort :: GenParser st Sort

Terms and Formulas (Sec 3.6)

qualIdentifier :: GenParser st QualIdentifier

varBinding :: GenParser st VarBinding

sortedVar :: GenParser st SortedVar

matchPattern :: GenParser st MatchPattern

matchCase :: GenParser st MatchCase

term :: GenParser st Term

Theory declarations (Sec 3.7)

sortSymbolDecl :: GenParser st SortSymbolDecl

metaSpecConstant :: GenParser st MetaSpecConstant

funSymbolDecl :: GenParser st FunSymbolDecl

parFunSymbolDecl :: GenParser st ParFunSymbolDecl

theoryAttribute :: GenParser st TheoryAttribute

theoryDecl :: GenParser st TheoryDecl

Logic Declarations (Sec 3.8)

logicAttribute :: GenParser st LogicAttribute

logic :: GenParser st Logic

Scripts (Sec 3.9)

sortDec :: GenParser st SortDec

selectorDec :: GenParser st SelectorDec

constructorDec :: GenParser st ConstructorDec

datatypeDec :: GenParser st DatatypeDec

functionDec :: GenParser st FunctionDec

functionDef :: GenParser st FunctionDef

propLiteral :: GenParser st PropLiteral

command :: GenParser st Command

script :: GenParser st Script

bValue :: GenParser st BValue

scriptOption :: GenParser st ScriptOption

infoFlag :: GenParser st InfoFlag

Responses (Sec 3.9.1)

values

resErrorBehaviour :: GenParser st ResErrorBehavior

resReasonUnknown :: GenParser st ResReasonUnknown

resModel :: GenParser st ResModel

resInfo :: GenParser st ResInfo

valuationPair :: GenParser st ValuationPair

tValuationPair :: GenParser st TValuationPair

resCheckSat :: GenParser st ResCheckSat

instances

checkSatRes :: GenParser st CheckSatRes

echoRes :: GenParser st EchoRes

getAssertionsRes :: GenParser st GetAssertionsRes

getAssignmentRes :: GenParser st GetAssignmentRes

getInfoRes :: GenParser st GetInfoRes

getModelRes :: GenParser st GetModelRes

getOptionRes :: GenParser st GetOptionRes

getProofRes :: GenParser st GetProofRes

getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes

getUnsatCoreRes :: GenParser st GetUnsatCoreRes

getValueRes :: GenParser st GetValueRes

Orphan instances

SpecificSuccessRes ResCheckSat

Methods

specificSuccessRes :: GenParser st ResCheckSat

SpecificSuccessRes ResModel

Methods

specificSuccessRes :: GenParser st ResModel

SpecificSuccessRes AttributeValue

Methods

specificSuccessRes :: GenParser st AttributeValue

SpecificSuccessRes SExpr

Methods

specificSuccessRes :: GenParser st SExpr

SpecificSuccessRes StringLiteral

Methods

specificSuccessRes :: GenParser st StringLiteral

SpecificSuccessRes [TValuationPair]

Methods

specificSuccessRes :: GenParser st [TValuationPair]

SpecificSuccessRes [Term]

Methods

specificSuccessRes :: GenParser st [Term]

SpecificSuccessRes [Symbol]

Methods

specificSuccessRes :: GenParser st [Symbol]

SpecificSuccessRes (NonEmpty ValuationPair)

Methods

specificSuccessRes :: GenParser st (NonEmpty ValuationPair)

SpecificSuccessRes (NonEmpty ResInfo)

Methods

specificSuccessRes :: GenParser st (NonEmpty ResInfo)