module Smtlib.Syntax.Syntax where
type Source = [Command]
data Command = 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
deriving (Show,Eq)
data Option = PrintSucess Bool
| ExpandDefinitions Bool
| InteractiveMode Bool
| ProduceProofs Bool
| ProduceUnsatCores Bool
| ProduceModels Bool
| ProduceAssignments Bool
| RegularOutputChannel String
| DiagnosticOutputChannel String
| RandomSeed Int
| Verbosity Int
| OptionAttr Attribute
deriving (Show,Eq)
data InfoFlags = ErrorBehavior
| Name
| Authors
| Version
| Status
| ReasonUnknown
| AllStatistics
| InfoFlags String
deriving (Show,Eq)
data Term = TermSpecConstant SpecConstant
| TermQualIdentifier QualIdentifier
| TermQualIdentifierT QualIdentifier [Term]
| TermLet [VarBinding] Term
| TermForall [SortedVar] Term
| TermExists [SortedVar] Term
| TermAnnot Term [Attribute]
deriving (Show,Eq)
data VarBinding = VB String Term deriving (Show,Eq)
data SortedVar = SV String Sort deriving (Show,Eq)
data QualIdentifier = QIdentifier Identifier
| QIdentifierAs Identifier Sort
deriving (Show,Eq)
data AttrValue = AttrValueConstant SpecConstant
| AttrValueSymbol String
| AttrValueSexpr [Sexpr]
deriving (Show,Eq)
data Attribute = Attribute String
| AttributeVal String AttrValue
deriving (Show,Eq)
data Identifier = ISymbol String
| I_Symbol String [Int] deriving (Show,Eq)
data Sort = SortId Identifier | SortIdentifiers Identifier [Sort]
deriving (Show,Eq)
data SpecConstant = SpecConstantNumeral Integer
| SpecConstantDecimal String
| SpecConstantHexadecimal String
| SpecConstantBinary String
| SpecConstantString String
deriving (Show, Eq)
data Sexpr = SexprSpecConstant SpecConstant
| SexprSymbol String
| SexprKeyword String
| SexprSxp [Sexpr]
deriving (Show, Eq)
data CmdResponse = CmdGenResponse GenResponse
| CmdGetInfoResponse GetInfoResponse
| CmdCheckSatResponse CheckSatResponse
| CmdGetAssertionsResponse GetAssertionsResponse
| CmdGetAssignmentResponse GetAssignmentResponse
| CmdGetProofResponse GetProofResponse
| CmdGetUnsatCoreResponse GetUnsatCoreResponse
| CmdGetValueResponse GetValueResponse
| CmdGetOptionResponse GetOptionResponse
deriving (Show, Eq)
data GenResponse = Unsupported | Success | Error String deriving (Show, Eq)
data ErrorBehavior = ImmediateExit | ContinuedExecution deriving (Show, Eq)
data ReasonUnknown = Memout | Incomplete deriving (Show, Eq)
data CheckSatResponse = Sat | Unsat | Unknown deriving (Show, Eq)
type GetInfoResponse = [InfoResponse]
data InfoResponse = ResponseErrorBehavior ErrorBehavior
| ResponseName String
| ResponseAuthors String
| ResponseVersion String
| ResponseReasonUnknown ReasonUnknown
| ResponseAttribute Attribute
deriving (Show, Eq)
type GetAssertionsResponse = [Term]
type GetProofResponse = Sexpr
type GetUnsatCoreResponse = [String]
data ValuationPair = ValuationPair Term Term deriving (Show, Eq)
type GetValueResponse = [ValuationPair]
data TValuationPair = TValuationPair String Bool deriving (Show, Eq)
type GetAssignmentResponse = [TValuationPair]
type GetOptionResponse = AttrValue