1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65

--- This module defines data types to represent SMT programs and formulas
--- in Curry.

module XFD.SMTLib.Types where

type SMTLib = [Command]

data Command = DeclareConst String Sort
             | Assert Term
             | CheckSat
             | GetModel
             | GetValue [Term]
             | Echo String
             | Exit
             | Pop Int
             | Push Int
             | SetLogic String
             | SetOption Option

data Option = ProduceModels Bool

data Term = TermSpecConstant SpecConstant
          | TermQualIdentifier QualIdentifier
          | TermQualIdentifierT QualIdentifier [Term]

data QualIdentifier = QIdentifier Identifier

data Identifier = ISymbol String

data SpecConstant = SpecConstantNumeral Int

data Sort = SortId Identifier
          | SortIdentifiers Identifier [Sort]

data SortedVar = SV String Sort

data FunDef = FunDef String [SortedVar] Sort Term


-- Response

data CmdResponse = CmdGenResponse GenResponse
                 | CmdCheckSatResponse CheckSatResponse
                 | CmdGetModelResponse GetModelResponse
                 | CmdGetValueResponse GetValueResponse

data GenResponse = Success
                 | Unsupported
                 | Error String

data CheckSatResponse = Sat
                      | Unsat
                      | Unknown

-- Get Model Response

type GetModelResponse = [ModelResponse]

data ModelResponse = MRDefineFun FunDef

-- Get Valuation Pair

type GetValueResponse = [ValuationPair]

data ValuationPair = ValuationPair Term Term