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

Safe HaskellSafe-Inferred

Hsmtlib.Solvers.Cmd.Parser.Syntax

Documentation

data SpecConstant Source

Constructors

SpecConstantNumeral Integer 
SpecConstantDecimal String 
SpecConstantHexadecimal String 
SpecConstantBinary String 
SpecConstantString String 

Instances

data Sexpr Source

Constructors

SexprSpecConstant SpecConstant 
SexprSymbol String 
SexprKeyword String 
SexprSxp [Sexpr] 

Instances

data Identifier Source

Constructors

ISymbol String 
I_Symbol String [String] 

Instances

data Sort Source

Constructors

SortId Identifier 
SortIdentifiers Identifier [Sort] 

Instances

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

data VarBinding Source

Constructors

VB String Term 

Instances

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

data GenResponse Source

Constructors

Unsupported 
Success 
Error String 

Instances

data ErrorBehavior Source

Constructors

ImmediateExit 
ContinuedExecution 

Instances

data ReasonUnknown Source

Constructors

Memout 
Incomplete 

Instances

data CheckSatResponse Source

Constructors

Sat 
Unsat 
Unknown 

Instances

type GetInfoResponse = [InfoResponse]Source

data InfoResponse Source

Constructors

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

Instances

type GetAssertionsResponse = [Term]Source

type GetProofResponse = SexprSource

type GetUnsatCoreResponse = [String]Source

data ValuationPair Source

Constructors

ValuationPair Term Term 

Instances

type GetValueResponse = [ValuationPair]Source

data TValuationPair Source

Constructors

TValuationPair String Bool 

Instances

type GetAssignmentResponse = [TValuationPair]Source

type GetOptionResponse = AttrValueSource

data CmdResponse Source

Constructors

CmdGenResponse GenResponse 
CmdGetInfoResponse GetInfoResponse 
CmdCheckSatResponse CheckSatResponse 
CmdGetAssertionResponse GetAssignmentResponse 
CmdGetProofResponse GetProofResponse 
CmdGetUnsatCoreResoponse GetUnsatCoreResponse 
CmdGetValueResponse GetValueResponse 
CmdGetAssigmnentResponse TValuationPair 
CmdGetOptionResponse GetOptionResponse 

Instances