Language.SMT2.Syntax

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

Lexicons (Sec. 3.1)

type Numeral = Text

type Decimal = Text

type Hexadecimal = Text

type Binary = Text

type StringLiteral = Text

type ReservedWord = Text

type Symbol = Text

type Keyword = Text

S-expressions (Sec. 3.2)

data SpecConstant

Constructors

SCNumeral Numeral

SCDecimal Decimal

SCHexadecimal Hexadecimal

SCBinary Binary

SCString StringLiteral

Instances

Eq SpecConstant

Defined in Language.SMT2.Syntax

Methods

(==) :: SpecConstant -> SpecConstant -> Bool

(/=) :: SpecConstant -> SpecConstant -> Bool

Show SpecConstant

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SpecConstant -> ShowS

show :: SpecConstant -> String

showList :: [SpecConstant] -> ShowS

data SExpr

Constructors

SEConstant SpecConstant

SEReservedWord ReservedWord

SESymbol Symbol

SEKeyword Keyword

SEList SList

Instances

Eq SExpr

Defined in Language.SMT2.Syntax

Methods

(==) :: SExpr -> SExpr -> Bool

(/=) :: SExpr -> SExpr -> Bool

Show SExpr

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SExpr -> ShowS

show :: SExpr -> String

showList :: [SExpr] -> ShowS

SpecificSuccessRes SExpr

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st SExpr

type SList = [SExpr]

Identifiers (Sec 3.3)

data Index

Constructors

IxNumeral Numeral

IxSymbol Symbol

Instances

Eq Index

Defined in Language.SMT2.Syntax

Methods

(==) :: Index -> Index -> Bool

(/=) :: Index -> Index -> Bool

Show Index

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Index -> ShowS

show :: Index -> String

showList :: [Index] -> ShowS

data Identifier

Constructors

IdSymbol Symbol

IdIndexed Symbol (NonEmpty Index)

Instances

Eq Identifier

Defined in Language.SMT2.Syntax

Methods

(==) :: Identifier -> Identifier -> Bool

(/=) :: Identifier -> Identifier -> Bool

Show Identifier

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Identifier -> ShowS

show :: Identifier -> String

showList :: [Identifier] -> ShowS

Attributes (Sec. 3.4)

data AttributeValue

Constructors

AttrValSpecConstant SpecConstant

AttrValSymbol Symbol

AttrValSList SList

Instances

Eq AttributeValue

Defined in Language.SMT2.Syntax

Methods

(==) :: AttributeValue -> AttributeValue -> Bool

(/=) :: AttributeValue -> AttributeValue -> Bool

Show AttributeValue

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> AttributeValue -> ShowS

show :: AttributeValue -> String

showList :: [AttributeValue] -> ShowS

SpecificSuccessRes AttributeValue

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st AttributeValue

data Attribute

Constructors

AttrKey Keyword

AttrKeyValue Keyword AttributeValue

Instances

Eq Attribute

Defined in Language.SMT2.Syntax

Methods

(==) :: Attribute -> Attribute -> Bool

(/=) :: Attribute -> Attribute -> Bool

Show Attribute

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Attribute -> ShowS

show :: Attribute -> String

showList :: [Attribute] -> ShowS

Sorts (Sec 3.5)

data Sort

Constructors

SortSymbol Identifier

SortParameter Identifier (NonEmpty Sort)

Instances

Eq Sort

Defined in Language.SMT2.Syntax

Methods

(==) :: Sort -> Sort -> Bool

(/=) :: Sort -> Sort -> Bool

Show Sort

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Sort -> ShowS

show :: Sort -> String

showList :: [Sort] -> ShowS

Terms and Formulas (Sec 3.6)

data QualIdentifier

Constructors

Unqualified Identifier

Qualified Identifier Sort

Instances

Eq QualIdentifier

Defined in Language.SMT2.Syntax

Methods

(==) :: QualIdentifier -> QualIdentifier -> Bool

(/=) :: QualIdentifier -> QualIdentifier -> Bool

Show QualIdentifier

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> QualIdentifier -> ShowS

show :: QualIdentifier -> String

showList :: [QualIdentifier] -> ShowS

data VarBinding

Constructors

VarBinding Symbol Term

Instances

Eq VarBinding

Defined in Language.SMT2.Syntax

Methods

(==) :: VarBinding -> VarBinding -> Bool

(/=) :: VarBinding -> VarBinding -> Bool

Show VarBinding

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> VarBinding -> ShowS

show :: VarBinding -> String

showList :: [VarBinding] -> ShowS

data SortedVar

Constructors

SortedVar Symbol Sort

Instances

Eq SortedVar

Defined in Language.SMT2.Syntax

Methods

(==) :: SortedVar -> SortedVar -> Bool

(/=) :: SortedVar -> SortedVar -> Bool

Show SortedVar

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SortedVar -> ShowS

show :: SortedVar -> String

showList :: [SortedVar] -> ShowS

data MatchPattern

Constructors

MPVariable Symbol

MPConstructor Symbol (NonEmpty Symbol)

Instances

Eq MatchPattern

Defined in Language.SMT2.Syntax

Methods

(==) :: MatchPattern -> MatchPattern -> Bool

(/=) :: MatchPattern -> MatchPattern -> Bool

Show MatchPattern

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> MatchPattern -> ShowS

show :: MatchPattern -> String

showList :: [MatchPattern] -> ShowS

data MatchCase

Constructors

MatchCase MatchPattern Term

Instances

Eq MatchCase

Defined in Language.SMT2.Syntax

Methods

(==) :: MatchCase -> MatchCase -> Bool

(/=) :: MatchCase -> MatchCase -> Bool

Show MatchCase

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> MatchCase -> ShowS

show :: MatchCase -> String

showList :: [MatchCase] -> ShowS

data Term

Constructors

TermSpecConstant SpecConstant

TermQualIdentifier QualIdentifier

TermApplication QualIdentifier (NonEmpty Term)

TermLet (NonEmpty VarBinding) Term

TermForall (NonEmpty SortedVar) Term

TermExists (NonEmpty SortedVar) Term

TermMatch Term (NonEmpty MatchCase)

TermAnnotation Term (NonEmpty Attribute)

Instances

Eq Term

Defined in Language.SMT2.Syntax

Methods

(==) :: Term -> Term -> Bool

(/=) :: Term -> Term -> Bool

Show Term

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Term -> ShowS

show :: Term -> String

showList :: [Term] -> ShowS

SpecificSuccessRes [Term]

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st [Term]

SpecificSuccessRes (NonEmpty ValuationPair)

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st (NonEmpty ValuationPair)

Theory declarations (Sec 3.7)

data SortSymbolDecl

Constructors

SortSymbolDecl Identifier Numeral [Attribute]

Instances

Eq SortSymbolDecl

Defined in Language.SMT2.Syntax

Methods

(==) :: SortSymbolDecl -> SortSymbolDecl -> Bool

(/=) :: SortSymbolDecl -> SortSymbolDecl -> Bool

Show SortSymbolDecl

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SortSymbolDecl -> ShowS

show :: SortSymbolDecl -> String

showList :: [SortSymbolDecl] -> ShowS

data MetaSpecConstant

Constructors

MSC_NUMERAL

MSC_DECIMAL

MSC_STRING

Instances

Eq MetaSpecConstant

Defined in Language.SMT2.Syntax

Methods

(==) :: MetaSpecConstant -> MetaSpecConstant -> Bool

(/=) :: MetaSpecConstant -> MetaSpecConstant -> Bool

Show MetaSpecConstant

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> MetaSpecConstant -> ShowS

show :: MetaSpecConstant -> String

showList :: [MetaSpecConstant] -> ShowS

data FunSymbolDecl

Constructors

FunConstant SpecConstant Sort [Attribute]

FunMeta MetaSpecConstant Sort [Attribute]

FunIdentifier Identifier (NonEmpty Sort) [Attribute]

potentially overloaded

Instances

Eq FunSymbolDecl

Defined in Language.SMT2.Syntax

Methods

(==) :: FunSymbolDecl -> FunSymbolDecl -> Bool

(/=) :: FunSymbolDecl -> FunSymbolDecl -> Bool

Show FunSymbolDecl

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> FunSymbolDecl -> ShowS

show :: FunSymbolDecl -> String

showList :: [FunSymbolDecl] -> ShowS

data ParFunSymbolDecl

Constructors

NonPar FunSymbolDecl

non-parametric

Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute]

parametric

Instances

Eq ParFunSymbolDecl

Defined in Language.SMT2.Syntax

Methods

(==) :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool

(/=) :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool

Show ParFunSymbolDecl

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ParFunSymbolDecl -> ShowS

show :: ParFunSymbolDecl -> String

showList :: [ParFunSymbolDecl] -> ShowS

data TheoryAttribute

Constructors

TASorts (NonEmpty SortSymbolDecl)

TAFuns (NonEmpty ParFunSymbolDecl)

TASortsDescription StringLiteral

TAFunsDescription StringLiteral

TADefinition StringLiteral

TAValues StringLiteral

TANotes StringLiteral

TAAttr Attribute

Instances

Eq TheoryAttribute

Defined in Language.SMT2.Syntax

Methods

(==) :: TheoryAttribute -> TheoryAttribute -> Bool

(/=) :: TheoryAttribute -> TheoryAttribute -> Bool

Show TheoryAttribute

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> TheoryAttribute -> ShowS

show :: TheoryAttribute -> String

showList :: [TheoryAttribute] -> ShowS

data TheoryDecl

Constructors

TheoryDecl Symbol (NonEmpty TheoryAttribute)

Instances

Eq TheoryDecl

Defined in Language.SMT2.Syntax

Methods

(==) :: TheoryDecl -> TheoryDecl -> Bool

(/=) :: TheoryDecl -> TheoryDecl -> Bool

Show TheoryDecl

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> TheoryDecl -> ShowS

show :: TheoryDecl -> String

showList :: [TheoryDecl] -> ShowS

Logic Declarations (Sec 3.8)

data LogicAttribute

Constructors

LATheories (NonEmpty Symbol)

LALanguage StringLiteral

LAExtensions StringLiteral

LAValues StringLiteral

LANotes StringLiteral

LAAttr Attribute

Instances

Eq LogicAttribute

Defined in Language.SMT2.Syntax

Methods

(==) :: LogicAttribute -> LogicAttribute -> Bool

(/=) :: LogicAttribute -> LogicAttribute -> Bool

Show LogicAttribute

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> LogicAttribute -> ShowS

show :: LogicAttribute -> String

showList :: [LogicAttribute] -> ShowS

data Logic

Constructors

Logic Symbol (NonEmpty LogicAttribute)

Instances

Eq Logic

Defined in Language.SMT2.Syntax

Methods

(==) :: Logic -> Logic -> Bool

(/=) :: Logic -> Logic -> Bool

Show Logic

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Logic -> ShowS

show :: Logic -> String

showList :: [Logic] -> ShowS

Scripts (Sec 3.9)

data SortDec

Constructors

SortDec Symbol Numeral

Instances

Eq SortDec

Defined in Language.SMT2.Syntax

Methods

(==) :: SortDec -> SortDec -> Bool

(/=) :: SortDec -> SortDec -> Bool

Show SortDec

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SortDec -> ShowS

show :: SortDec -> String

showList :: [SortDec] -> ShowS

data SelectorDec

Constructors

SelectorDec Symbol Sort

Instances

Eq SelectorDec

Defined in Language.SMT2.Syntax

Methods

(==) :: SelectorDec -> SelectorDec -> Bool

(/=) :: SelectorDec -> SelectorDec -> Bool

Show SelectorDec

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> SelectorDec -> ShowS

show :: SelectorDec -> String

showList :: [SelectorDec] -> ShowS

data ConstructorDec

Constructors

ConstructorDec Symbol [SelectorDec]

Instances

Eq ConstructorDec

Defined in Language.SMT2.Syntax

Methods

(==) :: ConstructorDec -> ConstructorDec -> Bool

(/=) :: ConstructorDec -> ConstructorDec -> Bool

Show ConstructorDec

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ConstructorDec -> ShowS

show :: ConstructorDec -> String

showList :: [ConstructorDec] -> ShowS

data DatatypeDec

Constructors

DDNonparametric (NonEmpty ConstructorDec)

DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec)

Instances

Eq DatatypeDec

Defined in Language.SMT2.Syntax

Methods

(==) :: DatatypeDec -> DatatypeDec -> Bool

(/=) :: DatatypeDec -> DatatypeDec -> Bool

Show DatatypeDec

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> DatatypeDec -> ShowS

show :: DatatypeDec -> String

showList :: [DatatypeDec] -> ShowS

data FunctionDec

Constructors

FunctionDec Symbol [SortedVar] Sort

Instances

Eq FunctionDec

Defined in Language.SMT2.Syntax

Methods

(==) :: FunctionDec -> FunctionDec -> Bool

(/=) :: FunctionDec -> FunctionDec -> Bool

Show FunctionDec

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> FunctionDec -> ShowS

show :: FunctionDec -> String

showList :: [FunctionDec] -> ShowS

data FunctionDef

Constructors

FunctionDef Symbol [SortedVar] Sort Term

Instances

Eq FunctionDef

Defined in Language.SMT2.Syntax

Methods

(==) :: FunctionDef -> FunctionDef -> Bool

(/=) :: FunctionDef -> FunctionDef -> Bool

Show FunctionDef

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> FunctionDef -> ShowS

show :: FunctionDef -> String

showList :: [FunctionDef] -> ShowS

data PropLiteral

Constructors

PLPositive Symbol

PLNegative Symbol

Instances

Eq PropLiteral

Defined in Language.SMT2.Syntax

Methods

(==) :: PropLiteral -> PropLiteral -> Bool

(/=) :: PropLiteral -> PropLiteral -> Bool

Show PropLiteral

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> PropLiteral -> ShowS

show :: PropLiteral -> String

showList :: [PropLiteral] -> ShowS

data Command

Constructors

Assert Term

CheckSat

CheckSatAssuming [PropLiteral]

DeclareConst Symbol Sort

DeclareDatatype Symbol DatatypeDec

DeclareDatatypes (NonEmpty SortDec) (NonEmpty DatatypeDec)

same number

DeclareFun Symbol [Sort] Sort

DeclareSort Symbol Numeral

DefineFun FunctionDef

DefineFunRec FunctionDef

DefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term)

same number

DefineSort Symbol [Symbol] Sort

Echo StringLiteral

Exit

GetAssertions

GetAssignment

GetInfo InfoFlag

GetModel

GetOption Keyword

GetProof

GetUnsatAssumptions

GetUnsatCore

GetValue (NonEmpty Term)

Pop Numeral

Push Numeral

Reset

ResetAssertions

SetInfo Attribute

SetLogic Symbol

SetOption ScriptOption

Instances

Eq Command

Defined in Language.SMT2.Syntax

Methods

(==) :: Command -> Command -> Bool

(/=) :: Command -> Command -> Bool

Show Command

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> Command -> ShowS

show :: Command -> String

showList :: [Command] -> ShowS

type Script = [Command]

data BValue

Constructors

BTrue

BFalse

Instances

Eq BValue

Defined in Language.SMT2.Syntax

Methods

(==) :: BValue -> BValue -> Bool

(/=) :: BValue -> BValue -> Bool

Show BValue

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> BValue -> ShowS

show :: BValue -> String

showList :: [BValue] -> ShowS

SpecificSuccessRes [TValuationPair]

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st [TValuationPair]

data ScriptOption

Constructors

DiagnosticOutputChannel StringLiteral

GlobalDeclarations BValue

InteractiveMode BValue

PrintSuccess BValue

ProduceAssertions BValue

ProduceAssignments BValue

ProduceModels BValue

ProduceProofs BValue

ProduceUnsatAssumptions BValue

ProduceUnsatCores BValue

RandomSeed Numeral

RegularOutputChannel StringLiteral

ReproducibleResourceLimit Numeral

Verbosity Numeral

OptionAttr Attribute

Instances

Eq ScriptOption

Defined in Language.SMT2.Syntax

Methods

(==) :: ScriptOption -> ScriptOption -> Bool

(/=) :: ScriptOption -> ScriptOption -> Bool

Show ScriptOption

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ScriptOption -> ShowS

show :: ScriptOption -> String

showList :: [ScriptOption] -> ShowS

data InfoFlag

Constructors

AllStatistics

AssertionStackLevels

Authors

ErrorBehavior

Name

ReasonUnknown

Version

IFKeyword Keyword

Instances

Eq InfoFlag

Defined in Language.SMT2.Syntax

Methods

(==) :: InfoFlag -> InfoFlag -> Bool

(/=) :: InfoFlag -> InfoFlag -> Bool

Show InfoFlag

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> InfoFlag -> ShowS

show :: InfoFlag -> String

showList :: [InfoFlag] -> ShowS

Responses (Sec 3.9.1)

data ResErrorBehavior

Constructors

ImmediateExit

ContinuedExecution

Instances

Eq ResErrorBehavior

Defined in Language.SMT2.Syntax

Methods

(==) :: ResErrorBehavior -> ResErrorBehavior -> Bool

(/=) :: ResErrorBehavior -> ResErrorBehavior -> Bool

Show ResErrorBehavior

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ResErrorBehavior -> ShowS

show :: ResErrorBehavior -> String

showList :: [ResErrorBehavior] -> ShowS

data ResReasonUnknown

Constructors

Memout

Incomplete

ResReasonSExpr SExpr

Instances

Eq ResReasonUnknown

Defined in Language.SMT2.Syntax

Methods

(==) :: ResReasonUnknown -> ResReasonUnknown -> Bool

(/=) :: ResReasonUnknown -> ResReasonUnknown -> Bool

Show ResReasonUnknown

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ResReasonUnknown -> ShowS

show :: ResReasonUnknown -> String

showList :: [ResReasonUnknown] -> ShowS

data ResModel

Constructors

RMDefineFun FunctionDef

RMDefineFunRec FunctionDef

RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term)

same number

Instances

SpecificSuccessRes ResModel

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st ResModel

data ResInfo

Constructors

IRErrorBehaviour ResErrorBehavior

IRName StringLiteral

IRAuthours StringLiteral

IRVersion StringLiteral

IRReasonUnknown ResReasonUnknown

IRAttr Attribute

Instances

Eq ResInfo

Defined in Language.SMT2.Syntax

Methods

(==) :: ResInfo -> ResInfo -> Bool

(/=) :: ResInfo -> ResInfo -> Bool

Show ResInfo

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ResInfo -> ShowS

show :: ResInfo -> String

showList :: [ResInfo] -> ShowS

SpecificSuccessRes (NonEmpty ResInfo)

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st (NonEmpty ResInfo)

type ValuationPair = (Term, Term)

type TValuationPair = (Symbol, BValue)

data ResCheckSat

Constructors

Sat

Unsat

Unknown

Instances

Eq ResCheckSat

Defined in Language.SMT2.Syntax

Methods

(==) :: ResCheckSat -> ResCheckSat -> Bool

(/=) :: ResCheckSat -> ResCheckSat -> Bool

Show ResCheckSat

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> ResCheckSat -> ShowS

show :: ResCheckSat -> String

showList :: [ResCheckSat] -> ShowS

SpecificSuccessRes ResCheckSat

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st ResCheckSat

instances

type CheckSatRes = GeneralRes ResCheckSat

type EchoRes = GeneralRes StringLiteral

type GetAssertionsRes = GeneralRes [Term]

type GetAssignmentRes = GeneralRes [TValuationPair]

type GetInfoRes = GeneralRes (NonEmpty ResInfo)

type GetModelRes = GeneralRes ResModel

type GetOptionRes = GeneralRes AttributeValue

type GetProofRes = GeneralRes SExpr

type GetUnsatAssumpRes = GeneralRes [Symbol]

type GetUnsatCoreRes = GeneralRes [Symbol]

type GetValueRes = GeneralRes (NonEmpty ValuationPair)

data GeneralRes res

Constructors

ResSuccess

ResSpecific res

ResUnsupported

ResError StringLiteral

Instances

Eq res => Eq (GeneralRes res)

Defined in Language.SMT2.Syntax

Methods

(==) :: GeneralRes res -> GeneralRes res -> Bool

(/=) :: GeneralRes res -> GeneralRes res -> Bool

Show res => Show (GeneralRes res)

Defined in Language.SMT2.Syntax

Methods

showsPrec :: Int -> GeneralRes res -> ShowS

show :: GeneralRes res -> String

showList :: [GeneralRes res] -> ShowS

class SpecificSuccessRes s where

Methods

specificSuccessRes :: GenParser st s

Instances

SpecificSuccessRes ResCheckSat

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st ResCheckSat

SpecificSuccessRes ResModel

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st ResModel

SpecificSuccessRes AttributeValue

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st AttributeValue

SpecificSuccessRes SExpr

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st SExpr

SpecificSuccessRes StringLiteral

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st StringLiteral

SpecificSuccessRes [TValuationPair]

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st [TValuationPair]

SpecificSuccessRes [Term]

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st [Term]

SpecificSuccessRes [Symbol]

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st [Symbol]

SpecificSuccessRes (NonEmpty ValuationPair)

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st (NonEmpty ValuationPair)

SpecificSuccessRes (NonEmpty ResInfo)

Defined in Language.SMT2.Parser

Methods

specificSuccessRes :: GenParser st (NonEmpty ResInfo)