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

Language.SMT2.Parser

Description

  • Module : Language.SMT2.Parser
  • Description : SMT language parser
  • Maintainer : ubikium@gmail.com
  • 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 #

hexadecimal :: GenParser st Hexadecimal Source #

binary :: GenParser st Binary Source #

stringLiteral :: GenParser st StringLiteral 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)

attributeValue :: GenParser st AttributeValue Source #

attribute :: GenParser st Attribute Source #

Sorts (Sec 3.5)

sort :: GenParser st Sort Source #

Terms and Formulas (Sec 3.6)

qualIdentifier :: GenParser st QualIdentifier Source #

varBinding :: GenParser st VarBinding Source #

sortedVar :: GenParser st SortedVar Source #

matchPattern :: GenParser st MatchPattern Source #

matchCase :: GenParser st MatchCase Source #

term :: GenParser st Term Source #

Theory declarations (Sec 3.7)

sortSymbolDecl :: GenParser st SortSymbolDecl Source #

metaSpecConstant :: GenParser st MetaSpecConstant Source #

funSymbolDecl :: GenParser st FunSymbolDecl Source #

parFunSymbolDecl :: GenParser st ParFunSymbolDecl Source #

theoryAttribute :: GenParser st TheoryAttribute Source #

theoryDecl :: GenParser st TheoryDecl Source #

Logic Declarations (Sec 3.8)

logicAttribute :: GenParser st LogicAttribute Source #

logic :: GenParser st Logic Source #

Scripts (Sec 3.9)

sortDec :: GenParser st SortDec Source #

selectorDec :: GenParser st SelectorDec Source #

constructorDec :: GenParser st ConstructorDec Source #

datatypeDec :: GenParser st DatatypeDec Source #

functionDec :: GenParser st FunctionDec Source #

functionDef :: GenParser st FunctionDef Source #

propLiteral :: GenParser st PropLiteral Source #

command :: GenParser st Command Source #

script :: GenParser st Script Source #

bValue :: GenParser st BValue Source #

scriptOption :: GenParser st ScriptOption Source #

infoFlag :: GenParser st InfoFlag Source #

Responses (Sec 3.9.1)

values

resErrorBehaviour :: GenParser st ResErrorBehavior Source #

resReasonUnknown :: GenParser st ResReasonUnknown Source #

resModel :: GenParser st ResModel Source #

resInfo :: GenParser st ResInfo Source #

valuationPair :: GenParser st ValuationPair Source #

tValuationPair :: GenParser st TValuationPair Source #

resCheckSat :: GenParser st ResCheckSat Source #

instances

checkSatRes :: GenParser st CheckSatRes Source #

echoRes :: GenParser st EchoRes Source #

getAssertionsRes :: GenParser st GetAssertionsRes Source #

getAssignmentRes :: GenParser st GetAssignmentRes Source #

getInfoRes :: GenParser st GetInfoRes Source #

getModelRes :: GenParser st GetModelRes Source #

getOptionRes :: GenParser st GetOptionRes Source #

getProofRes :: GenParser st GetProofRes Source #

getUnsatAssumpRes :: GenParser st GetUnsatAssumpRes Source #

getUnsatCoreRes :: GenParser st GetUnsatCoreRes Source #

getValueRes :: GenParser st GetValueRes Source #

Orphan instances