Show SpecConstant Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SpecConstant -> ShowS # show :: SpecConstant -> String # showList :: [SpecConstant] -> ShowS #
Eq SpecConstant Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SpecConstant -> SpecConstant -> Bool # (/=) :: SpecConstant -> SpecConstant -> Bool #

data SExpr Source #

Constructors

SEConstant SpecConstant
SEReservedWord ReservedWord
SESymbol Symbol
SEKeyword Keyword
SEList SList

Instances

Instances details

Show SExpr Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SExpr -> ShowS # show :: SExpr -> String # showList :: [SExpr] -> ShowS #
Eq SExpr Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SExpr -> SExpr -> Bool # (/=) :: SExpr -> SExpr -> Bool #
SpecificSuccessRes SExpr Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st SExpr Source #

type SList = [SExpr] Source #

Identifiers (Sec 3.3)

data Index Source #

Constructors

IxNumeral Numeral
IxSymbol Symbol

Instances

Instances details

Show Index Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Index -> ShowS # show :: Index -> String # showList :: [Index] -> ShowS #
Eq Index Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Index -> Index -> Bool # (/=) :: Index -> Index -> Bool #

data Identifier Source #

Constructors

IdSymbol Symbol
IdIndexed Symbol (NonEmpty Index)

Instances

Instances details

Show Identifier Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Identifier -> ShowS # show :: Identifier -> String # showList :: [Identifier] -> ShowS #
Eq Identifier Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Identifier -> Identifier -> Bool # (/=) :: Identifier -> Identifier -> Bool #

Attributes (Sec. 3.4)

data AttributeValue Source #

Constructors

AttrValSpecConstant SpecConstant
AttrValSymbol Symbol
AttrValSList SList

Instances

Instances details

Show AttributeValue Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> AttributeValue -> ShowS # show :: AttributeValue -> String # showList :: [AttributeValue] -> ShowS #
Eq AttributeValue Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: AttributeValue -> AttributeValue -> Bool # (/=) :: AttributeValue -> AttributeValue -> Bool #
SpecificSuccessRes AttributeValue Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st AttributeValue Source #

data Attribute Source #

Constructors

AttrKey Keyword
AttrKeyValue Keyword AttributeValue

Instances

Instances details

Show Attribute Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Attribute -> ShowS # show :: Attribute -> String # showList :: [Attribute] -> ShowS #
Eq Attribute Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Attribute -> Attribute -> Bool # (/=) :: Attribute -> Attribute -> Bool #

Sorts (Sec 3.5)

data Sort Source #

Constructors

SortSymbol Identifier
SortParameter Identifier (NonEmpty Sort)

Instances

Instances details

Show Sort Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Sort -> ShowS # show :: Sort -> String # showList :: [Sort] -> ShowS #
Eq Sort Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Sort -> Sort -> Bool # (/=) :: Sort -> Sort -> Bool #

Terms and Formulas (Sec 3.6)

data QualIdentifier Source #

Constructors

Unqualified Identifier
Qualified Identifier Sort

Instances

Instances details

Show QualIdentifier Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> QualIdentifier -> ShowS # show :: QualIdentifier -> String # showList :: [QualIdentifier] -> ShowS #
Eq QualIdentifier Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: QualIdentifier -> QualIdentifier -> Bool # (/=) :: QualIdentifier -> QualIdentifier -> Bool #

data VarBinding Source #

Constructors

VarBinding Symbol Term

Instances

Instances details

Show VarBinding Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> VarBinding -> ShowS # show :: VarBinding -> String # showList :: [VarBinding] -> ShowS #
Eq VarBinding Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: VarBinding -> VarBinding -> Bool # (/=) :: VarBinding -> VarBinding -> Bool #

data SortedVar Source #

Constructors

SortedVar Symbol Sort

Instances

Instances details

Show SortedVar Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SortedVar -> ShowS # show :: SortedVar -> String # showList :: [SortedVar] -> ShowS #
Eq SortedVar Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SortedVar -> SortedVar -> Bool # (/=) :: SortedVar -> SortedVar -> Bool #

data MatchPattern Source #

Constructors

MPVariable Symbol
MPConstructor Symbol (NonEmpty Symbol)

Instances

Instances details

Show MatchPattern Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> MatchPattern -> ShowS # show :: MatchPattern -> String # showList :: [MatchPattern] -> ShowS #
Eq MatchPattern Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: MatchPattern -> MatchPattern -> Bool # (/=) :: MatchPattern -> MatchPattern -> Bool #

data MatchCase Source #

Constructors

MatchCase MatchPattern Term

Instances

Instances details

Show MatchCase Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> MatchCase -> ShowS # show :: MatchCase -> String # showList :: [MatchCase] -> ShowS #
Eq MatchCase Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: MatchCase -> MatchCase -> Bool # (/=) :: MatchCase -> MatchCase -> Bool #

data Term Source #

Instances

Instances details

Show Term Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Term -> ShowS # show :: Term -> String # showList :: [Term] -> ShowS #
Eq Term Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Term -> Term -> Bool # (/=) :: Term -> Term -> Bool #
SpecificSuccessRes (NonEmpty ValuationPair) Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st (NonEmpty ValuationPair) Source #
SpecificSuccessRes [Term] Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st [Term] Source #

Theory declarations (Sec 3.7)

data SortSymbolDecl Source #

Constructors

SortSymbolDecl Identifier Numeral [Attribute]

Instances

Instances details

Show SortSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SortSymbolDecl -> ShowS # show :: SortSymbolDecl -> String # showList :: [SortSymbolDecl] -> ShowS #
Eq SortSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SortSymbolDecl -> SortSymbolDecl -> Bool # (/=) :: SortSymbolDecl -> SortSymbolDecl -> Bool #

data MetaSpecConstant Source #

Constructors

MSC_NUMERAL
MSC_DECIMAL
MSC_STRING

Instances

Instances details

Show MetaSpecConstant Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> MetaSpecConstant -> ShowS # show :: MetaSpecConstant -> String # showList :: [MetaSpecConstant] -> ShowS #
Eq MetaSpecConstant Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: MetaSpecConstant -> MetaSpecConstant -> Bool # (/=) :: MetaSpecConstant -> MetaSpecConstant -> Bool #

data FunSymbolDecl Source #

Constructors

FunConstant SpecConstant Sort [Attribute]
FunMeta MetaSpecConstant Sort [Attribute]
FunIdentifier Identifier (NonEmpty Sort) [Attribute]	potentially overloaded

Instances

Instances details

Show FunSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> FunSymbolDecl -> ShowS # show :: FunSymbolDecl -> String # showList :: [FunSymbolDecl] -> ShowS #
Eq FunSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: FunSymbolDecl -> FunSymbolDecl -> Bool # (/=) :: FunSymbolDecl -> FunSymbolDecl -> Bool #

data ParFunSymbolDecl Source #

Constructors

NonPar FunSymbolDecl	non-parametric
Par (NonEmpty Symbol) Identifier (NonEmpty Sort) [Attribute]	parametric

Instances

Instances details

Show ParFunSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ParFunSymbolDecl -> ShowS # show :: ParFunSymbolDecl -> String # showList :: [ParFunSymbolDecl] -> ShowS #
Eq ParFunSymbolDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool # (/=) :: ParFunSymbolDecl -> ParFunSymbolDecl -> Bool #

data TheoryAttribute Source #

Constructors

TASorts (NonEmpty SortSymbolDecl)
TAFuns (NonEmpty ParFunSymbolDecl)
TASortsDescription StringLiteral
TAFunsDescription StringLiteral
TADefinition StringLiteral
TAValues StringLiteral
TANotes StringLiteral
TAAttr Attribute

Instances

Instances details

Show TheoryAttribute Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> TheoryAttribute -> ShowS # show :: TheoryAttribute -> String # showList :: [TheoryAttribute] -> ShowS #
Eq TheoryAttribute Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: TheoryAttribute -> TheoryAttribute -> Bool # (/=) :: TheoryAttribute -> TheoryAttribute -> Bool #

data TheoryDecl Source #

Constructors

TheoryDecl Symbol (NonEmpty TheoryAttribute)

Instances

Instances details

Show TheoryDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> TheoryDecl -> ShowS # show :: TheoryDecl -> String # showList :: [TheoryDecl] -> ShowS #
Eq TheoryDecl Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: TheoryDecl -> TheoryDecl -> Bool # (/=) :: TheoryDecl -> TheoryDecl -> Bool #

Logic Declarations (Sec 3.8)

data LogicAttribute Source #

Constructors

LATheories (NonEmpty Symbol)
LALanguage StringLiteral
LAExtensions StringLiteral
LAValues StringLiteral
LANotes StringLiteral
LAAttr Attribute

Instances

Instances details

Show LogicAttribute Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> LogicAttribute -> ShowS # show :: LogicAttribute -> String # showList :: [LogicAttribute] -> ShowS #
Eq LogicAttribute Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: LogicAttribute -> LogicAttribute -> Bool # (/=) :: LogicAttribute -> LogicAttribute -> Bool #

data Logic Source #

Constructors

Logic Symbol (NonEmpty LogicAttribute)

Instances

Instances details

Show Logic Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Logic -> ShowS # show :: Logic -> String # showList :: [Logic] -> ShowS #
Eq Logic Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Logic -> Logic -> Bool # (/=) :: Logic -> Logic -> Bool #

Scripts (Sec 3.9)

data SortDec Source #

Constructors

SortDec Symbol Numeral

Instances

Instances details

Show SortDec Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SortDec -> ShowS # show :: SortDec -> String # showList :: [SortDec] -> ShowS #
Eq SortDec Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SortDec -> SortDec -> Bool # (/=) :: SortDec -> SortDec -> Bool #

data SelectorDec Source #

Constructors

SelectorDec Symbol Sort

Instances

Instances details

Show SelectorDec Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> SelectorDec -> ShowS # show :: SelectorDec -> String # showList :: [SelectorDec] -> ShowS #
Eq SelectorDec Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: SelectorDec -> SelectorDec -> Bool # (/=) :: SelectorDec -> SelectorDec -> Bool #

data ConstructorDec Source #

Constructors

ConstructorDec Symbol [SelectorDec]

Instances

Instances details

Show ConstructorDec Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ConstructorDec -> ShowS # show :: ConstructorDec -> String # showList :: [ConstructorDec] -> ShowS #
Eq ConstructorDec Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ConstructorDec -> ConstructorDec -> Bool # (/=) :: ConstructorDec -> ConstructorDec -> Bool #

data DatatypeDec Source #

Constructors

DDNonparametric (NonEmpty ConstructorDec)
DDParametric (NonEmpty Symbol) (NonEmpty ConstructorDec)

Instances

Instances details

Show DatatypeDec Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> DatatypeDec -> ShowS # show :: DatatypeDec -> String # showList :: [DatatypeDec] -> ShowS #
Eq DatatypeDec Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: DatatypeDec -> DatatypeDec -> Bool # (/=) :: DatatypeDec -> DatatypeDec -> Bool #

data FunctionDec Source #

Constructors

FunctionDec Symbol [SortedVar] Sort

Instances

Instances details

Show FunctionDec Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> FunctionDec -> ShowS # show :: FunctionDec -> String # showList :: [FunctionDec] -> ShowS #
Eq FunctionDec Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: FunctionDec -> FunctionDec -> Bool # (/=) :: FunctionDec -> FunctionDec -> Bool #

data FunctionDef Source #

Constructors

FunctionDef Symbol [SortedVar] Sort Term

Instances

Instances details

Show FunctionDef Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> FunctionDef -> ShowS # show :: FunctionDef -> String # showList :: [FunctionDef] -> ShowS #
Eq FunctionDef Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: FunctionDef -> FunctionDef -> Bool # (/=) :: FunctionDef -> FunctionDef -> Bool #

data PropLiteral Source #

Constructors

PLPositive Symbol
PLNegative Symbol

Instances

Instances details

Show PropLiteral Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> PropLiteral -> ShowS # show :: PropLiteral -> String # showList :: [PropLiteral] -> ShowS #
Eq PropLiteral Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: PropLiteral -> PropLiteral -> Bool # (/=) :: PropLiteral -> PropLiteral -> Bool #

data Command Source #

Instances

Instances details

Show Command Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> Command -> ShowS # show :: Command -> String # showList :: [Command] -> ShowS #
Eq Command Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: Command -> Command -> Bool # (/=) :: Command -> Command -> Bool #

type Script = [Command] Source #

data BValue Source #

Constructors

BTrue
BFalse

Instances

Instances details

Show BValue Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> BValue -> ShowS # show :: BValue -> String # showList :: [BValue] -> ShowS #
Eq BValue Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: BValue -> BValue -> Bool # (/=) :: BValue -> BValue -> Bool #
SpecificSuccessRes [TValuationPair] Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st [TValuationPair] Source #

data ScriptOption Source #

Instances

Instances details

Show ScriptOption Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ScriptOption -> ShowS # show :: ScriptOption -> String # showList :: [ScriptOption] -> ShowS #
Eq ScriptOption Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ScriptOption -> ScriptOption -> Bool # (/=) :: ScriptOption -> ScriptOption -> Bool #

data InfoFlag Source #

Constructors

AllStatistics
AssertionStackLevels
Authors
ErrorBehavior
Name
ReasonUnknown
Version
IFKeyword Keyword

Instances

Instances details

Show InfoFlag Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> InfoFlag -> ShowS # show :: InfoFlag -> String # showList :: [InfoFlag] -> ShowS #
Eq InfoFlag Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: InfoFlag -> InfoFlag -> Bool # (/=) :: InfoFlag -> InfoFlag -> Bool #

Responses (Sec 3.9.1)

data ResErrorBehavior Source #

Constructors

ImmediateExit
ContinuedExecution

Instances

Instances details

Show ResErrorBehavior Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ResErrorBehavior -> ShowS # show :: ResErrorBehavior -> String # showList :: [ResErrorBehavior] -> ShowS #
Eq ResErrorBehavior Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ResErrorBehavior -> ResErrorBehavior -> Bool # (/=) :: ResErrorBehavior -> ResErrorBehavior -> Bool #

data ResReasonUnknown Source #

Constructors

Memout
Incomplete
ResReasonSExpr SExpr

Instances

Instances details

Show ResReasonUnknown Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ResReasonUnknown -> ShowS # show :: ResReasonUnknown -> String # showList :: [ResReasonUnknown] -> ShowS #
Eq ResReasonUnknown Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ResReasonUnknown -> ResReasonUnknown -> Bool # (/=) :: ResReasonUnknown -> ResReasonUnknown -> Bool #

data ResModel Source #

Constructors

RMDefineFun FunctionDef
RMDefineFunRec FunctionDef
RMDefineFunsRec (NonEmpty FunctionDec) (NonEmpty Term)	same number

Instances

Instances details

SpecificSuccessRes ResModel Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st ResModel Source #

data ResInfo Source #

Constructors

IRErrorBehaviour ResErrorBehavior
IRName StringLiteral
IRAuthours StringLiteral
IRVersion StringLiteral
IRReasonUnknown ResReasonUnknown
IRAttr Attribute

Instances

Instances details

Show ResInfo Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ResInfo -> ShowS # show :: ResInfo -> String # showList :: [ResInfo] -> ShowS #
Eq ResInfo Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ResInfo -> ResInfo -> Bool # (/=) :: ResInfo -> ResInfo -> Bool #
SpecificSuccessRes (NonEmpty ResInfo) Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st (NonEmpty ResInfo) Source #

type ValuationPair = (Term, Term) Source #

type TValuationPair = (Symbol, BValue) Source #

data ResCheckSat Source #

Constructors

Sat
Unsat
Unknown

Instances

Instances details

Show ResCheckSat Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> ResCheckSat -> ShowS # show :: ResCheckSat -> String # showList :: [ResCheckSat] -> ShowS #
Eq ResCheckSat Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: ResCheckSat -> ResCheckSat -> Bool # (/=) :: ResCheckSat -> ResCheckSat -> Bool #
SpecificSuccessRes ResCheckSat Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st ResCheckSat Source #

instances

type CheckSatRes = GeneralRes ResCheckSat Source #

type EchoRes = GeneralRes StringLiteral Source #

type GetAssertionsRes = GeneralRes [Term] Source #

type GetAssignmentRes = GeneralRes [TValuationPair] Source #

type GetInfoRes = GeneralRes (NonEmpty ResInfo) Source #

type GetModelRes = GeneralRes ResModel Source #

type GetOptionRes = GeneralRes AttributeValue Source #

type GetProofRes = GeneralRes SExpr Source #

type GetUnsatAssumpRes = GeneralRes [Symbol] Source #

type GetUnsatCoreRes = GeneralRes [Symbol] Source #

type GetValueRes = GeneralRes (NonEmpty ValuationPair) Source #

data GeneralRes res Source #

Constructors

ResSuccess
ResSpecific res
ResUnsupported
ResError StringLiteral

Instances

Instances details

Show res => Show (GeneralRes res) Source #
Instance details Defined in Language.SMT2.Syntax Methods showsPrec :: Int -> GeneralRes res -> ShowS # show :: GeneralRes res -> String # showList :: [GeneralRes res] -> ShowS #
Eq res => Eq (GeneralRes res) Source #
Instance details Defined in Language.SMT2.Syntax Methods (==) :: GeneralRes res -> GeneralRes res -> Bool # (/=) :: GeneralRes res -> GeneralRes res -> Bool #

class SpecificSuccessRes s where Source #

Methods

specificSuccessRes :: GenParser st s Source #

Instances

Instances details

SpecificSuccessRes AttributeValue Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st AttributeValue Source #
SpecificSuccessRes ResCheckSat Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st ResCheckSat Source #
SpecificSuccessRes ResModel Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st ResModel Source #
SpecificSuccessRes SExpr Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st SExpr Source #
SpecificSuccessRes StringLiteral Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st StringLiteral Source #
SpecificSuccessRes (NonEmpty ResInfo) Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st (NonEmpty ResInfo) Source #
SpecificSuccessRes (NonEmpty ValuationPair) Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st (NonEmpty ValuationPair) Source #
SpecificSuccessRes [Symbol] Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st [Symbol] Source #
SpecificSuccessRes [TValuationPair] Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st [TValuationPair] Source #
SpecificSuccessRes [Term] Source #
Instance details Defined in Language.SMT2.Parser Methods specificSuccessRes :: GenParser st [Term] Source #

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)

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

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