smt2-parser-0.1.0.0: A Haskell parser for SMT-LIB version 2.6
Safe HaskellSafe
LanguageHaskell2010

Language.SMT2.Parser

Description

  • Module : Language.SMT2.Parser
  • Description : SMT language parser
  • Maintainer : yokis1997@pku.edu.cn
  • Stability : experimental
Synopsis

Utils

commonly used combinators

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

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

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

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

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

parse from a comment-free file string

stripSpaces :: GenParser st a -> GenParser st a Source #

strip away the leading and trailing spaces

removeComment :: Text -> Text Source #

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 Source #

decimal :: GenParser st Decimal Source #

binary :: GenParser st Binary Source #

reservedWord :: GenParser st ReservedWord Source #

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

symbol :: GenParser st Symbol Source #

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 Source #

S-expressions (Sec. 3.2)

slist :: GenParser st SList Source #

specConstant :: GenParser st SpecConstant Source #

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

sexpr :: GenParser st SExpr Source #

Identifiers (Sec 3.3)

index :: GenParser st Index Source #

identifier :: GenParser st Identifier Source #

Attributes (Sec. 3.4)

attribute :: GenParser st Attribute Source #

Sorts (Sec 3.5)

sort :: GenParser st Sort Source #

Terms and Formulas (Sec 3.6)

varBinding :: GenParser st VarBinding Source #

sortedVar :: GenParser st SortedVar Source #

matchCase :: GenParser st MatchCase Source #

term :: GenParser st Term Source #

Theory declarations (Sec 3.7)

theoryDecl :: GenParser st TheoryDecl Source #

Logic Declarations (Sec 3.8)

logic :: GenParser st Logic Source #

Scripts (Sec 3.9)

sortDec :: GenParser st SortDec Source #

command :: GenParser st Command Source #

script :: GenParser st Script Source #

bValue :: GenParser st BValue Source #

infoFlag :: GenParser st InfoFlag Source #

Responses (Sec 3.9.1)

values

resModel :: GenParser st ResModel Source #

resInfo :: GenParser st ResInfo Source #

instances

echoRes :: GenParser st EchoRes Source #

getInfoRes :: GenParser st GetInfoRes Source #

Orphan instances

SpecificSuccessRes ResCheckSat Source # 
Instance details

Methods

specificSuccessRes :: GenParser st ResCheckSat Source #

SpecificSuccessRes ResModel Source # 
Instance details

Methods

specificSuccessRes :: GenParser st ResModel Source #

SpecificSuccessRes AttributeValue Source # 
Instance details

Methods

specificSuccessRes :: GenParser st AttributeValue Source #

SpecificSuccessRes SExpr Source # 
Instance details

Methods

specificSuccessRes :: GenParser st SExpr Source #

SpecificSuccessRes StringLiteral Source # 
Instance details

Methods

specificSuccessRes :: GenParser st StringLiteral Source #

SpecificSuccessRes [TValuationPair] Source # 
Instance details

Methods

specificSuccessRes :: GenParser st [TValuationPair] Source #

SpecificSuccessRes [Term] Source # 
Instance details

Methods

specificSuccessRes :: GenParser st [Term] Source #

SpecificSuccessRes [Symbol] Source # 
Instance details

Methods

specificSuccessRes :: GenParser st [Symbol] Source #

SpecificSuccessRes (NonEmpty ValuationPair) Source # 
Instance details

Methods

specificSuccessRes :: GenParser st (NonEmpty ValuationPair) Source #

SpecificSuccessRes (NonEmpty ResInfo) Source # 
Instance details

Methods

specificSuccessRes :: GenParser st (NonEmpty ResInfo) Source #