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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
|
# import dereference and increment operators
from cython.operator cimport dereference as deref, preincrement as inc
from libc.stdint cimport int32_t, int64_t, uint32_t, uint64_t
from libcpp.string cimport string
from libcpp.vector cimport vector
from libcpp.pair cimport pair
from cvc4kinds cimport Kind
cdef extern from "<iostream>" namespace "std":
cdef cppclass ostream:
pass
ostream cout
cdef extern from "api/cvc4cpp.h" namespace "CVC4":
cdef cppclass Options:
pass
cdef extern from "api/cvc4cpp.h" namespace "CVC4::api":
cdef cppclass Datatype:
Datatype() except +
DatatypeConstructor operator[](const string& name) except +
DatatypeConstructor getConstructor(const string& name) except +
Term getConstructorTerm(const string& name) except +
size_t getNumConstructors() except +
bint isParametric() except +
string toString() except +
cppclass const_iterator:
const_iterator() except +
bint operator==(const const_iterator& it) except +
bint operator!=(const const_iterator& it) except +
const_iterator& operator++();
const DatatypeConstructor& operator*() except +
const_iterator begin() except +
const_iterator end() except +
cdef cppclass DatatypeConstructor:
DatatypeConstructor() except +
DatatypeSelector operator[](const string& name) except +
DatatypeSelector getSelector(const string& name) except +
Term getSelectorTerm(const string& name) except +
string toString() except +
cppclass const_iterator:
const_iterator() except +
bint operator==(const const_iterator& it) except +
bint operator!=(const const_iterator& it) except +
const_iterator& operator++();
const DatatypeSelector& operator*() except +
const_iterator begin() except +
const_iterator end() except +
cdef cppclass DatatypeConstructorDecl:
DatatypeConstructorDecl(const string& name) except +
void addSelector(const string& name, Sort sort) except +
void addSelectorSelf(const string& name) except +
string toString() except +
cdef cppclass DatatypeDecl:
void addConstructor(const DatatypeConstructorDecl& ctor) except +
bint isParametric() except +
string toString() except +
cdef cppclass DatatypeSelector:
DatatypeSelector() except +
string toString() except +
cdef cppclass Op:
Op() except +
bint operator==(const Op&) except +
bint operator!=(const Op&) except +
Kind getKind() except +
Sort getSort() except +
bint isNull() except +
T getIndices[T]() except +
string toString() except +
cdef cppclass Result:
# Note: don't even need constructor
bint isSat() except +
bint isUnsat() except +
bint isSatUnknown() except +
bint isValid() except +
bint isInvalid() except +
bint isValidUnknown() except +
string getUnknownExplanation() except +
string toString() except +
cdef cppclass RoundingMode:
pass
cdef cppclass Solver:
Solver(Options*) except +
Sort getBooleanSort() except +
Sort getIntegerSort() except +
Sort getRealSort() except +
Sort getRegExpSort() except +
Sort getRoundingmodeSort() except +
Sort getStringSort() except +
Sort mkArraySort(Sort indexSort, Sort elemSort) except +
Sort mkBitVectorSort(uint32_t size) except +
Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) except +
Sort mkDatatypeSort(DatatypeDecl dtypedecl) except +
Sort mkFunctionSort(Sort domain, Sort codomain) except +
Sort mkFunctionSort(const vector[Sort]& sorts, Sort codomain) except +
Sort mkParamSort(const string& symbol) except +
Sort mkPredicateSort(const vector[Sort]& sorts) except +
Sort mkRecordSort(const vector[pair[string, Sort]]& fields) except +
Sort mkSetSort(Sort elemSort) except +
Sort mkUninterpretedSort(const string& symbol) except +
Sort mkSortConstructorSort(const string& symbol, size_t arity) except +
Sort mkTupleSort(const vector[Sort]& sorts) except +
Term mkTerm(Op op) except +
Term mkTerm(Op op, const vector[Term]& children) except +
Op mkOp(Kind kind) except +
Op mkOp(Kind kind, Kind k) except +
Op mkOp(Kind kind, const string& arg) except +
Op mkOp(Kind kind, uint32_t arg) except +
Op mkOp(Kind kind, uint32_t arg1, uint32_t arg2) except +
Term mkTrue() except +
Term mkFalse() except +
Term mkBoolean(bint val) except +
Term mkPi() except +
Term mkReal(const string& s) except +
Term mkRegexpEmpty() except +
Term mkRegexpSigma() except +
Term mkEmptySet(Sort s) except +
Term mkSepNil(Sort sort) except +
Term mkString(const string& s) except +
Term mkString(const vector[unsigned]& s) except +
Term mkUniverseSet(Sort sort) except +
Term mkBitVector(uint32_t size) except +
Term mkBitVector(uint32_t size, uint64_t val) except +
Term mkBitVector(const string& s) except +
Term mkBitVector(const string& s, uint32_t base) except +
Term mkConstArray(Sort sort, Term val) except +
Term mkPosInf(uint32_t exp, uint32_t sig) except +
Term mkNegInf(uint32_t exp, uint32_t sig) except +
Term mkNaN(uint32_t exp, uint32_t sig) except +
Term mkPosZero(uint32_t exp, uint32_t sig) except +
Term mkNegZero(uint32_t exp, uint32_t sig) except +
Term mkRoundingMode(RoundingMode rm) except +
Term mkUninterpretedConst(Sort sort, int32_t index) except +
Term mkAbstractValue(const string& index) except +
Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except +
Term mkConst(Sort sort, const string& symbol) except +
# default value for symbol defined in cvc4cpp.h
Term mkConst(Sort sort) except +
Term mkVar(Sort sort, const string& symbol) except +
DatatypeDecl mkDatatypeDecl(const string& name) except +
DatatypeDecl mkDatatypeDecl(const string& name, bint isCoDatatype) except +
DatatypeDecl mkDatatypeDecl(const string& name, Sort param) except +
DatatypeDecl mkDatatypeDecl(const string& name, Sort param, bint isCoDatatype) except +
DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params) except +
DatatypeDecl mkDatatypeDecl(const string& name, vector[Sort]& params, bint isCoDatatype) except +
# default value for symbol defined in cvc4cpp.h
Term mkVar(Sort sort) except +
Term simplify(const Term& t) except +
void assertFormula(Term term) except +
Result checkSat() except +
Result checkSatAssuming(const vector[Term]& assumptions) except +
Result checkValid() except +
Result checkValidAssuming(const vector[Term]& assumptions) except +
Sort declareDatatype(const string& symbol, const vector[DatatypeConstructorDecl]& ctors)
Term declareFun(const string& symbol, Sort sort) except +
Term declareFun(const string& symbol, const vector[Sort]& sorts, Sort sort) except +
Sort declareSort(const string& symbol, uint32_t arity) except +
Term defineFun(const string& symbol, const vector[Term]& bound_vars,
Sort sort, Term term) except +
Term defineFun(Term fun, const vector[Term]& bound_vars, Term term) except +
Term defineFunRec(const string& symbol, const vector[Term]& bound_vars,
Sort sort, Term term) except +
Term defineFunRec(Term fun, const vector[Term]& bound_vars,
Term term) except +
Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars,
vector[Term]& terms) except +
vector[Term] getAssertions() except +
vector[pair[Term, Term]] getAssignment() except +
string getInfo(const string& flag) except +
string getOption(string& option) except +
vector[Term] getUnsatAssumptions() except +
vector[Term] getUnsatCore() except +
Term getValue(Term term) except +
vector[Term] getValue(const vector[Term]& terms) except +
void pop(uint32_t nscopes) except +
void printModel(ostream& out)
void push(uint32_t nscopes) except +
void reset() except +
void resetAssertions() except +
void setInfo(string& keyword, const string& value) except +
void setLogic(const string& logic) except +
void setOption(const string& option, const string& value) except +
cdef cppclass Sort:
Sort() except +
bint operator==(const Sort&) except +
bint operator!=(const Sort&) except +
bint isBoolean() except +
bint isInteger() except +
bint isReal() except +
bint isString() except +
bint isRegExp() except +
bint isRoundingMode() except +
bint isBitVector() except +
bint isFloatingPoint() except +
bint isDatatype() except +
bint isParametricDatatype() except +
bint isFunction() except +
bint isPredicate() except +
bint isTuple() except +
bint isRecord() except +
bint isArray() except +
bint isSet() except +
bint isUninterpretedSort() except +
bint isSortConstructor() except +
bint isFirstClass() except +
bint isFunctionLike() except +
Datatype getDatatype() except +
Sort instantiate(const vector[Sort]& params) except +
bint isUninterpretedSortParameterized() except +
string toString() except +
cdef cppclass Term:
Term()
bint operator==(const Term&) except +
bint operator!=(const Term&) except +
Kind getKind() except +
Sort getSort() except +
bint hasOp() except +
Op getOp() except +
bint isNull() except +
Term notTerm() except +
Term andTerm(const Term& t) except +
Term orTerm(const Term& t) except +
Term xorTerm(const Term& t) except +
Term eqTerm(const Term& t) except +
Term impTerm(const Term& t) except +
Term iteTerm(const Term& then_t, const Term& else_t) except +
string toString() except +
cppclass const_iterator:
const_iterator() except +
bint operator==(const const_iterator& it) except +
bint operator!=(const const_iterator& it) except +
const_iterator& operator++();
Term operator*() except +
const_iterator begin() except +
const_iterator end() except +
cdef extern from "api/cvc4cpp.h" namespace "CVC4::api::RoundingMode":
cdef RoundingMode ROUND_NEAREST_TIES_TO_EVEN,
cdef RoundingMode ROUND_TOWARD_POSITIVE,
cdef RoundingMode ROUND_TOWARD_NEGATIVE,
cdef RoundingMode ROUND_TOWARD_ZERO,
cdef RoundingMode ROUND_NEAREST_TIES_TO_AWAY
|
