Hsmtlib-0.2.0.6: Haskell library for easy interaction with SMT-LIB 2 compliant solvers.

Safe Haskell	Safe-Inferred

Hsmtlib.Solvers.Cmd.Parser.Syntax

Documentation

data SpecConstant Source

Constructors

SpecConstantNumeral Integer
SpecConstantDecimal String
SpecConstantHexadecimal String
SpecConstantBinary String
SpecConstantString String

Instances

Show SpecConstant

data Sexpr Source

Constructors

SexprSpecConstant SpecConstant
SexprSymbol String
SexprKeyword String
SexprSxp [Sexpr]

Instances

Show Sexpr

data Identifier Source

Constructors

ISymbol String
I_Symbol String [String]

Instances

Show Identifier

data Sort Source

Constructors

SortId Identifier
SortIdentifiers Identifier [Sort]

Instances

Show Sort

data AttrValue Source

Constructors

AttrValueConstant SpecConstant
AttrValueSymbol String
AttrValueSexpr [Sexpr]

Instances

data Attribute Source

Constructors

Attribute String
AttributeVal String AttrValue

Instances

data QualIdentifier Source

Constructors

QIdentifier Identifier
QIdentifierAs Identifier Sort

Instances

Show QualIdentifier

data VarBinding Source

Constructors

VB String Term

Instances

Show VarBinding

data SortedVar Source

Constructors

SV String Sort

Instances

data Term Source

Constructors

TermSpecConstant SpecConstant
TermQualIdentifier QualIdentifier
TermQualIdentifierT QualIdentifier [Term]
TermLet [VarBinding] Term
TermForall [SortedVar] Term
TermExists [SortedVar] Term
TermAnnot Term [Attribute]

Instances

Show Term

data GenResponse Source

Constructors

Unsupported
Success
Error String

Instances

Show GenResponse

data ErrorBehavior Source

Constructors

ImmediateExit
ContinuedExecution

Instances

Show ErrorBehavior

data ReasonUnknown Source

Constructors

Memout
Incomplete

Instances

Show ReasonUnknown

data CheckSatResponse Source

Constructors

Sat
Unsat
Unknown

Instances

Show CheckSatResponse

type GetInfoResponse = [InfoResponse]Source

data InfoResponse Source

Constructors

ResponseErrorBehavior ErrorBehavior
ResponseName String
ResponseAuthors String
ResponseVersion String
ResponseReasonUnknown ReasonUnknown
ResponseAttribute Attribute

Instances

Show InfoResponse

type GetAssertionsResponse = [Term]Source

type GetProofResponse = Sexpr Source

type GetUnsatCoreResponse = [String]Source

data ValuationPair Source

Constructors

ValuationPair Term Term

Instances

Show ValuationPair

type GetValueResponse = [ValuationPair]Source

data TValuationPair Source

Constructors

TValuationPair String Bool

Instances

Show TValuationPair

type GetAssignmentResponse = [TValuationPair]Source

type GetOptionResponse = AttrValue Source