Copyright	Rogério Pontes 2015
License	WTFPL
Maintainer	rogerp62@outlook.com
Stability	stable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Smtlib.Syntax.Syntax

Description

This module contains The syntax to create commands and responses.

Documentation

type Source = [Command] Source

data Command Source

Instances

Eq Command
Show Command
ShowSL Command

data InfoFlags Source

Constructors

ErrorBehavior
Name
Authors
Version
Status
ReasonUnknown
AllStatistics
InfoFlags String

Instances

Eq InfoFlags
Show InfoFlags
ShowSL InfoFlags

data Term Source

Constructors

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

Instances

Eq Term
Show Term
ShowSL Term

data VarBinding Source

Constructors

VB String Term

Instances

Eq VarBinding
Show VarBinding
ShowSL VarBinding

data SortedVar Source

Constructors

SV String Sort

Instances

Eq SortedVar
Show SortedVar
ShowSL SortedVar

data QualIdentifier Source

Constructors

QIdentifier Identifier
QIdentifierAs Identifier Sort

Instances

Eq QualIdentifier
Show QualIdentifier
ShowSL QualIdentifier

data AttrValue Source

Constructors

AttrValueConstant SpecConstant
AttrValueSymbol String
AttrValueSexpr [Sexpr]

Instances

Eq AttrValue
Show AttrValue
ShowSL AttrValue

data Attribute Source

Constructors

Attribute String
AttributeVal String AttrValue

Instances

Eq Attribute
Show Attribute
ShowSL Attribute

data Identifier Source

Constructors

ISymbol String
I_Symbol String [Int]

Instances

Eq Identifier
Show Identifier
ShowSL Identifier

data Sort Source

Constructors

SortId Identifier
SortIdentifiers Identifier [Sort]

Instances

Eq Sort
Show Sort
ShowSL Sort

data SpecConstant Source

Constructors

SpecConstantNumeral Integer
SpecConstantDecimal String
SpecConstantHexadecimal String
SpecConstantBinary String
SpecConstantString String

Instances

Eq SpecConstant
Show SpecConstant
ShowSL SpecConstant

data Sexpr Source

Constructors

SexprSpecConstant SpecConstant
SexprSymbol String
SexprKeyword String
SexprSxp [Sexpr]

Instances

Eq Sexpr
Show Sexpr
ShowSL Sexpr

data GenResponse Source

Constructors

Unsupported
Success
Error String

Instances

Eq GenResponse
Show GenResponse
ShowSL GenResponse

data ErrorBehavior Source

Constructors

ImmediateExit
ContinuedExecution

Instances

Eq ErrorBehavior
Show ErrorBehavior
ShowSL ErrorBehavior

data ReasonUnknown Source

Constructors

Memout
Incomplete

Instances

Eq ReasonUnknown
Show ReasonUnknown
ShowSL ReasonUnknown

data CheckSatResponse Source

Constructors

Sat
Unsat
Unknown

Instances

Eq CheckSatResponse
Show CheckSatResponse
ShowSL CheckSatResponse

type GetInfoResponse = [InfoResponse] Source

type GetAssertionsResponse = [Term] Source

type GetProofResponse = Sexpr Source

type GetUnsatCoreResponse = [String] Source

data ValuationPair Source

Constructors

ValuationPair Term Term

Instances

Eq ValuationPair
Show ValuationPair
ShowSL ValuationPair

type GetValueResponse = [ValuationPair] Source

data TValuationPair Source

Constructors

TValuationPair String Bool

Instances

Eq TValuationPair
Show TValuationPair
ShowSL TValuationPair

type GetAssignmentResponse = [TValuationPair] Source

type GetOptionResponse = AttrValue Source

SetLogic String
SetOption Option
SetInfo Attribute
DeclareSort String Int
DefineSort String [String] Sort
DeclareFun String [Sort] Sort
DefineFun String [SortedVar] Sort Term
Push Int
Pop Int
Assert Term
CheckSat
GetAssertions
GetProof
GetUnsatCore
GetValue [Term]
GetAssignment
GetOption String
GetInfo InfoFlags
Exit

PrintSucess Bool
ExpandDefinitions Bool
InteractiveMode Bool
ProduceProofs Bool
ProduceUnsatCores Bool
ProduceModels Bool
ProduceAssignments Bool
RegularOutputChannel String
DiagnosticOutputChannel String
RandomSeed Int
Verbosity Int
OptionAttr Attribute

CmdGenResponse GenResponse
CmdGetInfoResponse GetInfoResponse
CmdCheckSatResponse CheckSatResponse
CmdGetAssertionsResponse GetAssertionsResponse
CmdGetAssignmentResponse GetAssignmentResponse
CmdGetProofResponse GetProofResponse
CmdGetUnsatCoreResponse GetUnsatCoreResponse
CmdGetValueResponse GetValueResponse
CmdGetOptionResponse GetOptionResponse

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