projects / cvc5.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
history | raw | HEAD
Refactor DeclareSygusVarCommand and SynthFunCommand to use the API. (#5334)
[cvc5.git] / src / api / cvc4cpp.cpp
1 /********************* */
2 /*! \file cvc4cpp.cpp
3 ** \verbatim
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andrew Reynolds, Andres Noetzli
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
8 ** in the top-level source directory and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
11 **
12 ** \brief The CVC4 C++ API.
13 **
14 ** The CVC4 C++ API.
15 **
16 ** A brief note on how to guard API functions:
17 **
18 ** In general, we think of API guards as a fence -- they are supposed to make
19 ** sure that no invalid arguments get passed into internal realms of CVC4.
20 ** Thus we always want to catch such cases on the API level (and can then
21 ** assert internally that no invalid argument is passed in).
22 **
23 ** The only special case is when we use 3rd party back-ends we have no control
24 ** over, and which throw (invalid_argument) exceptions anyways. In this case,
25 ** we do not replicate argument checks but delegate them to the back-end,
26 ** catch thrown exceptions, and raise a CVC4ApiException.
27 **
28 ** Our Integer implementation, e.g., is such a special case since we support
29 ** two different back end implementations (GMP, CLN). Be aware that they do
30 ** not fully agree on what is (in)valid input, which requires extra checks for
31 ** consistent behavior (see Solver::mkRealFromStrHelper for an example).
32 **/
33
34 #include "api/cvc4cpp.h"
35
36 #include <cstring>
37 #include <sstream>
38
39 #include "base/check.h"
40 #include "base/configuration.h"
41 #include "expr/dtype.h"
42 #include "expr/expr.h"
43 #include "expr/expr_manager.h"
44 #include "expr/expr_manager_scope.h"
45 #include "expr/kind.h"
46 #include "expr/metakind.h"
47 #include "expr/node.h"
48 #include "expr/node_manager.h"
49 #include "expr/sequence.h"
50 #include "expr/type.h"
51 #include "options/main_options.h"
52 #include "options/options.h"
53 #include "options/smt_options.h"
54 #include "smt/model.h"
55 #include "smt/smt_engine.h"
56 #include "smt/smt_mode.h"
57 #include "theory/logic_info.h"
58 #include "theory/theory_model.h"
59 #include "util/random.h"
60 #include "util/result.h"
61 #include "util/utility.h"
62
63 namespace CVC4 {
64 namespace api {
65
66 /* -------------------------------------------------------------------------- */
67 /* Kind */
68 /* -------------------------------------------------------------------------- */
69
70 /* Mapping from external (API) kind to internal kind. */
71 const static std::unordered_map<Kind, CVC4::Kind, KindHashFunction> s_kinds{
72 {INTERNAL_KIND, CVC4::Kind::UNDEFINED_KIND},
73 {UNDEFINED_KIND, CVC4::Kind::UNDEFINED_KIND},
74 {NULL_EXPR, CVC4::Kind::NULL_EXPR},
75 /* Builtin ------------------------------------------------------------- */
76 {UNINTERPRETED_CONSTANT, CVC4::Kind::UNINTERPRETED_CONSTANT},
77 {ABSTRACT_VALUE, CVC4::Kind::ABSTRACT_VALUE},
78 {EQUAL, CVC4::Kind::EQUAL},
79 {DISTINCT, CVC4::Kind::DISTINCT},
80 {CONSTANT, CVC4::Kind::VARIABLE},
81 {VARIABLE, CVC4::Kind::BOUND_VARIABLE},
82 {SEXPR, CVC4::Kind::SEXPR},
83 {LAMBDA, CVC4::Kind::LAMBDA},
84 {WITNESS, CVC4::Kind::WITNESS},
85 /* Boolean ------------------------------------------------------------- */
86 {CONST_BOOLEAN, CVC4::Kind::CONST_BOOLEAN},
87 {NOT, CVC4::Kind::NOT},
88 {AND, CVC4::Kind::AND},
89 {IMPLIES, CVC4::Kind::IMPLIES},
90 {OR, CVC4::Kind::OR},
91 {XOR, CVC4::Kind::XOR},
92 {ITE, CVC4::Kind::ITE},
93 {MATCH, CVC4::Kind::MATCH},
94 {MATCH_CASE, CVC4::Kind::MATCH_CASE},
95 {MATCH_BIND_CASE, CVC4::Kind::MATCH_BIND_CASE},
96 /* UF ------------------------------------------------------------------ */
97 {APPLY_UF, CVC4::Kind::APPLY_UF},
98 {CARDINALITY_CONSTRAINT, CVC4::Kind::CARDINALITY_CONSTRAINT},
99 {CARDINALITY_VALUE, CVC4::Kind::CARDINALITY_VALUE},
100 {HO_APPLY, CVC4::Kind::HO_APPLY},
101 /* Arithmetic ---------------------------------------------------------- */
102 {PLUS, CVC4::Kind::PLUS},
103 {MULT, CVC4::Kind::MULT},
104 {IAND, CVC4::Kind::IAND},
105 {MINUS, CVC4::Kind::MINUS},
106 {UMINUS, CVC4::Kind::UMINUS},
107 {DIVISION, CVC4::Kind::DIVISION},
108 {INTS_DIVISION, CVC4::Kind::INTS_DIVISION},
109 {INTS_MODULUS, CVC4::Kind::INTS_MODULUS},
110 {ABS, CVC4::Kind::ABS},
111 {DIVISIBLE, CVC4::Kind::DIVISIBLE},
112 {POW, CVC4::Kind::POW},
113 {EXPONENTIAL, CVC4::Kind::EXPONENTIAL},
114 {SINE, CVC4::Kind::SINE},
115 {COSINE, CVC4::Kind::COSINE},
116 {TANGENT, CVC4::Kind::TANGENT},
117 {COSECANT, CVC4::Kind::COSECANT},
118 {SECANT, CVC4::Kind::SECANT},
119 {COTANGENT, CVC4::Kind::COTANGENT},
120 {ARCSINE, CVC4::Kind::ARCSINE},
121 {ARCCOSINE, CVC4::Kind::ARCCOSINE},
122 {ARCTANGENT, CVC4::Kind::ARCTANGENT},
123 {ARCCOSECANT, CVC4::Kind::ARCCOSECANT},
124 {ARCSECANT, CVC4::Kind::ARCSECANT},
125 {ARCCOTANGENT, CVC4::Kind::ARCCOTANGENT},
126 {SQRT, CVC4::Kind::SQRT},
127 {CONST_RATIONAL, CVC4::Kind::CONST_RATIONAL},
128 {LT, CVC4::Kind::LT},
129 {LEQ, CVC4::Kind::LEQ},
130 {GT, CVC4::Kind::GT},
131 {GEQ, CVC4::Kind::GEQ},
132 {IS_INTEGER, CVC4::Kind::IS_INTEGER},
133 {TO_INTEGER, CVC4::Kind::TO_INTEGER},
134 {TO_REAL, CVC4::Kind::TO_REAL},
135 {PI, CVC4::Kind::PI},
136 /* BV ------------------------------------------------------------------ */
137 {CONST_BITVECTOR, CVC4::Kind::CONST_BITVECTOR},
138 {BITVECTOR_CONCAT, CVC4::Kind::BITVECTOR_CONCAT},
139 {BITVECTOR_AND, CVC4::Kind::BITVECTOR_AND},
140 {BITVECTOR_OR, CVC4::Kind::BITVECTOR_OR},
141 {BITVECTOR_XOR, CVC4::Kind::BITVECTOR_XOR},
142 {BITVECTOR_NOT, CVC4::Kind::BITVECTOR_NOT},
143 {BITVECTOR_NAND, CVC4::Kind::BITVECTOR_NAND},
144 {BITVECTOR_NOR, CVC4::Kind::BITVECTOR_NOR},
145 {BITVECTOR_XNOR, CVC4::Kind::BITVECTOR_XNOR},
146 {BITVECTOR_COMP, CVC4::Kind::BITVECTOR_COMP},
147 {BITVECTOR_MULT, CVC4::Kind::BITVECTOR_MULT},
148 {BITVECTOR_PLUS, CVC4::Kind::BITVECTOR_PLUS},
149 {BITVECTOR_SUB, CVC4::Kind::BITVECTOR_SUB},
150 {BITVECTOR_NEG, CVC4::Kind::BITVECTOR_NEG},
151 {BITVECTOR_UDIV, CVC4::Kind::BITVECTOR_UDIV},
152 {BITVECTOR_UREM, CVC4::Kind::BITVECTOR_UREM},
153 {BITVECTOR_SDIV, CVC4::Kind::BITVECTOR_SDIV},
154 {BITVECTOR_SREM, CVC4::Kind::BITVECTOR_SREM},
155 {BITVECTOR_SMOD, CVC4::Kind::BITVECTOR_SMOD},
156 {BITVECTOR_SHL, CVC4::Kind::BITVECTOR_SHL},
157 {BITVECTOR_LSHR, CVC4::Kind::BITVECTOR_LSHR},
158 {BITVECTOR_ASHR, CVC4::Kind::BITVECTOR_ASHR},
159 {BITVECTOR_ULT, CVC4::Kind::BITVECTOR_ULT},
160 {BITVECTOR_ULE, CVC4::Kind::BITVECTOR_ULE},
161 {BITVECTOR_UGT, CVC4::Kind::BITVECTOR_UGT},
162 {BITVECTOR_UGE, CVC4::Kind::BITVECTOR_UGE},
163 {BITVECTOR_SLT, CVC4::Kind::BITVECTOR_SLT},
164 {BITVECTOR_SLE, CVC4::Kind::BITVECTOR_SLE},
165 {BITVECTOR_SGT, CVC4::Kind::BITVECTOR_SGT},
166 {BITVECTOR_SGE, CVC4::Kind::BITVECTOR_SGE},
167 {BITVECTOR_ULTBV, CVC4::Kind::BITVECTOR_ULTBV},
168 {BITVECTOR_SLTBV, CVC4::Kind::BITVECTOR_SLTBV},
169 {BITVECTOR_ITE, CVC4::Kind::BITVECTOR_ITE},
170 {BITVECTOR_REDOR, CVC4::Kind::BITVECTOR_REDOR},
171 {BITVECTOR_REDAND, CVC4::Kind::BITVECTOR_REDAND},
172 {BITVECTOR_EXTRACT, CVC4::Kind::BITVECTOR_EXTRACT},
173 {BITVECTOR_REPEAT, CVC4::Kind::BITVECTOR_REPEAT},
174 {BITVECTOR_ZERO_EXTEND, CVC4::Kind::BITVECTOR_ZERO_EXTEND},
175 {BITVECTOR_SIGN_EXTEND, CVC4::Kind::BITVECTOR_SIGN_EXTEND},
176 {BITVECTOR_ROTATE_LEFT, CVC4::Kind::BITVECTOR_ROTATE_LEFT},
177 {BITVECTOR_ROTATE_RIGHT, CVC4::Kind::BITVECTOR_ROTATE_RIGHT},
178 {INT_TO_BITVECTOR, CVC4::Kind::INT_TO_BITVECTOR},
179 {BITVECTOR_TO_NAT, CVC4::Kind::BITVECTOR_TO_NAT},
180 /* FP ------------------------------------------------------------------ */
181 {CONST_FLOATINGPOINT, CVC4::Kind::CONST_FLOATINGPOINT},
182 {CONST_ROUNDINGMODE, CVC4::Kind::CONST_ROUNDINGMODE},
183 {FLOATINGPOINT_FP, CVC4::Kind::FLOATINGPOINT_FP},
184 {FLOATINGPOINT_EQ, CVC4::Kind::FLOATINGPOINT_EQ},
185 {FLOATINGPOINT_ABS, CVC4::Kind::FLOATINGPOINT_ABS},
186 {FLOATINGPOINT_NEG, CVC4::Kind::FLOATINGPOINT_NEG},
187 {FLOATINGPOINT_PLUS, CVC4::Kind::FLOATINGPOINT_PLUS},
188 {FLOATINGPOINT_SUB, CVC4::Kind::FLOATINGPOINT_SUB},
189 {FLOATINGPOINT_MULT, CVC4::Kind::FLOATINGPOINT_MULT},
190 {FLOATINGPOINT_DIV, CVC4::Kind::FLOATINGPOINT_DIV},
191 {FLOATINGPOINT_FMA, CVC4::Kind::FLOATINGPOINT_FMA},
192 {FLOATINGPOINT_SQRT, CVC4::Kind::FLOATINGPOINT_SQRT},
193 {FLOATINGPOINT_REM, CVC4::Kind::FLOATINGPOINT_REM},
194 {FLOATINGPOINT_RTI, CVC4::Kind::FLOATINGPOINT_RTI},
195 {FLOATINGPOINT_MIN, CVC4::Kind::FLOATINGPOINT_MIN},
196 {FLOATINGPOINT_MAX, CVC4::Kind::FLOATINGPOINT_MAX},
197 {FLOATINGPOINT_LEQ, CVC4::Kind::FLOATINGPOINT_LEQ},
198 {FLOATINGPOINT_LT, CVC4::Kind::FLOATINGPOINT_LT},
199 {FLOATINGPOINT_GEQ, CVC4::Kind::FLOATINGPOINT_GEQ},
200 {FLOATINGPOINT_GT, CVC4::Kind::FLOATINGPOINT_GT},
201 {FLOATINGPOINT_ISN, CVC4::Kind::FLOATINGPOINT_ISN},
202 {FLOATINGPOINT_ISSN, CVC4::Kind::FLOATINGPOINT_ISSN},
203 {FLOATINGPOINT_ISZ, CVC4::Kind::FLOATINGPOINT_ISZ},
204 {FLOATINGPOINT_ISINF, CVC4::Kind::FLOATINGPOINT_ISINF},
205 {FLOATINGPOINT_ISNAN, CVC4::Kind::FLOATINGPOINT_ISNAN},
206 {FLOATINGPOINT_ISNEG, CVC4::Kind::FLOATINGPOINT_ISNEG},
207 {FLOATINGPOINT_ISPOS, CVC4::Kind::FLOATINGPOINT_ISPOS},
208 {FLOATINGPOINT_TO_FP_FLOATINGPOINT,
209 CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT},
210 {FLOATINGPOINT_TO_FP_REAL, CVC4::Kind::FLOATINGPOINT_TO_FP_REAL},
211 {FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
212 CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
213 {FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
214 CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
215 {FLOATINGPOINT_TO_FP_GENERIC, CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC},
216 {FLOATINGPOINT_TO_UBV, CVC4::Kind::FLOATINGPOINT_TO_UBV},
217 {FLOATINGPOINT_TO_SBV, CVC4::Kind::FLOATINGPOINT_TO_SBV},
218 {FLOATINGPOINT_TO_REAL, CVC4::Kind::FLOATINGPOINT_TO_REAL},
219 /* Arrays -------------------------------------------------------------- */
220 {SELECT, CVC4::Kind::SELECT},
221 {STORE, CVC4::Kind::STORE},
222 {CONST_ARRAY, CVC4::Kind::STORE_ALL},
223 {EQ_RANGE, CVC4::Kind::EQ_RANGE},
224 /* Datatypes ----------------------------------------------------------- */
225 {APPLY_SELECTOR, CVC4::Kind::APPLY_SELECTOR},
226 {APPLY_CONSTRUCTOR, CVC4::Kind::APPLY_CONSTRUCTOR},
227 {APPLY_TESTER, CVC4::Kind::APPLY_TESTER},
228 {TUPLE_UPDATE, CVC4::Kind::TUPLE_UPDATE},
229 {RECORD_UPDATE, CVC4::Kind::RECORD_UPDATE},
230 {DT_SIZE, CVC4::Kind::DT_SIZE},
231 /* Separation Logic ---------------------------------------------------- */
232 {SEP_NIL, CVC4::Kind::SEP_NIL},
233 {SEP_EMP, CVC4::Kind::SEP_EMP},
234 {SEP_PTO, CVC4::Kind::SEP_PTO},
235 {SEP_STAR, CVC4::Kind::SEP_STAR},
236 {SEP_WAND, CVC4::Kind::SEP_WAND},
237 /* Sets ---------------------------------------------------------------- */
238 {EMPTYSET, CVC4::Kind::EMPTYSET},
239 {UNION, CVC4::Kind::UNION},
240 {INTERSECTION, CVC4::Kind::INTERSECTION},
241 {SETMINUS, CVC4::Kind::SETMINUS},
242 {SUBSET, CVC4::Kind::SUBSET},
243 {MEMBER, CVC4::Kind::MEMBER},
244 {SINGLETON, CVC4::Kind::SINGLETON},
245 {INSERT, CVC4::Kind::INSERT},
246 {CARD, CVC4::Kind::CARD},
247 {COMPLEMENT, CVC4::Kind::COMPLEMENT},
248 {UNIVERSE_SET, CVC4::Kind::UNIVERSE_SET},
249 {JOIN, CVC4::Kind::JOIN},
250 {PRODUCT, CVC4::Kind::PRODUCT},
251 {TRANSPOSE, CVC4::Kind::TRANSPOSE},
252 {TCLOSURE, CVC4::Kind::TCLOSURE},
253 {JOIN_IMAGE, CVC4::Kind::JOIN_IMAGE},
254 {IDEN, CVC4::Kind::IDEN},
255 {COMPREHENSION, CVC4::Kind::COMPREHENSION},
256 {CHOOSE, CVC4::Kind::CHOOSE},
257 {IS_SINGLETON, CVC4::Kind::IS_SINGLETON},
258 /* Bags ---------------------------------------------------------------- */
259 {UNION_MAX, CVC4::Kind::UNION_MAX},
260 {UNION_DISJOINT, CVC4::Kind::UNION_DISJOINT},
261 {INTERSECTION_MIN, CVC4::Kind::INTERSECTION_MIN},
262 {DIFFERENCE_SUBTRACT, CVC4::Kind::DIFFERENCE_SUBTRACT},
263 {DIFFERENCE_REMOVE, CVC4::Kind::DIFFERENCE_REMOVE},
264 {SUBBAG, CVC4::Kind::SUBBAG},
265 {BAG_COUNT, CVC4::Kind::BAG_COUNT},
266 {DUPLICATE_REMOVAL, CVC4::Kind::DUPLICATE_REMOVAL},
267 {MK_BAG, CVC4::Kind::MK_BAG},
268 {EMPTYBAG, CVC4::Kind::EMPTYBAG},
269 {BAG_CARD, CVC4::Kind::BAG_CARD},
270 {BAG_CHOOSE, CVC4::Kind::BAG_CHOOSE},
271 {BAG_IS_SINGLETON, CVC4::Kind::BAG_IS_SINGLETON},
272 {BAG_FROM_SET, CVC4::Kind::BAG_FROM_SET},
273 {BAG_TO_SET, CVC4::Kind::BAG_TO_SET},
274 /* Strings ------------------------------------------------------------- */
275 {STRING_CONCAT, CVC4::Kind::STRING_CONCAT},
276 {STRING_IN_REGEXP, CVC4::Kind::STRING_IN_REGEXP},
277 {STRING_LENGTH, CVC4::Kind::STRING_LENGTH},
278 {STRING_SUBSTR, CVC4::Kind::STRING_SUBSTR},
279 {STRING_UPDATE, CVC4::Kind::STRING_UPDATE},
280 {STRING_CHARAT, CVC4::Kind::STRING_CHARAT},
281 {STRING_CONTAINS, CVC4::Kind::STRING_STRCTN},
282 {STRING_INDEXOF, CVC4::Kind::STRING_STRIDOF},
283 {STRING_REPLACE, CVC4::Kind::STRING_STRREPL},
284 {STRING_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL},
285 {STRING_REPLACE_RE, CVC4::Kind::STRING_REPLACE_RE},
286 {STRING_REPLACE_RE_ALL, CVC4::Kind::STRING_REPLACE_RE_ALL},
287 {STRING_TOLOWER, CVC4::Kind::STRING_TOLOWER},
288 {STRING_TOUPPER, CVC4::Kind::STRING_TOUPPER},
289 {STRING_REV, CVC4::Kind::STRING_REV},
290 {STRING_FROM_CODE, CVC4::Kind::STRING_FROM_CODE},
291 {STRING_TO_CODE, CVC4::Kind::STRING_TO_CODE},
292 {STRING_LT, CVC4::Kind::STRING_LT},
293 {STRING_LEQ, CVC4::Kind::STRING_LEQ},
294 {STRING_PREFIX, CVC4::Kind::STRING_PREFIX},
295 {STRING_SUFFIX, CVC4::Kind::STRING_SUFFIX},
296 {STRING_IS_DIGIT, CVC4::Kind::STRING_IS_DIGIT},
297 {STRING_FROM_INT, CVC4::Kind::STRING_ITOS},
298 {STRING_TO_INT, CVC4::Kind::STRING_STOI},
299 {CONST_STRING, CVC4::Kind::CONST_STRING},
300 {STRING_TO_REGEXP, CVC4::Kind::STRING_TO_REGEXP},
301 {REGEXP_CONCAT, CVC4::Kind::REGEXP_CONCAT},
302 {REGEXP_UNION, CVC4::Kind::REGEXP_UNION},
303 {REGEXP_INTER, CVC4::Kind::REGEXP_INTER},
304 {REGEXP_DIFF, CVC4::Kind::REGEXP_DIFF},
305 {REGEXP_STAR, CVC4::Kind::REGEXP_STAR},
306 {REGEXP_PLUS, CVC4::Kind::REGEXP_PLUS},
307 {REGEXP_OPT, CVC4::Kind::REGEXP_OPT},
308 {REGEXP_RANGE, CVC4::Kind::REGEXP_RANGE},
309 {REGEXP_REPEAT, CVC4::Kind::REGEXP_REPEAT},
310 {REGEXP_LOOP, CVC4::Kind::REGEXP_LOOP},
311 {REGEXP_EMPTY, CVC4::Kind::REGEXP_EMPTY},
312 {REGEXP_SIGMA, CVC4::Kind::REGEXP_SIGMA},
313 {REGEXP_COMPLEMENT, CVC4::Kind::REGEXP_COMPLEMENT},
314 // maps to the same kind as the string versions
315 {SEQ_CONCAT, CVC4::Kind::STRING_CONCAT},
316 {SEQ_LENGTH, CVC4::Kind::STRING_LENGTH},
317 {SEQ_EXTRACT, CVC4::Kind::STRING_SUBSTR},
318 {SEQ_UPDATE, CVC4::Kind::STRING_UPDATE},
319 {SEQ_AT, CVC4::Kind::STRING_CHARAT},
320 {SEQ_CONTAINS, CVC4::Kind::STRING_STRCTN},
321 {SEQ_INDEXOF, CVC4::Kind::STRING_STRIDOF},
322 {SEQ_REPLACE, CVC4::Kind::STRING_STRREPL},
323 {SEQ_REPLACE_ALL, CVC4::Kind::STRING_STRREPLALL},
324 {SEQ_REV, CVC4::Kind::STRING_REV},
325 {SEQ_PREFIX, CVC4::Kind::STRING_PREFIX},
326 {SEQ_SUFFIX, CVC4::Kind::STRING_SUFFIX},
327 {CONST_SEQUENCE, CVC4::Kind::CONST_SEQUENCE},
328 {SEQ_UNIT, CVC4::Kind::SEQ_UNIT},
329 {SEQ_NTH, CVC4::Kind::SEQ_NTH},
330 /* Quantifiers --------------------------------------------------------- */
331 {FORALL, CVC4::Kind::FORALL},
332 {EXISTS, CVC4::Kind::EXISTS},
333 {BOUND_VAR_LIST, CVC4::Kind::BOUND_VAR_LIST},
334 {INST_CLOSURE, CVC4::Kind::INST_CLOSURE},
335 {INST_PATTERN, CVC4::Kind::INST_PATTERN},
336 {INST_NO_PATTERN, CVC4::Kind::INST_NO_PATTERN},
337 {INST_ATTRIBUTE, CVC4::Kind::INST_ATTRIBUTE},
338 {INST_PATTERN_LIST, CVC4::Kind::INST_PATTERN_LIST},
339 {LAST_KIND, CVC4::Kind::LAST_KIND},
340 };
341
342 /* Mapping from internal kind to external (API) kind. */
343 const static std::unordered_map<CVC4::Kind, Kind, CVC4::kind::KindHashFunction>
344 s_kinds_internal{
345 {CVC4::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
346 {CVC4::Kind::NULL_EXPR, NULL_EXPR},
347 /* Builtin --------------------------------------------------------- */
348 {CVC4::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
349 {CVC4::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
350 {CVC4::Kind::EQUAL, EQUAL},
351 {CVC4::Kind::DISTINCT, DISTINCT},
352 {CVC4::Kind::VARIABLE, CONSTANT},
353 {CVC4::Kind::BOUND_VARIABLE, VARIABLE},
354 {CVC4::Kind::LAMBDA, LAMBDA},
355 {CVC4::Kind::WITNESS, WITNESS},
356 /* Boolean --------------------------------------------------------- */
357 {CVC4::Kind::CONST_BOOLEAN, CONST_BOOLEAN},
358 {CVC4::Kind::NOT, NOT},
359 {CVC4::Kind::AND, AND},
360 {CVC4::Kind::IMPLIES, IMPLIES},
361 {CVC4::Kind::OR, OR},
362 {CVC4::Kind::XOR, XOR},
363 {CVC4::Kind::ITE, ITE},
364 {CVC4::Kind::MATCH, MATCH},
365 {CVC4::Kind::MATCH_CASE, MATCH_CASE},
366 {CVC4::Kind::MATCH_BIND_CASE, MATCH_BIND_CASE},
367 /* UF -------------------------------------------------------------- */
368 {CVC4::Kind::APPLY_UF, APPLY_UF},
369 {CVC4::Kind::CARDINALITY_CONSTRAINT, CARDINALITY_CONSTRAINT},
370 {CVC4::Kind::CARDINALITY_VALUE, CARDINALITY_VALUE},
371 {CVC4::Kind::HO_APPLY, HO_APPLY},
372 /* Arithmetic ------------------------------------------------------ */
373 {CVC4::Kind::PLUS, PLUS},
374 {CVC4::Kind::MULT, MULT},
375 {CVC4::Kind::IAND, IAND},
376 {CVC4::Kind::MINUS, MINUS},
377 {CVC4::Kind::UMINUS, UMINUS},
378 {CVC4::Kind::DIVISION, DIVISION},
379 {CVC4::Kind::DIVISION_TOTAL, INTERNAL_KIND},
380 {CVC4::Kind::INTS_DIVISION, INTS_DIVISION},
381 {CVC4::Kind::INTS_DIVISION_TOTAL, INTERNAL_KIND},
382 {CVC4::Kind::INTS_MODULUS, INTS_MODULUS},
383 {CVC4::Kind::INTS_MODULUS_TOTAL, INTERNAL_KIND},
384 {CVC4::Kind::ABS, ABS},
385 {CVC4::Kind::DIVISIBLE, DIVISIBLE},
386 {CVC4::Kind::POW, POW},
387 {CVC4::Kind::EXPONENTIAL, EXPONENTIAL},
388 {CVC4::Kind::SINE, SINE},
389 {CVC4::Kind::COSINE, COSINE},
390 {CVC4::Kind::TANGENT, TANGENT},
391 {CVC4::Kind::COSECANT, COSECANT},
392 {CVC4::Kind::SECANT, SECANT},
393 {CVC4::Kind::COTANGENT, COTANGENT},
394 {CVC4::Kind::ARCSINE, ARCSINE},
395 {CVC4::Kind::ARCCOSINE, ARCCOSINE},
396 {CVC4::Kind::ARCTANGENT, ARCTANGENT},
397 {CVC4::Kind::ARCCOSECANT, ARCCOSECANT},
398 {CVC4::Kind::ARCSECANT, ARCSECANT},
399 {CVC4::Kind::ARCCOTANGENT, ARCCOTANGENT},
400 {CVC4::Kind::SQRT, SQRT},
401 {CVC4::Kind::DIVISIBLE_OP, DIVISIBLE},
402 {CVC4::Kind::CONST_RATIONAL, CONST_RATIONAL},
403 {CVC4::Kind::LT, LT},
404 {CVC4::Kind::LEQ, LEQ},
405 {CVC4::Kind::GT, GT},
406 {CVC4::Kind::GEQ, GEQ},
407 {CVC4::Kind::IS_INTEGER, IS_INTEGER},
408 {CVC4::Kind::TO_INTEGER, TO_INTEGER},
409 {CVC4::Kind::TO_REAL, TO_REAL},
410 {CVC4::Kind::PI, PI},
411 /* BV -------------------------------------------------------------- */
412 {CVC4::Kind::CONST_BITVECTOR, CONST_BITVECTOR},
413 {CVC4::Kind::BITVECTOR_CONCAT, BITVECTOR_CONCAT},
414 {CVC4::Kind::BITVECTOR_AND, BITVECTOR_AND},
415 {CVC4::Kind::BITVECTOR_OR, BITVECTOR_OR},
416 {CVC4::Kind::BITVECTOR_XOR, BITVECTOR_XOR},
417 {CVC4::Kind::BITVECTOR_NOT, BITVECTOR_NOT},
418 {CVC4::Kind::BITVECTOR_NAND, BITVECTOR_NAND},
419 {CVC4::Kind::BITVECTOR_NOR, BITVECTOR_NOR},
420 {CVC4::Kind::BITVECTOR_XNOR, BITVECTOR_XNOR},
421 {CVC4::Kind::BITVECTOR_COMP, BITVECTOR_COMP},
422 {CVC4::Kind::BITVECTOR_MULT, BITVECTOR_MULT},
423 {CVC4::Kind::BITVECTOR_PLUS, BITVECTOR_PLUS},
424 {CVC4::Kind::BITVECTOR_SUB, BITVECTOR_SUB},
425 {CVC4::Kind::BITVECTOR_NEG, BITVECTOR_NEG},
426 {CVC4::Kind::BITVECTOR_UDIV, BITVECTOR_UDIV},
427 {CVC4::Kind::BITVECTOR_UREM, BITVECTOR_UREM},
428 {CVC4::Kind::BITVECTOR_SDIV, BITVECTOR_SDIV},
429 {CVC4::Kind::BITVECTOR_SREM, BITVECTOR_SREM},
430 {CVC4::Kind::BITVECTOR_SMOD, BITVECTOR_SMOD},
431 {CVC4::Kind::BITVECTOR_UDIV_TOTAL, INTERNAL_KIND},
432 {CVC4::Kind::BITVECTOR_UREM_TOTAL, INTERNAL_KIND},
433 {CVC4::Kind::BITVECTOR_SHL, BITVECTOR_SHL},
434 {CVC4::Kind::BITVECTOR_LSHR, BITVECTOR_LSHR},
435 {CVC4::Kind::BITVECTOR_ASHR, BITVECTOR_ASHR},
436 {CVC4::Kind::BITVECTOR_ULT, BITVECTOR_ULT},
437 {CVC4::Kind::BITVECTOR_ULE, BITVECTOR_ULE},
438 {CVC4::Kind::BITVECTOR_UGT, BITVECTOR_UGT},
439 {CVC4::Kind::BITVECTOR_UGE, BITVECTOR_UGE},
440 {CVC4::Kind::BITVECTOR_SLT, BITVECTOR_SLT},
441 {CVC4::Kind::BITVECTOR_SLE, BITVECTOR_SLE},
442 {CVC4::Kind::BITVECTOR_SGT, BITVECTOR_SGT},
443 {CVC4::Kind::BITVECTOR_SGE, BITVECTOR_SGE},
444 {CVC4::Kind::BITVECTOR_ULTBV, BITVECTOR_ULTBV},
445 {CVC4::Kind::BITVECTOR_SLTBV, BITVECTOR_SLTBV},
446 {CVC4::Kind::BITVECTOR_ITE, BITVECTOR_ITE},
447 {CVC4::Kind::BITVECTOR_REDOR, BITVECTOR_REDOR},
448 {CVC4::Kind::BITVECTOR_REDAND, BITVECTOR_REDAND},
449 {CVC4::Kind::BITVECTOR_EXTRACT_OP, BITVECTOR_EXTRACT},
450 {CVC4::Kind::BITVECTOR_REPEAT_OP, BITVECTOR_REPEAT},
451 {CVC4::Kind::BITVECTOR_ZERO_EXTEND_OP, BITVECTOR_ZERO_EXTEND},
452 {CVC4::Kind::BITVECTOR_SIGN_EXTEND_OP, BITVECTOR_SIGN_EXTEND},
453 {CVC4::Kind::BITVECTOR_ROTATE_LEFT_OP, BITVECTOR_ROTATE_LEFT},
454 {CVC4::Kind::BITVECTOR_ROTATE_RIGHT_OP, BITVECTOR_ROTATE_RIGHT},
455 {CVC4::Kind::BITVECTOR_EXTRACT, BITVECTOR_EXTRACT},
456 {CVC4::Kind::BITVECTOR_REPEAT, BITVECTOR_REPEAT},
457 {CVC4::Kind::BITVECTOR_ZERO_EXTEND, BITVECTOR_ZERO_EXTEND},
458 {CVC4::Kind::BITVECTOR_SIGN_EXTEND, BITVECTOR_SIGN_EXTEND},
459 {CVC4::Kind::BITVECTOR_ROTATE_LEFT, BITVECTOR_ROTATE_LEFT},
460 {CVC4::Kind::BITVECTOR_ROTATE_RIGHT, BITVECTOR_ROTATE_RIGHT},
461 {CVC4::Kind::INT_TO_BITVECTOR_OP, INT_TO_BITVECTOR},
462 {CVC4::Kind::INT_TO_BITVECTOR, INT_TO_BITVECTOR},
463 {CVC4::Kind::BITVECTOR_TO_NAT, BITVECTOR_TO_NAT},
464 /* FP -------------------------------------------------------------- */
465 {CVC4::Kind::CONST_FLOATINGPOINT, CONST_FLOATINGPOINT},
466 {CVC4::Kind::CONST_ROUNDINGMODE, CONST_ROUNDINGMODE},
467 {CVC4::Kind::FLOATINGPOINT_FP, FLOATINGPOINT_FP},
468 {CVC4::Kind::FLOATINGPOINT_EQ, FLOATINGPOINT_EQ},
469 {CVC4::Kind::FLOATINGPOINT_ABS, FLOATINGPOINT_ABS},
470 {CVC4::Kind::FLOATINGPOINT_NEG, FLOATINGPOINT_NEG},
471 {CVC4::Kind::FLOATINGPOINT_PLUS, FLOATINGPOINT_PLUS},
472 {CVC4::Kind::FLOATINGPOINT_SUB, FLOATINGPOINT_SUB},
473 {CVC4::Kind::FLOATINGPOINT_MULT, FLOATINGPOINT_MULT},
474 {CVC4::Kind::FLOATINGPOINT_DIV, FLOATINGPOINT_DIV},
475 {CVC4::Kind::FLOATINGPOINT_FMA, FLOATINGPOINT_FMA},
476 {CVC4::Kind::FLOATINGPOINT_SQRT, FLOATINGPOINT_SQRT},
477 {CVC4::Kind::FLOATINGPOINT_REM, FLOATINGPOINT_REM},
478 {CVC4::Kind::FLOATINGPOINT_RTI, FLOATINGPOINT_RTI},
479 {CVC4::Kind::FLOATINGPOINT_MIN, FLOATINGPOINT_MIN},
480 {CVC4::Kind::FLOATINGPOINT_MAX, FLOATINGPOINT_MAX},
481 {CVC4::Kind::FLOATINGPOINT_LEQ, FLOATINGPOINT_LEQ},
482 {CVC4::Kind::FLOATINGPOINT_LT, FLOATINGPOINT_LT},
483 {CVC4::Kind::FLOATINGPOINT_GEQ, FLOATINGPOINT_GEQ},
484 {CVC4::Kind::FLOATINGPOINT_GT, FLOATINGPOINT_GT},
485 {CVC4::Kind::FLOATINGPOINT_ISN, FLOATINGPOINT_ISN},
486 {CVC4::Kind::FLOATINGPOINT_ISSN, FLOATINGPOINT_ISSN},
487 {CVC4::Kind::FLOATINGPOINT_ISZ, FLOATINGPOINT_ISZ},
488 {CVC4::Kind::FLOATINGPOINT_ISINF, FLOATINGPOINT_ISINF},
489 {CVC4::Kind::FLOATINGPOINT_ISNAN, FLOATINGPOINT_ISNAN},
490 {CVC4::Kind::FLOATINGPOINT_ISNEG, FLOATINGPOINT_ISNEG},
491 {CVC4::Kind::FLOATINGPOINT_ISPOS, FLOATINGPOINT_ISPOS},
492 {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR_OP,
493 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
494 {CVC4::Kind::FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
495 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR},
496 {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT_OP,
497 FLOATINGPOINT_TO_FP_FLOATINGPOINT},
498 {CVC4::Kind::FLOATINGPOINT_TO_FP_FLOATINGPOINT,
499 FLOATINGPOINT_TO_FP_FLOATINGPOINT},
500 {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL_OP, FLOATINGPOINT_TO_FP_REAL},
501 {CVC4::Kind::FLOATINGPOINT_TO_FP_REAL, FLOATINGPOINT_TO_FP_REAL},
502 {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR_OP,
503 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
504 {CVC4::Kind::FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
505 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR},
506 {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR_OP,
507 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
508 {CVC4::Kind::FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
509 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR},
510 {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC_OP,
511 FLOATINGPOINT_TO_FP_GENERIC},
512 {CVC4::Kind::FLOATINGPOINT_TO_FP_GENERIC, FLOATINGPOINT_TO_FP_GENERIC},
513 {CVC4::Kind::FLOATINGPOINT_TO_UBV_OP, FLOATINGPOINT_TO_UBV},
514 {CVC4::Kind::FLOATINGPOINT_TO_UBV, FLOATINGPOINT_TO_UBV},
515 {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL_OP, INTERNAL_KIND},
516 {CVC4::Kind::FLOATINGPOINT_TO_UBV_TOTAL, INTERNAL_KIND},
517 {CVC4::Kind::FLOATINGPOINT_TO_SBV_OP, FLOATINGPOINT_TO_SBV},
518 {CVC4::Kind::FLOATINGPOINT_TO_SBV, FLOATINGPOINT_TO_SBV},
519 {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL_OP, INTERNAL_KIND},
520 {CVC4::Kind::FLOATINGPOINT_TO_SBV_TOTAL, INTERNAL_KIND},
521 {CVC4::Kind::FLOATINGPOINT_TO_REAL, FLOATINGPOINT_TO_REAL},
522 {CVC4::Kind::FLOATINGPOINT_TO_REAL_TOTAL, INTERNAL_KIND},
523 /* Arrays ---------------------------------------------------------- */
524 {CVC4::Kind::SELECT, SELECT},
525 {CVC4::Kind::STORE, STORE},
526 {CVC4::Kind::STORE_ALL, CONST_ARRAY},
527 /* Datatypes ------------------------------------------------------- */
528 {CVC4::Kind::APPLY_SELECTOR, APPLY_SELECTOR},
529 {CVC4::Kind::APPLY_CONSTRUCTOR, APPLY_CONSTRUCTOR},
530 {CVC4::Kind::APPLY_SELECTOR_TOTAL, INTERNAL_KIND},
531 {CVC4::Kind::APPLY_TESTER, APPLY_TESTER},
532 {CVC4::Kind::TUPLE_UPDATE_OP, TUPLE_UPDATE},
533 {CVC4::Kind::TUPLE_UPDATE, TUPLE_UPDATE},
534 {CVC4::Kind::RECORD_UPDATE_OP, RECORD_UPDATE},
535 {CVC4::Kind::RECORD_UPDATE, RECORD_UPDATE},
536 {CVC4::Kind::DT_SIZE, DT_SIZE},
537 /* Separation Logic ------------------------------------------------ */
538 {CVC4::Kind::SEP_NIL, SEP_NIL},
539 {CVC4::Kind::SEP_EMP, SEP_EMP},
540 {CVC4::Kind::SEP_PTO, SEP_PTO},
541 {CVC4::Kind::SEP_STAR, SEP_STAR},
542 {CVC4::Kind::SEP_WAND, SEP_WAND},
543 /* Sets ------------------------------------------------------------ */
544 {CVC4::Kind::EMPTYSET, EMPTYSET},
545 {CVC4::Kind::UNION, UNION},
546 {CVC4::Kind::INTERSECTION, INTERSECTION},
547 {CVC4::Kind::SETMINUS, SETMINUS},
548 {CVC4::Kind::SUBSET, SUBSET},
549 {CVC4::Kind::MEMBER, MEMBER},
550 {CVC4::Kind::SINGLETON, SINGLETON},
551 {CVC4::Kind::INSERT, INSERT},
552 {CVC4::Kind::CARD, CARD},
553 {CVC4::Kind::COMPLEMENT, COMPLEMENT},
554 {CVC4::Kind::UNIVERSE_SET, UNIVERSE_SET},
555 {CVC4::Kind::JOIN, JOIN},
556 {CVC4::Kind::PRODUCT, PRODUCT},
557 {CVC4::Kind::TRANSPOSE, TRANSPOSE},
558 {CVC4::Kind::TCLOSURE, TCLOSURE},
559 {CVC4::Kind::JOIN_IMAGE, JOIN_IMAGE},
560 {CVC4::Kind::IDEN, IDEN},
561 {CVC4::Kind::COMPREHENSION, COMPREHENSION},
562 {CVC4::Kind::CHOOSE, CHOOSE},
563 {CVC4::Kind::IS_SINGLETON, IS_SINGLETON},
564 /* Bags ------------------------------------------------------------ */
565 {CVC4::Kind::UNION_MAX, UNION_MAX},
566 {CVC4::Kind::UNION_DISJOINT, UNION_DISJOINT},
567 {CVC4::Kind::INTERSECTION_MIN, INTERSECTION_MIN},
568 {CVC4::Kind::DIFFERENCE_SUBTRACT, DIFFERENCE_SUBTRACT},
569 {CVC4::Kind::DIFFERENCE_REMOVE, DIFFERENCE_REMOVE},
570 {CVC4::Kind::SUBBAG, SUBBAG},
571 {CVC4::Kind::BAG_COUNT, BAG_COUNT},
572 {CVC4::Kind::DUPLICATE_REMOVAL, DUPLICATE_REMOVAL},
573 {CVC4::Kind::MK_BAG, MK_BAG},
574 {CVC4::Kind::EMPTYBAG, EMPTYBAG},
575 {CVC4::Kind::BAG_CARD, BAG_CARD},
576 {CVC4::Kind::BAG_CHOOSE, BAG_CHOOSE},
577 {CVC4::Kind::BAG_IS_SINGLETON, BAG_IS_SINGLETON},
578 {CVC4::Kind::BAG_FROM_SET, BAG_FROM_SET},
579 {CVC4::Kind::BAG_TO_SET, BAG_TO_SET},
580 /* Strings --------------------------------------------------------- */
581 {CVC4::Kind::STRING_CONCAT, STRING_CONCAT},
582 {CVC4::Kind::STRING_IN_REGEXP, STRING_IN_REGEXP},
583 {CVC4::Kind::STRING_LENGTH, STRING_LENGTH},
584 {CVC4::Kind::STRING_SUBSTR, STRING_SUBSTR},
585 {CVC4::Kind::STRING_UPDATE, STRING_UPDATE},
586 {CVC4::Kind::STRING_CHARAT, STRING_CHARAT},
587 {CVC4::Kind::STRING_STRCTN, STRING_CONTAINS},
588 {CVC4::Kind::STRING_STRIDOF, STRING_INDEXOF},
589 {CVC4::Kind::STRING_STRREPL, STRING_REPLACE},
590 {CVC4::Kind::STRING_STRREPLALL, STRING_REPLACE_ALL},
591 {CVC4::Kind::STRING_REPLACE_RE, STRING_REPLACE_RE},
592 {CVC4::Kind::STRING_REPLACE_RE_ALL, STRING_REPLACE_RE_ALL},
593 {CVC4::Kind::STRING_TOLOWER, STRING_TOLOWER},
594 {CVC4::Kind::STRING_TOUPPER, STRING_TOUPPER},
595 {CVC4::Kind::STRING_REV, STRING_REV},
596 {CVC4::Kind::STRING_FROM_CODE, STRING_FROM_CODE},
597 {CVC4::Kind::STRING_TO_CODE, STRING_TO_CODE},
598 {CVC4::Kind::STRING_LT, STRING_LT},
599 {CVC4::Kind::STRING_LEQ, STRING_LEQ},
600 {CVC4::Kind::STRING_PREFIX, STRING_PREFIX},
601 {CVC4::Kind::STRING_SUFFIX, STRING_SUFFIX},
602 {CVC4::Kind::STRING_IS_DIGIT, STRING_IS_DIGIT},
603 {CVC4::Kind::STRING_ITOS, STRING_FROM_INT},
604 {CVC4::Kind::STRING_STOI, STRING_TO_INT},
605 {CVC4::Kind::CONST_STRING, CONST_STRING},
606 {CVC4::Kind::STRING_TO_REGEXP, STRING_TO_REGEXP},
607 {CVC4::Kind::REGEXP_CONCAT, REGEXP_CONCAT},
608 {CVC4::Kind::REGEXP_UNION, REGEXP_UNION},
609 {CVC4::Kind::REGEXP_INTER, REGEXP_INTER},
610 {CVC4::Kind::REGEXP_DIFF, REGEXP_DIFF},
611 {CVC4::Kind::REGEXP_STAR, REGEXP_STAR},
612 {CVC4::Kind::REGEXP_PLUS, REGEXP_PLUS},
613 {CVC4::Kind::REGEXP_OPT, REGEXP_OPT},
614 {CVC4::Kind::REGEXP_RANGE, REGEXP_RANGE},
615 {CVC4::Kind::REGEXP_REPEAT, REGEXP_REPEAT},
616 {CVC4::Kind::REGEXP_REPEAT_OP, REGEXP_REPEAT},
617 {CVC4::Kind::REGEXP_LOOP, REGEXP_LOOP},
618 {CVC4::Kind::REGEXP_LOOP_OP, REGEXP_LOOP},
619 {CVC4::Kind::REGEXP_EMPTY, REGEXP_EMPTY},
620 {CVC4::Kind::REGEXP_SIGMA, REGEXP_SIGMA},
621 {CVC4::Kind::REGEXP_COMPLEMENT, REGEXP_COMPLEMENT},
622 {CVC4::Kind::CONST_SEQUENCE, CONST_SEQUENCE},
623 {CVC4::Kind::SEQ_UNIT, SEQ_UNIT},
624 {CVC4::Kind::SEQ_NTH, SEQ_NTH},
625 /* Quantifiers ----------------------------------------------------- */
626 {CVC4::Kind::FORALL, FORALL},
627 {CVC4::Kind::EXISTS, EXISTS},
628 {CVC4::Kind::BOUND_VAR_LIST, BOUND_VAR_LIST},
629 {CVC4::Kind::INST_CLOSURE, INST_CLOSURE},
630 {CVC4::Kind::INST_PATTERN, INST_PATTERN},
631 {CVC4::Kind::INST_NO_PATTERN, INST_NO_PATTERN},
632 {CVC4::Kind::INST_ATTRIBUTE, INST_ATTRIBUTE},
633 {CVC4::Kind::INST_PATTERN_LIST, INST_PATTERN_LIST},
634 /* ----------------------------------------------------------------- */
635 {CVC4::Kind::LAST_KIND, LAST_KIND},
636 };
637
638 /* Set of kinds for indexed operators */
639 const static std::unordered_set<Kind, KindHashFunction> s_indexed_kinds(
640 {RECORD_UPDATE,
641 DIVISIBLE,
642 IAND,
643 BITVECTOR_REPEAT,
644 BITVECTOR_ZERO_EXTEND,
645 BITVECTOR_SIGN_EXTEND,
646 BITVECTOR_ROTATE_LEFT,
647 BITVECTOR_ROTATE_RIGHT,
648 INT_TO_BITVECTOR,
649 FLOATINGPOINT_TO_UBV,
650 FLOATINGPOINT_TO_SBV,
651 TUPLE_UPDATE,
652 BITVECTOR_EXTRACT,
653 FLOATINGPOINT_TO_FP_IEEE_BITVECTOR,
654 FLOATINGPOINT_TO_FP_FLOATINGPOINT,
655 FLOATINGPOINT_TO_FP_REAL,
656 FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR,
657 FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR,
658 FLOATINGPOINT_TO_FP_GENERIC});
659
660 namespace {
661
662 bool isDefinedKind(Kind k) { return k > UNDEFINED_KIND && k < LAST_KIND; }
663
664 /** Returns true if the internal kind is one where the API term structure
665 * differs from internal structure. This happens for APPLY_* kinds.
666 * The API takes a "higher-order" perspective and treats functions as well
667 * as datatype constructors/selectors/testers as terms
668 * but interally they are not
669 */
670 bool isApplyKind(CVC4::Kind k)
671 {
672 return (k == CVC4::Kind::APPLY_UF || k == CVC4::Kind::APPLY_CONSTRUCTOR
673 || k == CVC4::Kind::APPLY_SELECTOR || k == CVC4::Kind::APPLY_TESTER);
674 }
675
676 #ifdef CVC4_ASSERTIONS
677 bool isDefinedIntKind(CVC4::Kind k)
678 {
679 return k != CVC4::Kind::UNDEFINED_KIND && k != CVC4::Kind::LAST_KIND;
680 }
681 #endif
682
683 uint32_t minArity(Kind k)
684 {
685 Assert(isDefinedKind(k));
686 Assert(isDefinedIntKind(extToIntKind(k)));
687 uint32_t min = CVC4::ExprManager::minArity(extToIntKind(k));
688
689 // At the API level, we treat functions/constructors/selectors/testers as
690 // normal terms instead of making them part of the operator
691 if (isApplyKind(extToIntKind(k)))
692 {
693 min++;
694 }
695 return min;
696 }
697
698 uint32_t maxArity(Kind k)
699 {
700 Assert(isDefinedKind(k));
701 Assert(isDefinedIntKind(extToIntKind(k)));
702 uint32_t max = CVC4::ExprManager::maxArity(extToIntKind(k));
703
704 // At the API level, we treat functions/constructors/selectors/testers as
705 // normal terms instead of making them part of the operator
706 if (isApplyKind(extToIntKind(k))
707 && max != std::numeric_limits<uint32_t>::max()) // be careful not to
708 // overflow
709 {
710 max++;
711 }
712 return max;
713 }
714
715 } // namespace
716
717 std::string kindToString(Kind k)
718 {
719 return k == INTERNAL_KIND ? "INTERNAL_KIND"
720 : CVC4::kind::kindToString(extToIntKind(k));
721 }
722
723 std::ostream& operator<<(std::ostream& out, Kind k)
724 {
725 switch (k)
726 {
727 case INTERNAL_KIND: out << "INTERNAL_KIND"; break;
728 default: out << extToIntKind(k);
729 }
730 return out;
731 }
732
733 size_t KindHashFunction::operator()(Kind k) const { return k; }
734
735 /* -------------------------------------------------------------------------- */
736 /* API guard helpers */
737 /* -------------------------------------------------------------------------- */
738
739 namespace {
740
741 class CVC4ApiExceptionStream
742 {
743 public:
744 CVC4ApiExceptionStream() {}
745 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
746 * a destructor that throws an exception and in C++11 all destructors
747 * default to noexcept(true) (else this triggers a call to std::terminate). */
748 ~CVC4ApiExceptionStream() noexcept(false)
749 {
750 if (!std::uncaught_exception())
751 {
752 throw CVC4ApiException(d_stream.str());
753 }
754 }
755
756 std::ostream& ostream() { return d_stream; }
757
758 private:
759 std::stringstream d_stream;
760 };
761
762 class CVC4ApiRecoverableExceptionStream
763 {
764 public:
765 CVC4ApiRecoverableExceptionStream() {}
766 /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
767 * a destructor that throws an exception and in C++11 all destructors
768 * default to noexcept(true) (else this triggers a call to std::terminate). */
769 ~CVC4ApiRecoverableExceptionStream() noexcept(false)
770 {
771 if (!std::uncaught_exception())
772 {
773 throw CVC4ApiRecoverableException(d_stream.str());
774 }
775 }
776
777 std::ostream& ostream() { return d_stream; }
778
779 private:
780 std::stringstream d_stream;
781 };
782
783 #define CVC4_API_CHECK(cond) \
784 CVC4_PREDICT_TRUE(cond) \
785 ? (void)0 : OstreamVoider() & CVC4ApiExceptionStream().ostream()
786
787 #define CVC4_API_RECOVERABLE_CHECK(cond) \
788 CVC4_PREDICT_TRUE(cond) \
789 ? (void)0 : OstreamVoider() & CVC4ApiRecoverableExceptionStream().ostream()
790
791 #define CVC4_API_CHECK_NOT_NULL \
792 CVC4_API_CHECK(!isNullHelper()) \
793 << "Invalid call to '" << __PRETTY_FUNCTION__ \
794 << "', expected non-null object";
795
796 #define CVC4_API_ARG_CHECK_NOT_NULL(arg) \
797 CVC4_API_CHECK(!arg.isNull()) << "Invalid null argument for '" << #arg << "'";
798
799 #define CVC4_API_ARG_CHECK_NOT_NULLPTR(arg) \
800 CVC4_API_CHECK(arg != nullptr) \
801 << "Invalid null argument for '" << #arg << "'";
802
803 #define CVC4_API_KIND_CHECK(kind) \
804 CVC4_API_CHECK(isDefinedKind(kind)) \
805 << "Invalid kind '" << kindToString(kind) << "'";
806
807 #define CVC4_API_KIND_CHECK_EXPECTED(cond, kind) \
808 CVC4_PREDICT_TRUE(cond) \
809 ? (void)0 \
810 : OstreamVoider() \
811 & CVC4ApiExceptionStream().ostream() \
812 << "Invalid kind '" << kindToString(kind) << "', expected "
813
814 #define CVC4_API_ARG_CHECK_EXPECTED(cond, arg) \
815 CVC4_PREDICT_TRUE(cond) \
816 ? (void)0 \
817 : OstreamVoider() \
818 & CVC4ApiExceptionStream().ostream() \
819 << "Invalid argument '" << arg << "' for '" << #arg \
820 << "', expected "
821
822 #define CVC4_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \
823 CVC4_PREDICT_TRUE(cond) \
824 ? (void)0 \
825 : OstreamVoider() \
826 & CVC4ApiExceptionStream().ostream() \
827 << "Invalid size of argument '" << #arg << "', expected "
828
829 #define CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, arg, idx) \
830 CVC4_PREDICT_TRUE(cond) \
831 ? (void)0 \
832 : OstreamVoider() \
833 & CVC4ApiExceptionStream().ostream() \
834 << "Invalid " << what << " '" << arg << "' at index " << idx \
835 << ", expected "
836
837 #define CVC4_API_SOLVER_TRY_CATCH_BEGIN \
838 try \
839 {
840 #define CVC4_API_SOLVER_TRY_CATCH_END \
841 } \
842 catch (const CVC4::RecoverableModalException& e) \
843 { \
844 throw CVC4ApiRecoverableException(e.getMessage()); \
845 } \
846 catch (const CVC4::Exception& e) { throw CVC4ApiException(e.getMessage()); } \
847 catch (const std::invalid_argument& e) { throw CVC4ApiException(e.what()); }
848
849 #define CVC4_API_SOLVER_CHECK_SORT(sort) \
850 CVC4_API_CHECK(this == sort.d_solver) \
851 << "Given sort is not associated with this solver";
852
853 #define CVC4_API_SOLVER_CHECK_TERM(term) \
854 CVC4_API_CHECK(this == term.d_solver) \
855 << "Given term is not associated with this solver";
856
857 #define CVC4_API_SOLVER_CHECK_OP(op) \
858 CVC4_API_CHECK(this == op.d_solver) \
859 << "Given operator is not associated with this solver";
860
861 } // namespace
862
863 /* -------------------------------------------------------------------------- */
864 /* Result */
865 /* -------------------------------------------------------------------------- */
866
867 Result::Result(const CVC4::Result& r) : d_result(new CVC4::Result(r)) {}
868
869 Result::Result() : d_result(new CVC4::Result()) {}
870
871 bool Result::isNull() const
872 {
873 return d_result->getType() == CVC4::Result::TYPE_NONE;
874 }
875
876 bool Result::isSat(void) const
877 {
878 return d_result->getType() == CVC4::Result::TYPE_SAT
879 && d_result->isSat() == CVC4::Result::SAT;
880 }
881
882 bool Result::isUnsat(void) const
883 {
884 return d_result->getType() == CVC4::Result::TYPE_SAT
885 && d_result->isSat() == CVC4::Result::UNSAT;
886 }
887
888 bool Result::isSatUnknown(void) const
889 {
890 return d_result->getType() == CVC4::Result::TYPE_SAT
891 && d_result->isSat() == CVC4::Result::SAT_UNKNOWN;
892 }
893
894 bool Result::isEntailed(void) const
895 {
896 return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
897 && d_result->isEntailed() == CVC4::Result::ENTAILED;
898 }
899
900 bool Result::isNotEntailed(void) const
901 {
902 return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
903 && d_result->isEntailed() == CVC4::Result::NOT_ENTAILED;
904 }
905
906 bool Result::isEntailmentUnknown(void) const
907 {
908 return d_result->getType() == CVC4::Result::TYPE_ENTAILMENT
909 && d_result->isEntailed() == CVC4::Result::ENTAILMENT_UNKNOWN;
910 }
911
912 bool Result::operator==(const Result& r) const
913 {
914 return *d_result == *r.d_result;
915 }
916
917 bool Result::operator!=(const Result& r) const
918 {
919 return *d_result != *r.d_result;
920 }
921
922 std::string Result::getUnknownExplanation(void) const
923 {
924 std::stringstream ss;
925 ss << d_result->whyUnknown();
926 return ss.str();
927 }
928
929 std::string Result::toString(void) const { return d_result->toString(); }
930
931 // !!! This is only temporarily available until the parser is fully migrated
932 // to the new API. !!!
933 CVC4::Result Result::getResult(void) const { return *d_result; }
934
935 std::ostream& operator<<(std::ostream& out, const Result& r)
936 {
937 out << r.toString();
938 return out;
939 }
940
941 /* -------------------------------------------------------------------------- */
942 /* Sort */
943 /* -------------------------------------------------------------------------- */
944
945 Sort::Sort(const Solver* slv, const CVC4::Type& t)
946 : d_solver(slv), d_type(new CVC4::Type(t))
947 {
948 }
949
950 Sort::Sort() : d_solver(nullptr), d_type(new CVC4::Type()) {}
951
952 Sort::~Sort() {}
953
954 /* Helpers */
955 /* -------------------------------------------------------------------------- */
956
957 /* Split out to avoid nested API calls (problematic with API tracing). */
958 /* .......................................................................... */
959
960 bool Sort::isNullHelper() const { return d_type->isNull(); }
961
962 bool Sort::operator==(const Sort& s) const { return *d_type == *s.d_type; }
963
964 bool Sort::operator!=(const Sort& s) const { return *d_type != *s.d_type; }
965
966 bool Sort::operator<(const Sort& s) const { return *d_type < *s.d_type; }
967
968 bool Sort::operator>(const Sort& s) const { return *d_type > *s.d_type; }
969
970 bool Sort::operator<=(const Sort& s) const { return *d_type <= *s.d_type; }
971
972 bool Sort::operator>=(const Sort& s) const { return *d_type >= *s.d_type; }
973
974 bool Sort::isNull() const { return isNullHelper(); }
975
976 bool Sort::isBoolean() const { return d_type->isBoolean(); }
977
978 bool Sort::isInteger() const { return d_type->isInteger(); }
979
980 bool Sort::isReal() const { return d_type->isReal(); }
981
982 bool Sort::isString() const { return d_type->isString(); }
983
984 bool Sort::isRegExp() const { return d_type->isRegExp(); }
985
986 bool Sort::isRoundingMode() const { return d_type->isRoundingMode(); }
987
988 bool Sort::isBitVector() const { return d_type->isBitVector(); }
989
990 bool Sort::isFloatingPoint() const { return d_type->isFloatingPoint(); }
991
992 bool Sort::isDatatype() const { return d_type->isDatatype(); }
993
994 bool Sort::isParametricDatatype() const
995 {
996 if (!d_type->isDatatype()) return false;
997 return TypeNode::fromType(*d_type).isParametricDatatype();
998 }
999
1000 bool Sort::isConstructor() const { return d_type->isConstructor(); }
1001 bool Sort::isSelector() const { return d_type->isSelector(); }
1002 bool Sort::isTester() const { return d_type->isTester(); }
1003
1004 bool Sort::isFunction() const { return d_type->isFunction(); }
1005
1006 bool Sort::isPredicate() const { return d_type->isPredicate(); }
1007
1008 bool Sort::isTuple() const { return d_type->isTuple(); }
1009
1010 bool Sort::isRecord() const { return d_type->isRecord(); }
1011
1012 bool Sort::isArray() const { return d_type->isArray(); }
1013
1014 bool Sort::isSet() const { return d_type->isSet(); }
1015
1016 bool Sort::isBag() const { return TypeNode::fromType(*d_type).isBag(); }
1017
1018 bool Sort::isSequence() const { return d_type->isSequence(); }
1019
1020 bool Sort::isUninterpretedSort() const { return d_type->isSort(); }
1021
1022 bool Sort::isSortConstructor() const { return d_type->isSortConstructor(); }
1023
1024 bool Sort::isFirstClass() const { return d_type->isFirstClass(); }
1025
1026 bool Sort::isFunctionLike() const { return d_type->isFunctionLike(); }
1027
1028 bool Sort::isSubsortOf(Sort s) const { return d_type->isSubtypeOf(*s.d_type); }
1029
1030 bool Sort::isComparableTo(Sort s) const
1031 {
1032 return d_type->isComparableTo(*s.d_type);
1033 }
1034
1035 Datatype Sort::getDatatype() const
1036 {
1037 NodeManagerScope scope(d_solver->getNodeManager());
1038 CVC4_API_CHECK(isDatatype()) << "Expected datatype sort.";
1039 return Datatype(d_solver, TypeNode::fromType(*d_type).getDType());
1040 }
1041
1042 Sort Sort::instantiate(const std::vector<Sort>& params) const
1043 {
1044 NodeManagerScope scope(d_solver->getNodeManager());
1045 CVC4_API_CHECK(isParametricDatatype() || isSortConstructor())
1046 << "Expected parametric datatype or sort constructor sort.";
1047 std::vector<TypeNode> tparams;
1048 for (const Sort& s : params)
1049 {
1050 tparams.push_back(TypeNode::fromType(*s.d_type.get()));
1051 }
1052 if (d_type->isDatatype())
1053 {
1054 return Sort(d_solver,
1055 TypeNode::fromType(*d_type)
1056 .instantiateParametricDatatype(tparams)
1057 .toType());
1058 }
1059 Assert(d_type->isSortConstructor());
1060 return Sort(d_solver,
1061 d_solver->getNodeManager()
1062 ->mkSort(TypeNode::fromType(*d_type), tparams)
1063 .toType());
1064 }
1065
1066 std::string Sort::toString() const
1067 {
1068 if (d_solver != nullptr)
1069 {
1070 NodeManagerScope scope(d_solver->getNodeManager());
1071 return d_type->toString();
1072 }
1073 return d_type->toString();
1074 }
1075
1076 // !!! This is only temporarily available until the parser is fully migrated
1077 // to the new API. !!!
1078 CVC4::Type Sort::getType(void) const { return *d_type; }
1079
1080 /* Constructor sort ------------------------------------------------------- */
1081
1082 size_t Sort::getConstructorArity() const
1083 {
1084 CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1085 return ConstructorType(*d_type).getArity();
1086 }
1087
1088 std::vector<Sort> Sort::getConstructorDomainSorts() const
1089 {
1090 CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1091 std::vector<CVC4::Type> types = ConstructorType(*d_type).getArgTypes();
1092 return typeVectorToSorts(d_solver, types);
1093 }
1094
1095 Sort Sort::getConstructorCodomainSort() const
1096 {
1097 CVC4_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this);
1098 return Sort(d_solver, ConstructorType(*d_type).getRangeType());
1099 }
1100
1101 /* Selector sort ------------------------------------------------------- */
1102
1103 Sort Sort::getSelectorDomainSort() const
1104 {
1105 CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1106 TypeNode typeNode = TypeNode::fromType(*d_type);
1107 return Sort(d_solver, typeNode.getSelectorDomainType().toType());
1108 }
1109
1110 Sort Sort::getSelectorCodomainSort() const
1111 {
1112 CVC4_API_CHECK(isSelector()) << "Not a selector sort: " << (*this);
1113 TypeNode typeNode = TypeNode::fromType(*d_type);
1114 return Sort(d_solver, typeNode.getSelectorRangeType().toType());
1115 }
1116
1117 /* Tester sort ------------------------------------------------------- */
1118
1119 Sort Sort::getTesterDomainSort() const
1120 {
1121 CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1122 TypeNode typeNode = TypeNode::fromType(*d_type);
1123 return Sort(d_solver, typeNode.getTesterDomainType().toType());
1124 }
1125
1126 Sort Sort::getTesterCodomainSort() const
1127 {
1128 CVC4_API_CHECK(isTester()) << "Not a tester sort: " << (*this);
1129 return d_solver->getBooleanSort();
1130 }
1131
1132 /* Function sort ------------------------------------------------------- */
1133
1134 size_t Sort::getFunctionArity() const
1135 {
1136 CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1137 return FunctionType(*d_type).getArity();
1138 }
1139
1140 std::vector<Sort> Sort::getFunctionDomainSorts() const
1141 {
1142 CVC4_API_CHECK(isFunction()) << "Not a function sort: " << (*this);
1143 std::vector<CVC4::Type> types = FunctionType(*d_type).getArgTypes();
1144 return typeVectorToSorts(d_solver, types);
1145 }
1146
1147 Sort Sort::getFunctionCodomainSort() const
1148 {
1149 CVC4_API_CHECK(isFunction()) << "Not a function sort" << (*this);
1150 return Sort(d_solver, FunctionType(*d_type).getRangeType());
1151 }
1152
1153 /* Array sort ---------------------------------------------------------- */
1154
1155 Sort Sort::getArrayIndexSort() const
1156 {
1157 CVC4_API_CHECK(isArray()) << "Not an array sort.";
1158 return Sort(d_solver, ArrayType(*d_type).getIndexType());
1159 }
1160
1161 Sort Sort::getArrayElementSort() const
1162 {
1163 CVC4_API_CHECK(isArray()) << "Not an array sort.";
1164 return Sort(d_solver, ArrayType(*d_type).getConstituentType());
1165 }
1166
1167 /* Set sort ------------------------------------------------------------ */
1168
1169 Sort Sort::getSetElementSort() const
1170 {
1171 CVC4_API_CHECK(isSet()) << "Not a set sort.";
1172 return Sort(d_solver, SetType(*d_type).getElementType());
1173 }
1174
1175 /* Bag sort ------------------------------------------------------------ */
1176
1177 Sort Sort::getBagElementSort() const
1178 {
1179 CVC4_API_CHECK(isBag()) << "Not a bag sort.";
1180 TypeNode typeNode = TypeNode::fromType(*d_type);
1181 Type type = typeNode.getBagElementType().toType();
1182 return Sort(d_solver, type);
1183 }
1184
1185 /* Sequence sort ------------------------------------------------------- */
1186
1187 Sort Sort::getSequenceElementSort() const
1188 {
1189 CVC4_API_CHECK(isSequence()) << "Not a sequence sort.";
1190 return Sort(d_solver, SequenceType(*d_type).getElementType());
1191 }
1192
1193 /* Uninterpreted sort -------------------------------------------------- */
1194
1195 std::string Sort::getUninterpretedSortName() const
1196 {
1197 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1198 return SortType(*d_type).getName();
1199 }
1200
1201 bool Sort::isUninterpretedSortParameterized() const
1202 {
1203 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1204 return SortType(*d_type).isParameterized();
1205 }
1206
1207 std::vector<Sort> Sort::getUninterpretedSortParamSorts() const
1208 {
1209 CVC4_API_CHECK(isUninterpretedSort()) << "Not an uninterpreted sort.";
1210 std::vector<CVC4::Type> types = SortType(*d_type).getParamTypes();
1211 return typeVectorToSorts(d_solver, types);
1212 }
1213
1214 /* Sort constructor sort ----------------------------------------------- */
1215
1216 std::string Sort::getSortConstructorName() const
1217 {
1218 CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1219 return SortConstructorType(*d_type).getName();
1220 }
1221
1222 size_t Sort::getSortConstructorArity() const
1223 {
1224 CVC4_API_CHECK(isSortConstructor()) << "Not a sort constructor sort.";
1225 return SortConstructorType(*d_type).getArity();
1226 }
1227
1228 /* Bit-vector sort ----------------------------------------------------- */
1229
1230 uint32_t Sort::getBVSize() const
1231 {
1232 CVC4_API_CHECK(isBitVector()) << "Not a bit-vector sort.";
1233 return BitVectorType(*d_type).getSize();
1234 }
1235
1236 /* Floating-point sort ------------------------------------------------- */
1237
1238 uint32_t Sort::getFPExponentSize() const
1239 {
1240 CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1241 return FloatingPointType(*d_type).getExponentSize();
1242 }
1243
1244 uint32_t Sort::getFPSignificandSize() const
1245 {
1246 CVC4_API_CHECK(isFloatingPoint()) << "Not a floating-point sort.";
1247 return FloatingPointType(*d_type).getSignificandSize();
1248 }
1249
1250 /* Datatype sort ------------------------------------------------------- */
1251
1252 std::vector<Sort> Sort::getDatatypeParamSorts() const
1253 {
1254 CVC4_API_CHECK(isParametricDatatype()) << "Not a parametric datatype sort.";
1255 std::vector<CVC4::TypeNode> typeNodes =
1256 TypeNode::fromType(*d_type).getParamTypes();
1257 std::vector<Sort> sorts;
1258 for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++)
1259 {
1260 sorts.push_back(Sort(d_solver, typeNodes[i].toType()));
1261 }
1262 return sorts;
1263 }
1264
1265 size_t Sort::getDatatypeArity() const
1266 {
1267 CVC4_API_CHECK(isDatatype()) << "Not a datatype sort.";
1268 return TypeNode::fromType(*d_type).getNumChildren() - 1;
1269 }
1270
1271 /* Tuple sort ---------------------------------------------------------- */
1272
1273 size_t Sort::getTupleLength() const
1274 {
1275 CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
1276 return TypeNode::fromType(*d_type).getTupleLength();
1277 }
1278
1279 std::vector<Sort> Sort::getTupleSorts() const
1280 {
1281 CVC4_API_CHECK(isTuple()) << "Not a tuple sort.";
1282 std::vector<CVC4::TypeNode> typeNodes =
1283 TypeNode::fromType(*d_type).getTupleTypes();
1284 std::vector<Sort> sorts;
1285 for (size_t i = 0, tsize = typeNodes.size(); i < tsize; i++)
1286 {
1287 sorts.push_back(Sort(d_solver, typeNodes[i].toType()));
1288 }
1289 return sorts;
1290 }
1291
1292 /* --------------------------------------------------------------------- */
1293
1294 std::ostream& operator<<(std::ostream& out, const Sort& s)
1295 {
1296 out << s.toString();
1297 return out;
1298 }
1299
1300 size_t SortHashFunction::operator()(const Sort& s) const
1301 {
1302 return TypeHashFunction()(*s.d_type);
1303 }
1304
1305 /* -------------------------------------------------------------------------- */
1306 /* Op */
1307 /* -------------------------------------------------------------------------- */
1308
1309 Op::Op() : d_solver(nullptr), d_kind(NULL_EXPR), d_node(new CVC4::Node()) {}
1310
1311 Op::Op(const Solver* slv, const Kind k)
1312 : d_solver(slv), d_kind(k), d_node(new CVC4::Node())
1313 {
1314 }
1315
1316 Op::Op(const Solver* slv, const Kind k, const CVC4::Expr& e)
1317 : d_solver(slv), d_kind(k), d_node(new CVC4::Node(Node::fromExpr(e)))
1318 {
1319 }
1320
1321 Op::Op(const Solver* slv, const Kind k, const CVC4::Node& n)
1322 : d_solver(slv), d_kind(k), d_node(new CVC4::Node(n))
1323 {
1324 }
1325
1326 Op::~Op()
1327 {
1328 if (d_solver != nullptr)
1329 {
1330 // Ensure that the correct node manager is in scope when the node is
1331 // destroyed.
1332 NodeManagerScope scope(d_solver->getNodeManager());
1333 d_node.reset();
1334 }
1335 }
1336
1337 /* Helpers */
1338 /* -------------------------------------------------------------------------- */
1339
1340 /* Split out to avoid nested API calls (problematic with API tracing). */
1341 /* .......................................................................... */
1342
1343 bool Op::isNullHelper() const
1344 {
1345 return (d_node->isNull() && (d_kind == NULL_EXPR));
1346 }
1347
1348 bool Op::isIndexedHelper() const { return !d_node->isNull(); }
1349
1350 /* Public methods */
1351 bool Op::operator==(const Op& t) const
1352 {
1353 if (d_node->isNull() && t.d_node->isNull())
1354 {
1355 return (d_kind == t.d_kind);
1356 }
1357 else if (d_node->isNull() || t.d_node->isNull())
1358 {
1359 return false;
1360 }
1361 return (d_kind == t.d_kind) && (*d_node == *t.d_node);
1362 }
1363
1364 bool Op::operator!=(const Op& t) const { return !(*this == t); }
1365
1366 Kind Op::getKind() const
1367 {
1368 CVC4_API_CHECK(d_kind != NULL_EXPR) << "Expecting a non-null Kind";
1369 return d_kind;
1370 }
1371
1372 bool Op::isNull() const { return isNullHelper(); }
1373
1374 bool Op::isIndexed() const { return isIndexedHelper(); }
1375
1376 template <>
1377 std::string Op::getIndices() const
1378 {
1379 CVC4_API_CHECK_NOT_NULL;
1380 CVC4_API_CHECK(!d_node->isNull())
1381 << "Expecting a non-null internal expression. This Op is not indexed.";
1382
1383 std::string i;
1384 Kind k = intToExtKind(d_node->getKind());
1385
1386 if (k == DIVISIBLE)
1387 {
1388 // DIVISIBLE returns a string index to support
1389 // arbitrary precision integers
1390 CVC4::Integer _int = d_node->getConst<Divisible>().k;
1391 i = _int.toString();
1392 }
1393 else if (k == RECORD_UPDATE)
1394 {
1395 i = d_node->getConst<RecordUpdate>().getField();
1396 }
1397 else
1398 {
1399 CVC4_API_CHECK(false) << "Can't get string index from"
1400 << " kind " << kindToString(k);
1401 }
1402
1403 return i;
1404 }
1405
1406 template <>
1407 uint32_t Op::getIndices() const
1408 {
1409 CVC4_API_CHECK_NOT_NULL;
1410 CVC4_API_CHECK(!d_node->isNull())
1411 << "Expecting a non-null internal expression. This Op is not indexed.";
1412
1413 uint32_t i = 0;
1414 Kind k = intToExtKind(d_node->getKind());
1415 switch (k)
1416 {
1417 case BITVECTOR_REPEAT:
1418 i = d_node->getConst<BitVectorRepeat>().d_repeatAmount;
1419 break;
1420 case BITVECTOR_ZERO_EXTEND:
1421 i = d_node->getConst<BitVectorZeroExtend>().d_zeroExtendAmount;
1422 break;
1423 case BITVECTOR_SIGN_EXTEND:
1424 i = d_node->getConst<BitVectorSignExtend>().d_signExtendAmount;
1425 break;
1426 case BITVECTOR_ROTATE_LEFT:
1427 i = d_node->getConst<BitVectorRotateLeft>().d_rotateLeftAmount;
1428 break;
1429 case BITVECTOR_ROTATE_RIGHT:
1430 i = d_node->getConst<BitVectorRotateRight>().d_rotateRightAmount;
1431 break;
1432 case INT_TO_BITVECTOR: i = d_node->getConst<IntToBitVector>().d_size; break;
1433 case IAND: i = d_node->getConst<IntAnd>().d_size; break;
1434 case FLOATINGPOINT_TO_UBV:
1435 i = d_node->getConst<FloatingPointToUBV>().bvs.d_size;
1436 break;
1437 case FLOATINGPOINT_TO_SBV:
1438 i = d_node->getConst<FloatingPointToSBV>().bvs.d_size;
1439 break;
1440 case TUPLE_UPDATE: i = d_node->getConst<TupleUpdate>().getIndex(); break;
1441 case REGEXP_REPEAT:
1442 i = d_node->getConst<RegExpRepeat>().d_repeatAmount;
1443 break;
1444 default:
1445 CVC4ApiExceptionStream().ostream() << "Can't get uint32_t index from"
1446 << " kind " << kindToString(k);
1447 }
1448 return i;
1449 }
1450
1451 template <>
1452 std::pair<uint32_t, uint32_t> Op::getIndices() const
1453 {
1454 CVC4_API_CHECK_NOT_NULL;
1455 CVC4_API_CHECK(!d_node->isNull())
1456 << "Expecting a non-null internal expression. This Op is not indexed.";
1457
1458 std::pair<uint32_t, uint32_t> indices;
1459 Kind k = intToExtKind(d_node->getKind());
1460
1461 // using if/else instead of case statement because want local variables
1462 if (k == BITVECTOR_EXTRACT)
1463 {
1464 CVC4::BitVectorExtract ext = d_node->getConst<BitVectorExtract>();
1465 indices = std::make_pair(ext.d_high, ext.d_low);
1466 }
1467 else if (k == FLOATINGPOINT_TO_FP_IEEE_BITVECTOR)
1468 {
1469 CVC4::FloatingPointToFPIEEEBitVector ext =
1470 d_node->getConst<FloatingPointToFPIEEEBitVector>();
1471 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1472 }
1473 else if (k == FLOATINGPOINT_TO_FP_FLOATINGPOINT)
1474 {
1475 CVC4::FloatingPointToFPFloatingPoint ext =
1476 d_node->getConst<FloatingPointToFPFloatingPoint>();
1477 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1478 }
1479 else if (k == FLOATINGPOINT_TO_FP_REAL)
1480 {
1481 CVC4::FloatingPointToFPReal ext = d_node->getConst<FloatingPointToFPReal>();
1482 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1483 }
1484 else if (k == FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR)
1485 {
1486 CVC4::FloatingPointToFPSignedBitVector ext =
1487 d_node->getConst<FloatingPointToFPSignedBitVector>();
1488 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1489 }
1490 else if (k == FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR)
1491 {
1492 CVC4::FloatingPointToFPUnsignedBitVector ext =
1493 d_node->getConst<FloatingPointToFPUnsignedBitVector>();
1494 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1495 }
1496 else if (k == FLOATINGPOINT_TO_FP_GENERIC)
1497 {
1498 CVC4::FloatingPointToFPGeneric ext =
1499 d_node->getConst<FloatingPointToFPGeneric>();
1500 indices = std::make_pair(ext.t.exponent(), ext.t.significand());
1501 }
1502 else if (k == REGEXP_LOOP)
1503 {
1504 CVC4::RegExpLoop ext = d_node->getConst<RegExpLoop>();
1505 indices = std::make_pair(ext.d_loopMinOcc, ext.d_loopMaxOcc);
1506 }
1507 else
1508 {
1509 CVC4_API_CHECK(false) << "Can't get pair<uint32_t, uint32_t> indices from"
1510 << " kind " << kindToString(k);
1511 }
1512 return indices;
1513 }
1514
1515 std::string Op::toString() const
1516 {
1517 CVC4_API_CHECK_NOT_NULL;
1518 if (d_node->isNull())
1519 {
1520 return kindToString(d_kind);
1521 }
1522 else
1523 {
1524 CVC4_API_CHECK(!d_node->isNull())
1525 << "Expecting a non-null internal expression";
1526 if (d_solver != nullptr)
1527 {
1528 NodeManagerScope scope(d_solver->getNodeManager());
1529 return d_node->toString();
1530 }
1531 return d_node->toString();
1532 }
1533 }
1534
1535 // !!! This is only temporarily available until the parser is fully migrated
1536 // to the new API. !!!
1537 CVC4::Expr Op::getExpr(void) const
1538 {
1539 if (d_node->isNull()) return Expr();
1540 NodeManagerScope scope(d_solver->getNodeManager());
1541 return d_node->toExpr();
1542 }
1543
1544 std::ostream& operator<<(std::ostream& out, const Op& t)
1545 {
1546 out << t.toString();
1547 return out;
1548 }
1549
1550 size_t OpHashFunction::operator()(const Op& t) const
1551 {
1552 if (t.isIndexedHelper())
1553 {
1554 return ExprHashFunction()(t.d_node->toExpr());
1555 }
1556 else
1557 {
1558 return KindHashFunction()(t.d_kind);
1559 }
1560 }
1561
1562 /* -------------------------------------------------------------------------- */
1563 /* Term */
1564 /* -------------------------------------------------------------------------- */
1565
1566 Term::Term() : d_solver(nullptr), d_node(new CVC4::Node()) {}
1567
1568 Term::Term(const Solver* slv, const CVC4::Expr& e) : d_solver(slv)
1569 {
1570 // Ensure that we create the node in the correct node manager.
1571 NodeManagerScope scope(d_solver->getNodeManager());
1572 d_node.reset(new CVC4::Node(e));
1573 }
1574
1575 Term::Term(const Solver* slv, const CVC4::Node& n) : d_solver(slv)
1576 {
1577 // Ensure that we create the node in the correct node manager.
1578 NodeManagerScope scope(d_solver->getNodeManager());
1579 d_node.reset(new CVC4::Node(n));
1580 }
1581
1582 Term::~Term()
1583 {
1584 if (d_solver != nullptr)
1585 {
1586 // Ensure that the correct node manager is in scope when the node is
1587 // destroyed.
1588 NodeManagerScope scope(d_solver->getNodeManager());
1589 d_node.reset();
1590 }
1591 }
1592
1593 bool Term::isNullHelper() const
1594 {
1595 /* Split out to avoid nested API calls (problematic with API tracing). */
1596 return d_node->isNull();
1597 }
1598
1599 Kind Term::getKindHelper() const
1600 {
1601 // Sequence kinds do not exist internally, so we must convert their internal
1602 // (string) versions back to sequence. All operators where this is
1603 // necessary are such that their first child is of sequence type, which
1604 // we check here.
1605 if (getNumChildren() > 0 && (*this)[0].getSort().isSequence())
1606 {
1607 switch (d_node->getKind())
1608 {
1609 case CVC4::Kind::STRING_CONCAT: return SEQ_CONCAT;
1610 case CVC4::Kind::STRING_LENGTH: return SEQ_LENGTH;
1611 case CVC4::Kind::STRING_SUBSTR: return SEQ_EXTRACT;
1612 case CVC4::Kind::STRING_UPDATE: return SEQ_UPDATE;
1613 case CVC4::Kind::STRING_CHARAT: return SEQ_AT;
1614 case CVC4::Kind::STRING_STRCTN: return SEQ_CONTAINS;
1615 case CVC4::Kind::STRING_STRIDOF: return SEQ_INDEXOF;
1616 case CVC4::Kind::STRING_STRREPL: return SEQ_REPLACE;
1617 case CVC4::Kind::STRING_STRREPLALL: return SEQ_REPLACE_ALL;
1618 case CVC4::Kind::STRING_REV: return SEQ_REV;
1619 case CVC4::Kind::STRING_PREFIX: return SEQ_PREFIX;
1620 case CVC4::Kind::STRING_SUFFIX: return SEQ_SUFFIX;
1621 default:
1622 // fall through to conversion below
1623 break;
1624 }
1625 }
1626 // Notice that kinds like APPLY_TYPE_ASCRIPTION will be converted to
1627 // INTERNAL_KIND.
1628 return intToExtKind(d_node->getKind());
1629 }
1630
1631 bool Term::operator==(const Term& t) const { return *d_node == *t.d_node; }
1632
1633 bool Term::operator!=(const Term& t) const { return *d_node != *t.d_node; }
1634
1635 bool Term::operator<(const Term& t) const { return *d_node < *t.d_node; }
1636
1637 bool Term::operator>(const Term& t) const { return *d_node > *t.d_node; }
1638
1639 bool Term::operator<=(const Term& t) const { return *d_node <= *t.d_node; }
1640
1641 bool Term::operator>=(const Term& t) const { return *d_node >= *t.d_node; }
1642
1643 size_t Term::getNumChildren() const
1644 {
1645 CVC4_API_CHECK_NOT_NULL;
1646 // special case for apply kinds
1647 if (isApplyKind(d_node->getKind()))
1648 {
1649 return d_node->getNumChildren() + 1;
1650 }
1651 return d_node->getNumChildren();
1652 }
1653
1654 Term Term::operator[](size_t index) const
1655 {
1656 CVC4_API_CHECK_NOT_NULL;
1657 // special cases for apply kinds
1658 if (isApplyKind(d_node->getKind()))
1659 {
1660 CVC4_API_CHECK(d_node->hasOperator())
1661 << "Expected apply kind to have operator when accessing child of Term";
1662 if (index == 0)
1663 {
1664 // return the operator
1665 return Term(d_solver, d_node->getOperator().toExpr());
1666 }
1667 // otherwise we are looking up child at (index-1)
1668 index--;
1669 }
1670 return Term(d_solver, (*d_node)[index].toExpr());
1671 }
1672
1673 uint64_t Term::getId() const
1674 {
1675 CVC4_API_CHECK_NOT_NULL;
1676 return d_node->getId();
1677 }
1678
1679 Kind Term::getKind() const
1680 {
1681 CVC4_API_CHECK_NOT_NULL;
1682 return getKindHelper();
1683 }
1684
1685 Sort Term::getSort() const
1686 {
1687 CVC4_API_CHECK_NOT_NULL;
1688 NodeManagerScope scope(d_solver->getNodeManager());
1689 return Sort(d_solver, d_node->getType().toType());
1690 }
1691
1692 Term Term::substitute(Term e, Term replacement) const
1693 {
1694 CVC4_API_CHECK_NOT_NULL;
1695 CVC4_API_CHECK(!e.isNull())
1696 << "Expected non-null term to replace in substitute";
1697 CVC4_API_CHECK(!replacement.isNull())
1698 << "Expected non-null term as replacement in substitute";
1699 CVC4_API_CHECK(e.getSort().isComparableTo(replacement.getSort()))
1700 << "Expecting terms of comparable sort in substitute";
1701 return Term(d_solver,
1702 d_node->substitute(TNode(*e.d_node), TNode(*replacement.d_node)));
1703 }
1704
1705 Term Term::substitute(const std::vector<Term> es,
1706 const std::vector<Term>& replacements) const
1707 {
1708 CVC4_API_CHECK_NOT_NULL;
1709 CVC4_API_CHECK(es.size() == replacements.size())
1710 << "Expecting vectors of the same arity in substitute";
1711 for (unsigned i = 0, nterms = es.size(); i < nterms; i++)
1712 {
1713 CVC4_API_CHECK(!es[i].isNull())
1714 << "Expected non-null term to replace in substitute";
1715 CVC4_API_CHECK(!replacements[i].isNull())
1716 << "Expected non-null term as replacement in substitute";
1717 CVC4_API_CHECK(es[i].getSort().isComparableTo(replacements[i].getSort()))
1718 << "Expecting terms of comparable sort in substitute";
1719 }
1720
1721 std::vector<Node> nodes = termVectorToNodes(es);
1722 std::vector<Node> nodeReplacements = termVectorToNodes(replacements);
1723 return Term(d_solver,
1724 d_node->substitute(nodes.begin(),
1725 nodes.end(),
1726 nodeReplacements.begin(),
1727 nodeReplacements.end()));
1728 }
1729
1730 bool Term::hasOp() const
1731 {
1732 CVC4_API_CHECK_NOT_NULL;
1733 return d_node->hasOperator();
1734 }
1735
1736 Op Term::getOp() const
1737 {
1738 CVC4_API_CHECK_NOT_NULL;
1739 CVC4_API_CHECK(d_node->hasOperator())
1740 << "Expecting Term to have an Op when calling getOp()";
1741
1742 // special cases for parameterized operators that are not indexed operators
1743 // the API level differs from the internal structure
1744 // indexed operators are stored in Ops
1745 // whereas functions and datatype operators are terms, and the Op
1746 // is one of the APPLY_* kinds
1747 if (isApplyKind(d_node->getKind()))
1748 {
1749 return Op(d_solver, intToExtKind(d_node->getKind()));
1750 }
1751 else if (d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
1752 {
1753 // it's an indexed operator
1754 // so we should return the indexed op
1755 CVC4::Node op = d_node->getOperator();
1756 return Op(d_solver, intToExtKind(d_node->getKind()), op);
1757 }
1758 // Notice this is the only case where getKindHelper is used, since the
1759 // cases above do not have special cases for intToExtKind.
1760 return Op(d_solver, getKindHelper());
1761 }
1762
1763 bool Term::isNull() const { return isNullHelper(); }
1764
1765 bool Term::isValue() const
1766 {
1767 CVC4_API_CHECK_NOT_NULL;
1768 return d_node->isConst();
1769 }
1770
1771 Term Term::getConstArrayBase() const
1772 {
1773 CVC4::ExprManagerScope exmgrs(*(d_solver->getExprManager()));
1774 CVC4_API_CHECK_NOT_NULL;
1775 // CONST_ARRAY kind maps to STORE_ALL internal kind
1776 CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::STORE_ALL)
1777 << "Expecting a CONST_ARRAY Term when calling getConstArrayBase()";
1778 return Term(d_solver, d_node->getConst<ArrayStoreAll>().getValue());
1779 }
1780
1781 std::vector<Term> Term::getConstSequenceElements() const
1782 {
1783 CVC4_API_CHECK_NOT_NULL;
1784 CVC4_API_CHECK(d_node->getKind() == CVC4::Kind::CONST_SEQUENCE)
1785 << "Expecting a CONST_SEQUENCE Term when calling "
1786 "getConstSequenceElements()";
1787 const std::vector<Node>& elems = d_node->getConst<Sequence>().getVec();
1788 std::vector<Term> terms;
1789 for (const Node& t : elems)
1790 {
1791 terms.push_back(Term(d_solver, t));
1792 }
1793 return terms;
1794 }
1795
1796 Term Term::notTerm() const
1797 {
1798 CVC4_API_CHECK_NOT_NULL;
1799 try
1800 {
1801 Node res = d_node->notNode();
1802 (void)res.getType(true); /* kick off type checking */
1803 return Term(d_solver, res);
1804 }
1805 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1806 {
1807 throw CVC4ApiException(e.getMessage());
1808 }
1809 }
1810
1811 Term Term::andTerm(const Term& t) const
1812 {
1813 CVC4_API_CHECK_NOT_NULL;
1814 CVC4_API_ARG_CHECK_NOT_NULL(t);
1815 try
1816 {
1817 Node res = d_node->andNode(*t.d_node);
1818 (void)res.getType(true); /* kick off type checking */
1819 return Term(d_solver, res);
1820 }
1821 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1822 {
1823 throw CVC4ApiException(e.getMessage());
1824 }
1825 }
1826
1827 Term Term::orTerm(const Term& t) const
1828 {
1829 CVC4_API_CHECK_NOT_NULL;
1830 CVC4_API_ARG_CHECK_NOT_NULL(t);
1831 try
1832 {
1833 Node res = d_node->orNode(*t.d_node);
1834 (void)res.getType(true); /* kick off type checking */
1835 return Term(d_solver, res);
1836 }
1837 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1838 {
1839 throw CVC4ApiException(e.getMessage());
1840 }
1841 }
1842
1843 Term Term::xorTerm(const Term& t) const
1844 {
1845 CVC4_API_CHECK_NOT_NULL;
1846 CVC4_API_ARG_CHECK_NOT_NULL(t);
1847 try
1848 {
1849 Node res = d_node->xorNode(*t.d_node);
1850 (void)res.getType(true); /* kick off type checking */
1851 return Term(d_solver, res);
1852 }
1853 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1854 {
1855 throw CVC4ApiException(e.getMessage());
1856 }
1857 }
1858
1859 Term Term::eqTerm(const Term& t) const
1860 {
1861 CVC4_API_CHECK_NOT_NULL;
1862 CVC4_API_ARG_CHECK_NOT_NULL(t);
1863 try
1864 {
1865 Node res = d_node->eqNode(*t.d_node);
1866 (void)res.getType(true); /* kick off type checking */
1867 return Term(d_solver, res);
1868 }
1869 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1870 {
1871 throw CVC4ApiException(e.getMessage());
1872 }
1873 }
1874
1875 Term Term::impTerm(const Term& t) const
1876 {
1877 CVC4_API_CHECK_NOT_NULL;
1878 CVC4_API_ARG_CHECK_NOT_NULL(t);
1879 try
1880 {
1881 Node res = d_node->impNode(*t.d_node);
1882 (void)res.getType(true); /* kick off type checking */
1883 return Term(d_solver, res);
1884 }
1885 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1886 {
1887 throw CVC4ApiException(e.getMessage());
1888 }
1889 }
1890
1891 Term Term::iteTerm(const Term& then_t, const Term& else_t) const
1892 {
1893 CVC4_API_CHECK_NOT_NULL;
1894 CVC4_API_ARG_CHECK_NOT_NULL(then_t);
1895 CVC4_API_ARG_CHECK_NOT_NULL(else_t);
1896 try
1897 {
1898 Node res = d_node->iteNode(*then_t.d_node, *else_t.d_node);
1899 (void)res.getType(true); /* kick off type checking */
1900 return Term(d_solver, res);
1901 }
1902 catch (const CVC4::TypeCheckingExceptionPrivate& e)
1903 {
1904 throw CVC4ApiException(e.getMessage());
1905 }
1906 }
1907
1908 std::string Term::toString() const
1909 {
1910 if (d_solver != nullptr)
1911 {
1912 NodeManagerScope scope(d_solver->getNodeManager());
1913 return d_node->toString();
1914 }
1915 return d_node->toString();
1916 }
1917
1918 Term::const_iterator::const_iterator()
1919 : d_solver(nullptr), d_origNode(nullptr), d_pos(0)
1920 {
1921 }
1922
1923 Term::const_iterator::const_iterator(const Solver* slv,
1924 const std::shared_ptr<CVC4::Node>& n,
1925 uint32_t p)
1926 : d_solver(slv), d_origNode(n), d_pos(p)
1927 {
1928 }
1929
1930 Term::const_iterator::const_iterator(const const_iterator& it)
1931 : d_solver(nullptr), d_origNode(nullptr)
1932 {
1933 if (it.d_origNode != nullptr)
1934 {
1935 d_solver = it.d_solver;
1936 d_origNode = it.d_origNode;
1937 d_pos = it.d_pos;
1938 }
1939 }
1940
1941 Term::const_iterator& Term::const_iterator::operator=(const const_iterator& it)
1942 {
1943 d_solver = it.d_solver;
1944 d_origNode = it.d_origNode;
1945 d_pos = it.d_pos;
1946 return *this;
1947 }
1948
1949 bool Term::const_iterator::operator==(const const_iterator& it) const
1950 {
1951 if (d_origNode == nullptr || it.d_origNode == nullptr)
1952 {
1953 return false;
1954 }
1955 return (d_solver == it.d_solver && *d_origNode == *it.d_origNode)
1956 && (d_pos == it.d_pos);
1957 }
1958
1959 bool Term::const_iterator::operator!=(const const_iterator& it) const
1960 {
1961 return !(*this == it);
1962 }
1963
1964 Term::const_iterator& Term::const_iterator::operator++()
1965 {
1966 Assert(d_origNode != nullptr);
1967 ++d_pos;
1968 return *this;
1969 }
1970
1971 Term::const_iterator Term::const_iterator::operator++(int)
1972 {
1973 Assert(d_origNode != nullptr);
1974 const_iterator it = *this;
1975 ++d_pos;
1976 return it;
1977 }
1978
1979 Term Term::const_iterator::operator*() const
1980 {
1981 Assert(d_origNode != nullptr);
1982 // this term has an extra child (mismatch between API and internal structure)
1983 // the extra child will be the first child
1984 bool extra_child = isApplyKind(d_origNode->getKind());
1985
1986 if (!d_pos && extra_child)
1987 {
1988 return Term(d_solver, d_origNode->getOperator());
1989 }
1990 else
1991 {
1992 uint32_t idx = d_pos;
1993 if (extra_child)
1994 {
1995 Assert(idx > 0);
1996 --idx;
1997 }
1998 Assert(idx >= 0);
1999 return Term(d_solver, (*d_origNode)[idx]);
2000 }
2001 }
2002
2003 Term::const_iterator Term::begin() const
2004 {
2005 return Term::const_iterator(d_solver, d_node, 0);
2006 }
2007
2008 Term::const_iterator Term::end() const
2009 {
2010 int endpos = d_node->getNumChildren();
2011 // special cases for APPLY_*
2012 // the API differs from the internal structure
2013 // the API takes a "higher-order" perspective and the applied
2014 // function or datatype constructor/selector/tester is a Term
2015 // which means it needs to be one of the children, even though
2016 // internally it is not
2017 if (isApplyKind(d_node->getKind()))
2018 {
2019 // one more child if this is a UF application (count the UF as a child)
2020 ++endpos;
2021 }
2022 return Term::const_iterator(d_solver, d_node, endpos);
2023 }
2024
2025 // !!! This is only temporarily available until the parser is fully migrated
2026 // to the new API. !!!
2027 CVC4::Expr Term::getExpr(void) const
2028 {
2029 if (d_node->isNull())
2030 {
2031 return Expr();
2032 }
2033 NodeManagerScope scope(d_solver->getNodeManager());
2034 return d_node->toExpr();
2035 }
2036
2037 // !!! This is only temporarily available until the parser is fully migrated
2038 // to the new API. !!!
2039 const CVC4::Node& Term::getNode(void) const { return *d_node; }
2040
2041 std::ostream& operator<<(std::ostream& out, const Term& t)
2042 {
2043 out << t.toString();
2044 return out;
2045 }
2046
2047 std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector)
2048 {
2049 container_to_stream(out, vector);
2050 return out;
2051 }
2052
2053 std::ostream& operator<<(std::ostream& out, const std::set<Term>& set)
2054 {
2055 container_to_stream(out, set);
2056 return out;
2057 }
2058
2059 std::ostream& operator<<(
2060 std::ostream& out,
2061 const std::unordered_set<Term, TermHashFunction>& unordered_set)
2062 {
2063 container_to_stream(out, unordered_set);
2064 return out;
2065 }
2066
2067 template <typename V>
2068 std::ostream& operator<<(std::ostream& out, const std::map<Term, V>& map)
2069 {
2070 container_to_stream(out, map);
2071 return out;
2072 }
2073
2074 template <typename V>
2075 std::ostream& operator<<(
2076 std::ostream& out,
2077 const std::unordered_map<Term, V, TermHashFunction>& unordered_map)
2078 {
2079 container_to_stream(out, unordered_map);
2080 return out;
2081 }
2082
2083 size_t TermHashFunction::operator()(const Term& t) const
2084 {
2085 return ExprHashFunction()(t.d_node->toExpr());
2086 }
2087
2088 /* -------------------------------------------------------------------------- */
2089 /* Datatypes */
2090 /* -------------------------------------------------------------------------- */
2091
2092 /* DatatypeConstructorDecl -------------------------------------------------- */
2093
2094 DatatypeConstructorDecl::DatatypeConstructorDecl()
2095 : d_solver(nullptr), d_ctor(nullptr)
2096 {
2097 }
2098
2099 DatatypeConstructorDecl::DatatypeConstructorDecl(const Solver* slv,
2100 const std::string& name)
2101 : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(name))
2102 {
2103 }
2104 DatatypeConstructorDecl::~DatatypeConstructorDecl()
2105 {
2106 if (d_ctor != nullptr)
2107 {
2108 // ensure proper node manager is in scope
2109 NodeManagerScope scope(d_solver->getNodeManager());
2110 d_ctor.reset();
2111 }
2112 }
2113
2114 void DatatypeConstructorDecl::addSelector(const std::string& name, Sort sort)
2115 {
2116 NodeManagerScope scope(d_solver->getNodeManager());
2117 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort)
2118 << "non-null range sort for selector";
2119 d_ctor->addArg(name, TypeNode::fromType(*sort.d_type));
2120 }
2121
2122 void DatatypeConstructorDecl::addSelectorSelf(const std::string& name)
2123 {
2124 NodeManagerScope scope(d_solver->getNodeManager());
2125 d_ctor->addArgSelf(name);
2126 }
2127
2128 std::string DatatypeConstructorDecl::toString() const
2129 {
2130 std::stringstream ss;
2131 ss << *d_ctor;
2132 return ss.str();
2133 }
2134
2135 // !!! This is only temporarily available until the parser is fully migrated
2136 // to the new API. !!!
2137 const CVC4::DTypeConstructor& DatatypeConstructorDecl::getDatatypeConstructor(
2138 void) const
2139 {
2140 return *d_ctor;
2141 }
2142
2143 std::ostream& operator<<(std::ostream& out,
2144 const DatatypeConstructorDecl& ctordecl)
2145 {
2146 out << ctordecl.toString();
2147 return out;
2148 }
2149
2150 std::ostream& operator<<(std::ostream& out,
2151 const std::vector<DatatypeConstructorDecl>& vector)
2152 {
2153 container_to_stream(out, vector);
2154 return out;
2155 }
2156
2157 /* DatatypeDecl ------------------------------------------------------------- */
2158
2159 DatatypeDecl::DatatypeDecl() : d_solver(nullptr), d_dtype(nullptr) {}
2160
2161 DatatypeDecl::DatatypeDecl(const Solver* slv,
2162 const std::string& name,
2163 bool isCoDatatype)
2164 : d_solver(slv), d_dtype(new CVC4::DType(name, isCoDatatype))
2165 {
2166 }
2167
2168 DatatypeDecl::DatatypeDecl(const Solver* slv,
2169 const std::string& name,
2170 Sort param,
2171 bool isCoDatatype)
2172 : d_solver(slv),
2173 d_dtype(new CVC4::DType(
2174 name,
2175 std::vector<TypeNode>{TypeNode::fromType(*param.d_type)},
2176 isCoDatatype))
2177 {
2178 }
2179
2180 DatatypeDecl::DatatypeDecl(const Solver* slv,
2181 const std::string& name,
2182 const std::vector<Sort>& params,
2183 bool isCoDatatype)
2184 : d_solver(slv)
2185 {
2186 std::vector<TypeNode> tparams;
2187 for (const Sort& p : params)
2188 {
2189 tparams.push_back(TypeNode::fromType(*p.d_type));
2190 }
2191 d_dtype = std::shared_ptr<CVC4::DType>(
2192 new CVC4::DType(name, tparams, isCoDatatype));
2193 }
2194
2195 bool DatatypeDecl::isNullHelper() const { return !d_dtype; }
2196
2197 DatatypeDecl::~DatatypeDecl()
2198 {
2199 if (d_dtype != nullptr)
2200 {
2201 // ensure proper node manager is in scope
2202 NodeManagerScope scope(d_solver->getNodeManager());
2203 d_dtype.reset();
2204 }
2205 }
2206
2207 void DatatypeDecl::addConstructor(const DatatypeConstructorDecl& ctor)
2208 {
2209 NodeManagerScope scope(d_solver->getNodeManager());
2210 CVC4_API_CHECK_NOT_NULL;
2211 d_dtype->addConstructor(ctor.d_ctor);
2212 }
2213
2214 size_t DatatypeDecl::getNumConstructors() const
2215 {
2216 CVC4_API_CHECK_NOT_NULL;
2217 return d_dtype->getNumConstructors();
2218 }
2219
2220 bool DatatypeDecl::isParametric() const
2221 {
2222 CVC4_API_CHECK_NOT_NULL;
2223 return d_dtype->isParametric();
2224 }
2225
2226 std::string DatatypeDecl::toString() const
2227 {
2228 CVC4_API_CHECK_NOT_NULL;
2229 std::stringstream ss;
2230 ss << *d_dtype;
2231 return ss.str();
2232 }
2233
2234 std::string DatatypeDecl::getName() const
2235 {
2236 CVC4_API_CHECK_NOT_NULL;
2237 return d_dtype->getName();
2238 }
2239
2240 bool DatatypeDecl::isNull() const { return isNullHelper(); }
2241
2242 // !!! This is only temporarily available until the parser is fully migrated
2243 // to the new API. !!!
2244 CVC4::DType& DatatypeDecl::getDatatype(void) const { return *d_dtype; }
2245
2246 std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl)
2247 {
2248 out << dtdecl.toString();
2249 return out;
2250 }
2251
2252 /* DatatypeSelector --------------------------------------------------------- */
2253
2254 DatatypeSelector::DatatypeSelector() : d_solver(nullptr), d_stor(nullptr) {}
2255
2256 DatatypeSelector::DatatypeSelector(const Solver* slv,
2257 const CVC4::DTypeSelector& stor)
2258 : d_solver(slv), d_stor(new CVC4::DTypeSelector(stor))
2259 {
2260 CVC4_API_CHECK(d_stor->isResolved()) << "Expected resolved datatype selector";
2261 }
2262
2263 DatatypeSelector::~DatatypeSelector()
2264 {
2265 if (d_stor != nullptr)
2266 {
2267 // ensure proper node manager is in scope
2268 NodeManagerScope scope(d_solver->getNodeManager());
2269 d_stor.reset();
2270 }
2271 }
2272
2273 std::string DatatypeSelector::getName() const { return d_stor->getName(); }
2274
2275 Term DatatypeSelector::getSelectorTerm() const
2276 {
2277 Term sel = Term(d_solver, d_stor->getSelector());
2278 return sel;
2279 }
2280
2281 Sort DatatypeSelector::getRangeSort() const
2282 {
2283 return Sort(d_solver, d_stor->getRangeType().toType());
2284 }
2285
2286 std::string DatatypeSelector::toString() const
2287 {
2288 std::stringstream ss;
2289 ss << *d_stor;
2290 return ss.str();
2291 }
2292
2293 // !!! This is only temporarily available until the parser is fully migrated
2294 // to the new API. !!!
2295 CVC4::DTypeSelector DatatypeSelector::getDatatypeConstructorArg(void) const
2296 {
2297 return *d_stor;
2298 }
2299
2300 std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor)
2301 {
2302 out << stor.toString();
2303 return out;
2304 }
2305
2306 /* DatatypeConstructor ------------------------------------------------------ */
2307
2308 DatatypeConstructor::DatatypeConstructor() : d_solver(nullptr), d_ctor(nullptr)
2309 {
2310 }
2311
2312 DatatypeConstructor::DatatypeConstructor(const Solver* slv,
2313 const CVC4::DTypeConstructor& ctor)
2314 : d_solver(slv), d_ctor(new CVC4::DTypeConstructor(ctor))
2315 {
2316 CVC4_API_CHECK(d_ctor->isResolved())
2317 << "Expected resolved datatype constructor";
2318 }
2319
2320 DatatypeConstructor::~DatatypeConstructor()
2321 {
2322 if (d_ctor != nullptr)
2323 {
2324 // ensure proper node manager is in scope
2325 NodeManagerScope scope(d_solver->getNodeManager());
2326 d_ctor.reset();
2327 }
2328 }
2329
2330 std::string DatatypeConstructor::getName() const { return d_ctor->getName(); }
2331
2332 Term DatatypeConstructor::getConstructorTerm() const
2333 {
2334 Term ctor = Term(d_solver, d_ctor->getConstructor());
2335 return ctor;
2336 }
2337
2338 Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const
2339 {
2340 NodeManagerScope scope(d_solver->getNodeManager());
2341 CVC4_API_CHECK(d_ctor->isResolved())
2342 << "Expected resolved datatype constructor";
2343 CVC4_API_CHECK(retSort.isDatatype())
2344 << "Cannot get specialized constructor type for non-datatype type "
2345 << retSort;
2346 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
2347
2348 NodeManager* nm = d_solver->getNodeManager();
2349 Node ret = nm->mkNode(
2350 kind::APPLY_TYPE_ASCRIPTION,
2351 nm->mkConst(AscriptionType(d_ctor
2352 ->getSpecializedConstructorType(
2353 TypeNode::fromType(retSort.getType()))
2354 .toType())),
2355 d_ctor->getConstructor());
2356 (void)ret.getType(true); /* kick off type checking */
2357 // apply type ascription to the operator
2358 Term sctor = api::Term(d_solver, ret);
2359 return sctor;
2360
2361 CVC4_API_SOLVER_TRY_CATCH_END;
2362 }
2363
2364 Term DatatypeConstructor::getTesterTerm() const
2365 {
2366 Term tst = Term(d_solver, d_ctor->getTester());
2367 return tst;
2368 }
2369
2370 size_t DatatypeConstructor::getNumSelectors() const
2371 {
2372 return d_ctor->getNumArgs();
2373 }
2374
2375 DatatypeSelector DatatypeConstructor::operator[](size_t index) const
2376 {
2377 return DatatypeSelector(d_solver, (*d_ctor)[index]);
2378 }
2379
2380 DatatypeSelector DatatypeConstructor::operator[](const std::string& name) const
2381 {
2382 return getSelectorForName(name);
2383 }
2384
2385 DatatypeSelector DatatypeConstructor::getSelector(const std::string& name) const
2386 {
2387 return getSelectorForName(name);
2388 }
2389
2390 Term DatatypeConstructor::getSelectorTerm(const std::string& name) const
2391 {
2392 DatatypeSelector sel = getSelector(name);
2393 return sel.getSelectorTerm();
2394 }
2395
2396 DatatypeConstructor::const_iterator DatatypeConstructor::begin() const
2397 {
2398 return DatatypeConstructor::const_iterator(d_solver, *d_ctor, true);
2399 }
2400
2401 DatatypeConstructor::const_iterator DatatypeConstructor::end() const
2402 {
2403 return DatatypeConstructor::const_iterator(d_solver, *d_ctor, false);
2404 }
2405
2406 DatatypeConstructor::const_iterator::const_iterator(
2407 const Solver* slv, const CVC4::DTypeConstructor& ctor, bool begin)
2408 {
2409 d_solver = slv;
2410 d_int_stors = &ctor.getArgs();
2411
2412 const std::vector<std::shared_ptr<CVC4::DTypeSelector>>& sels =
2413 ctor.getArgs();
2414 for (const std::shared_ptr<CVC4::DTypeSelector>& s : sels)
2415 {
2416 /* Can not use emplace_back here since constructor is private. */
2417 d_stors.push_back(DatatypeSelector(d_solver, *s.get()));
2418 }
2419 d_idx = begin ? 0 : sels.size();
2420 }
2421
2422 DatatypeConstructor::const_iterator::const_iterator()
2423 : d_solver(nullptr), d_int_stors(nullptr), d_idx(0)
2424 {
2425 }
2426
2427 DatatypeConstructor::const_iterator&
2428 DatatypeConstructor::const_iterator::operator=(
2429 const DatatypeConstructor::const_iterator& it)
2430 {
2431 d_solver = it.d_solver;
2432 d_int_stors = it.d_int_stors;
2433 d_stors = it.d_stors;
2434 d_idx = it.d_idx;
2435 return *this;
2436 }
2437
2438 const DatatypeSelector& DatatypeConstructor::const_iterator::operator*() const
2439 {
2440 return d_stors[d_idx];
2441 }
2442
2443 const DatatypeSelector* DatatypeConstructor::const_iterator::operator->() const
2444 {
2445 return &d_stors[d_idx];
2446 }
2447
2448 DatatypeConstructor::const_iterator&
2449 DatatypeConstructor::const_iterator::operator++()
2450 {
2451 ++d_idx;
2452 return *this;
2453 }
2454
2455 DatatypeConstructor::const_iterator
2456 DatatypeConstructor::const_iterator::operator++(int)
2457 {
2458 DatatypeConstructor::const_iterator it(*this);
2459 ++d_idx;
2460 return it;
2461 }
2462
2463 bool DatatypeConstructor::const_iterator::operator==(
2464 const DatatypeConstructor::const_iterator& other) const
2465 {
2466 return d_int_stors == other.d_int_stors && d_idx == other.d_idx;
2467 }
2468
2469 bool DatatypeConstructor::const_iterator::operator!=(
2470 const DatatypeConstructor::const_iterator& other) const
2471 {
2472 return d_int_stors != other.d_int_stors || d_idx != other.d_idx;
2473 }
2474
2475 std::string DatatypeConstructor::toString() const
2476 {
2477 std::stringstream ss;
2478 ss << *d_ctor;
2479 return ss.str();
2480 }
2481
2482 // !!! This is only temporarily available until the parser is fully migrated
2483 // to the new API. !!!
2484 const CVC4::DTypeConstructor& DatatypeConstructor::getDatatypeConstructor(
2485 void) const
2486 {
2487 return *d_ctor;
2488 }
2489
2490 DatatypeSelector DatatypeConstructor::getSelectorForName(
2491 const std::string& name) const
2492 {
2493 bool foundSel = false;
2494 size_t index = 0;
2495 for (size_t i = 0, nsels = getNumSelectors(); i < nsels; i++)
2496 {
2497 if ((*d_ctor)[i].getName() == name)
2498 {
2499 index = i;
2500 foundSel = true;
2501 break;
2502 }
2503 }
2504 if (!foundSel)
2505 {
2506 std::stringstream snames;
2507 snames << "{ ";
2508 for (size_t i = 0, ncons = getNumSelectors(); i < ncons; i++)
2509 {
2510 snames << (*d_ctor)[i].getName() << " ";
2511 }
2512 snames << "} ";
2513 CVC4_API_CHECK(foundSel) << "No selector " << name << " for constructor "
2514 << getName() << " exists among " << snames.str();
2515 }
2516 return DatatypeSelector(d_solver, (*d_ctor)[index]);
2517 }
2518
2519 std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor)
2520 {
2521 out << ctor.toString();
2522 return out;
2523 }
2524
2525 /* Datatype ----------------------------------------------------------------- */
2526
2527 Datatype::Datatype(const Solver* slv, const CVC4::DType& dtype)
2528 : d_solver(slv), d_dtype(new CVC4::DType(dtype))
2529 {
2530 CVC4_API_CHECK(d_dtype->isResolved()) << "Expected resolved datatype";
2531 }
2532
2533 Datatype::Datatype() : d_solver(nullptr), d_dtype(nullptr) {}
2534
2535 Datatype::~Datatype()
2536 {
2537 if (d_dtype != nullptr)
2538 {
2539 // ensure proper node manager is in scope
2540 NodeManagerScope scope(d_solver->getNodeManager());
2541 d_dtype.reset();
2542 }
2543 }
2544
2545 DatatypeConstructor Datatype::operator[](size_t idx) const
2546 {
2547 CVC4_API_CHECK(idx < getNumConstructors()) << "Index out of bounds.";
2548 return DatatypeConstructor(d_solver, (*d_dtype)[idx]);
2549 }
2550
2551 DatatypeConstructor Datatype::operator[](const std::string& name) const
2552 {
2553 return getConstructorForName(name);
2554 }
2555
2556 DatatypeConstructor Datatype::getConstructor(const std::string& name) const
2557 {
2558 return getConstructorForName(name);
2559 }
2560
2561 Term Datatype::getConstructorTerm(const std::string& name) const
2562 {
2563 DatatypeConstructor ctor = getConstructor(name);
2564 return ctor.getConstructorTerm();
2565 }
2566
2567 std::string Datatype::getName() const { return d_dtype->getName(); }
2568
2569 size_t Datatype::getNumConstructors() const
2570 {
2571 return d_dtype->getNumConstructors();
2572 }
2573
2574 bool Datatype::isParametric() const { return d_dtype->isParametric(); }
2575 bool Datatype::isCodatatype() const { return d_dtype->isCodatatype(); }
2576
2577 bool Datatype::isTuple() const { return d_dtype->isTuple(); }
2578
2579 bool Datatype::isRecord() const { return d_dtype->isRecord(); }
2580
2581 bool Datatype::isFinite() const { return d_dtype->isFinite(); }
2582 bool Datatype::isWellFounded() const { return d_dtype->isWellFounded(); }
2583 bool Datatype::hasNestedRecursion() const
2584 {
2585 return d_dtype->hasNestedRecursion();
2586 }
2587
2588 std::string Datatype::toString() const { return d_dtype->getName(); }
2589
2590 Datatype::const_iterator Datatype::begin() const
2591 {
2592 return Datatype::const_iterator(d_solver, *d_dtype, true);
2593 }
2594
2595 Datatype::const_iterator Datatype::end() const
2596 {
2597 return Datatype::const_iterator(d_solver, *d_dtype, false);
2598 }
2599
2600 // !!! This is only temporarily available until the parser is fully migrated
2601 // to the new API. !!!
2602 const CVC4::DType& Datatype::getDatatype(void) const { return *d_dtype; }
2603
2604 DatatypeConstructor Datatype::getConstructorForName(
2605 const std::string& name) const
2606 {
2607 bool foundCons = false;
2608 size_t index = 0;
2609 for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
2610 {
2611 if ((*d_dtype)[i].getName() == name)
2612 {
2613 index = i;
2614 foundCons = true;
2615 break;
2616 }
2617 }
2618 if (!foundCons)
2619 {
2620 std::stringstream snames;
2621 snames << "{ ";
2622 for (size_t i = 0, ncons = getNumConstructors(); i < ncons; i++)
2623 {
2624 snames << (*d_dtype)[i].getName() << " ";
2625 }
2626 snames << "}";
2627 CVC4_API_CHECK(foundCons) << "No constructor " << name << " for datatype "
2628 << getName() << " exists, among " << snames.str();
2629 }
2630 return DatatypeConstructor(d_solver, (*d_dtype)[index]);
2631 }
2632
2633 Datatype::const_iterator::const_iterator(const Solver* slv,
2634 const CVC4::DType& dtype,
2635 bool begin)
2636 : d_solver(slv), d_int_ctors(&dtype.getConstructors())
2637 {
2638 const std::vector<std::shared_ptr<DTypeConstructor>>& cons =
2639 dtype.getConstructors();
2640 for (const std::shared_ptr<DTypeConstructor>& c : cons)
2641 {
2642 /* Can not use emplace_back here since constructor is private. */
2643 d_ctors.push_back(DatatypeConstructor(d_solver, *c.get()));
2644 }
2645 d_idx = begin ? 0 : cons.size();
2646 }
2647
2648 Datatype::const_iterator::const_iterator()
2649 : d_solver(nullptr), d_int_ctors(nullptr), d_idx(0)
2650 {
2651 }
2652
2653 Datatype::const_iterator& Datatype::const_iterator::operator=(
2654 const Datatype::const_iterator& it)
2655 {
2656 d_solver = it.d_solver;
2657 d_int_ctors = it.d_int_ctors;
2658 d_ctors = it.d_ctors;
2659 d_idx = it.d_idx;
2660 return *this;
2661 }
2662
2663 const DatatypeConstructor& Datatype::const_iterator::operator*() const
2664 {
2665 return d_ctors[d_idx];
2666 }
2667
2668 const DatatypeConstructor* Datatype::const_iterator::operator->() const
2669 {
2670 return &d_ctors[d_idx];
2671 }
2672
2673 Datatype::const_iterator& Datatype::const_iterator::operator++()
2674 {
2675 ++d_idx;
2676 return *this;
2677 }
2678
2679 Datatype::const_iterator Datatype::const_iterator::operator++(int)
2680 {
2681 Datatype::const_iterator it(*this);
2682 ++d_idx;
2683 return it;
2684 }
2685
2686 bool Datatype::const_iterator::operator==(
2687 const Datatype::const_iterator& other) const
2688 {
2689 return d_int_ctors == other.d_int_ctors && d_idx == other.d_idx;
2690 }
2691
2692 bool Datatype::const_iterator::operator!=(
2693 const Datatype::const_iterator& other) const
2694 {
2695 return d_int_ctors != other.d_int_ctors || d_idx != other.d_idx;
2696 }
2697
2698 /* -------------------------------------------------------------------------- */
2699 /* Grammar */
2700 /* -------------------------------------------------------------------------- */
2701
2702 Grammar::Grammar()
2703 : d_solver(nullptr),
2704 d_sygusVars(),
2705 d_ntSyms(),
2706 d_ntsToTerms(0),
2707 d_allowConst(),
2708 d_allowVars(),
2709 d_isResolved(false)
2710 {
2711 }
2712
2713 Grammar::Grammar(const Solver* slv,
2714 const std::vector<Term>& sygusVars,
2715 const std::vector<Term>& ntSymbols)
2716 : d_solver(slv),
2717 d_sygusVars(sygusVars),
2718 d_ntSyms(ntSymbols),
2719 d_ntsToTerms(ntSymbols.size()),
2720 d_allowConst(),
2721 d_allowVars(),
2722 d_isResolved(false)
2723 {
2724 for (Term ntsymbol : d_ntSyms)
2725 {
2726 d_ntsToTerms.emplace(ntsymbol, std::vector<Term>());
2727 }
2728 }
2729
2730 void Grammar::addRule(Term ntSymbol, Term rule)
2731 {
2732 CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
2733 "it as an argument to synthFun/synthInv";
2734 CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
2735 CVC4_API_ARG_CHECK_NOT_NULL(rule);
2736 CVC4_API_ARG_CHECK_EXPECTED(
2737 d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
2738 << "ntSymbol to be one of the non-terminal symbols given in the "
2739 "predeclaration";
2740 CVC4_API_CHECK(ntSymbol.d_node->getType() == rule.d_node->getType())
2741 << "Expected ntSymbol and rule to have the same sort";
2742
2743 d_ntsToTerms[ntSymbol].push_back(rule);
2744 }
2745
2746 void Grammar::addRules(Term ntSymbol, std::vector<Term> rules)
2747 {
2748 CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
2749 "it as an argument to synthFun/synthInv";
2750 CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
2751 CVC4_API_ARG_CHECK_EXPECTED(
2752 d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
2753 << "ntSymbol to be one of the non-terminal symbols given in the "
2754 "predeclaration";
2755
2756 for (size_t i = 0, n = rules.size(); i < n; ++i)
2757 {
2758 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
2759 !rules[i].isNull(), "parameter rule", rules[i], i)
2760 << "non-null term";
2761 CVC4_API_CHECK(ntSymbol.d_node->getType() == rules[i].d_node->getType())
2762 << "Expected ntSymbol and rule at index " << i
2763 << " to have the same sort";
2764 }
2765
2766 d_ntsToTerms[ntSymbol].insert(
2767 d_ntsToTerms[ntSymbol].cend(), rules.cbegin(), rules.cend());
2768 }
2769
2770 void Grammar::addAnyConstant(Term ntSymbol)
2771 {
2772 CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
2773 "it as an argument to synthFun/synthInv";
2774 CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
2775 CVC4_API_ARG_CHECK_EXPECTED(
2776 d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
2777 << "ntSymbol to be one of the non-terminal symbols given in the "
2778 "predeclaration";
2779
2780 d_allowConst.insert(ntSymbol);
2781 }
2782
2783 void Grammar::addAnyVariable(Term ntSymbol)
2784 {
2785 CVC4_API_CHECK(!d_isResolved) << "Grammar cannot be modified after passing "
2786 "it as an argument to synthFun/synthInv";
2787 CVC4_API_ARG_CHECK_NOT_NULL(ntSymbol);
2788 CVC4_API_ARG_CHECK_EXPECTED(
2789 d_ntsToTerms.find(ntSymbol) != d_ntsToTerms.cend(), ntSymbol)
2790 << "ntSymbol to be one of the non-terminal symbols given in the "
2791 "predeclaration";
2792
2793 d_allowVars.insert(ntSymbol);
2794 }
2795
2796 /**
2797 * this function concatinates the outputs of calling f on each element between
2798 * first and last, seperated by sep.
2799 * @param first the beginning of the range
2800 * @param last the end of the range
2801 * @param f the function to call on each element in the range, its output must
2802 * be overloaded for operator<<
2803 * @param sep the string to add between successive calls to f
2804 */
2805 template <typename Iterator, typename Function>
2806 std::string join(Iterator first, Iterator last, Function f, std::string sep)
2807 {
2808 std::stringstream ss;
2809 Iterator i = first;
2810
2811 if (i != last)
2812 {
2813 ss << f(*i);
2814 ++i;
2815 }
2816
2817 while (i != last)
2818 {
2819 ss << sep << f(*i);
2820 ++i;
2821 }
2822
2823 return ss.str();
2824 }
2825
2826 std::string Grammar::toString() const
2827 {
2828 std::stringstream ss;
2829 ss << " (" // pre-declaration
2830 << join(
2831 d_ntSyms.cbegin(),
2832 d_ntSyms.cend(),
2833 [](const Term& t) {
2834 std::stringstream s;
2835 s << '(' << t << ' ' << t.getSort() << ')';
2836 return s.str();
2837 },
2838 " ")
2839 << ")\n (" // grouped rule listing
2840 << join(
2841 d_ntSyms.cbegin(),
2842 d_ntSyms.cend(),
2843 [this](const Term& t) {
2844 bool allowConst = d_allowConst.find(t) != d_allowConst.cend(),
2845 allowVars = d_allowVars.find(t) != d_allowVars.cend();
2846 const std::vector<Term>& rules = d_ntsToTerms.at(t);
2847 std::stringstream s;
2848 s << '(' << t << ' ' << t.getSort() << " ("
2849 << (allowConst ? "(Constant " + t.getSort().toString() + ")"
2850 : "")
2851 << (allowConst && allowVars ? " " : "")
2852 << (allowVars ? "(Var " + t.getSort().toString() + ")" : "")
2853 << ((allowConst || allowVars) && !rules.empty() ? " " : "")
2854 << join(
2855 rules.cbegin(),
2856 rules.cend(),
2857 [](const Term& rule) { return rule.toString(); },
2858 " ")
2859 << "))";
2860 return s.str();
2861 },
2862 "\n ")
2863 << ')';
2864
2865 return ss.str();
2866 }
2867
2868 Sort Grammar::resolve()
2869 {
2870 d_isResolved = true;
2871
2872 Term bvl;
2873
2874 if (!d_sygusVars.empty())
2875 {
2876 bvl = Term(d_solver,
2877 d_solver->getExprManager()->mkExpr(
2878 CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(d_sygusVars)));
2879 }
2880
2881 std::unordered_map<Term, Sort, TermHashFunction> ntsToUnres(d_ntSyms.size());
2882
2883 for (Term ntsymbol : d_ntSyms)
2884 {
2885 // make the unresolved type, used for referencing the final version of
2886 // the ntsymbol's datatype
2887 ntsToUnres[ntsymbol] =
2888 Sort(d_solver, d_solver->getExprManager()->mkSort(ntsymbol.toString()));
2889 }
2890
2891 std::vector<CVC4::DType> datatypes;
2892 std::set<TypeNode> unresTypes;
2893
2894 datatypes.reserve(d_ntSyms.size());
2895
2896 for (const Term& ntSym : d_ntSyms)
2897 {
2898 // make the datatype, which encodes terms generated by this non-terminal
2899 DatatypeDecl dtDecl(d_solver, ntSym.toString());
2900
2901 for (const Term& consTerm : d_ntsToTerms[ntSym])
2902 {
2903 addSygusConstructorTerm(dtDecl, consTerm, ntsToUnres);
2904 }
2905
2906 if (d_allowVars.find(ntSym) != d_allowVars.cend())
2907 {
2908 addSygusConstructorVariables(
2909 dtDecl, Sort(d_solver, ntSym.d_node->getType().toType()));
2910 }
2911
2912 bool aci = d_allowConst.find(ntSym) != d_allowConst.end();
2913 TypeNode btt = ntSym.d_node->getType();
2914 dtDecl.d_dtype->setSygus(btt, *bvl.d_node, aci, false);
2915
2916 // We can be in a case where the only rule specified was (Variable T)
2917 // and there are no variables of type T, in which case this is a bogus
2918 // grammar. This results in the error below.
2919 CVC4_API_CHECK(dtDecl.d_dtype->getNumConstructors() != 0)
2920 << "Grouped rule listing for " << *dtDecl.d_dtype
2921 << " produced an empty rule list";
2922
2923 datatypes.push_back(*dtDecl.d_dtype);
2924 unresTypes.insert(TypeNode::fromType(*ntsToUnres[ntSym].d_type));
2925 }
2926
2927 std::vector<TypeNode> datatypeTypes =
2928 d_solver->getNodeManager()->mkMutualDatatypeTypes(
2929 datatypes, unresTypes, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
2930
2931 // return is the first datatype
2932 return Sort(d_solver, datatypeTypes[0].toType());
2933 }
2934
2935 void Grammar::addSygusConstructorTerm(
2936 DatatypeDecl& dt,
2937 Term term,
2938 const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
2939 {
2940 // At this point, we should know that dt is well founded, and that its
2941 // builtin sygus operators are well-typed.
2942 // Now, purify each occurrence of a non-terminal symbol in term, replace by
2943 // free variables. These become arguments to constructors. Notice we must do
2944 // a tree traversal in this function, since unique paths to the same term
2945 // should be treated as distinct terms.
2946 // Notice that let expressions are forbidden in the input syntax of term, so
2947 // this does not lead to exponential behavior with respect to input size.
2948 std::vector<Term> args;
2949 std::vector<Sort> cargs;
2950 Term op = purifySygusGTerm(term, args, cargs, ntsToUnres);
2951 std::stringstream ssCName;
2952 ssCName << op.getKind();
2953 if (!args.empty())
2954 {
2955 Term lbvl = Term(d_solver,
2956 d_solver->getExprManager()->mkExpr(
2957 CVC4::kind::BOUND_VAR_LIST, termVectorToExprs(args)));
2958 // its operator is a lambda
2959 op = Term(
2960 d_solver,
2961 d_solver->getExprManager()->mkExpr(
2962 CVC4::kind::LAMBDA, {lbvl.d_node->toExpr(), op.d_node->toExpr()}));
2963 }
2964 std::vector<TypeNode> cargst;
2965 for (const Sort& s : cargs)
2966 {
2967 cargst.push_back(TypeNode::fromType(s.getType()));
2968 }
2969 dt.d_dtype->addSygusConstructor(*op.d_node, ssCName.str(), cargst);
2970 }
2971
2972 Term Grammar::purifySygusGTerm(
2973 Term term,
2974 std::vector<Term>& args,
2975 std::vector<Sort>& cargs,
2976 const std::unordered_map<Term, Sort, TermHashFunction>& ntsToUnres) const
2977 {
2978 std::unordered_map<Term, Sort, TermHashFunction>::const_iterator itn =
2979 ntsToUnres.find(term);
2980 if (itn != ntsToUnres.cend())
2981 {
2982 Term ret =
2983 Term(d_solver,
2984 d_solver->getNodeManager()->mkBoundVar(term.d_node->getType()));
2985 args.push_back(ret);
2986 cargs.push_back(itn->second);
2987 return ret;
2988 }
2989 std::vector<Term> pchildren;
2990 bool childChanged = false;
2991 for (unsigned i = 0, nchild = term.d_node->getNumChildren(); i < nchild; i++)
2992 {
2993 Term ptermc = purifySygusGTerm(
2994 Term(d_solver, (*term.d_node)[i]), args, cargs, ntsToUnres);
2995 pchildren.push_back(ptermc);
2996 childChanged =
2997 childChanged || ptermc.d_node->toExpr() != (term.d_node->toExpr())[i];
2998 }
2999 if (!childChanged)
3000 {
3001 return term;
3002 }
3003
3004 Node nret;
3005
3006 if (term.d_node->getMetaKind() == kind::metakind::PARAMETERIZED)
3007 {
3008 // it's an indexed operator so we should provide the op
3009 NodeBuilder<> nb(term.d_node->getKind());
3010 nb << term.d_node->getOperator();
3011 nb.append(termVectorToNodes(pchildren));
3012 nret = nb.constructNode();
3013 }
3014 else
3015 {
3016 nret = d_solver->getNodeManager()->mkNode(term.d_node->getKind(),
3017 termVectorToNodes(pchildren));
3018 }
3019
3020 return Term(d_solver, nret);
3021 }
3022
3023 void Grammar::addSygusConstructorVariables(DatatypeDecl& dt, Sort sort) const
3024 {
3025 Assert(!sort.isNull());
3026 // each variable of appropriate type becomes a sygus constructor in dt.
3027 for (unsigned i = 0, size = d_sygusVars.size(); i < size; i++)
3028 {
3029 Term v = d_sygusVars[i];
3030 if (v.d_node->getType().toType() == *sort.d_type)
3031 {
3032 std::stringstream ss;
3033 ss << v;
3034 std::vector<TypeNode> cargs;
3035 dt.d_dtype->addSygusConstructor(*v.d_node, ss.str(), cargs);
3036 }
3037 }
3038 }
3039
3040 std::ostream& operator<<(std::ostream& out, const Grammar& g)
3041 {
3042 return out << g.toString();
3043 }
3044
3045 /* -------------------------------------------------------------------------- */
3046 /* Rounding Mode for Floating Points */
3047 /* -------------------------------------------------------------------------- */
3048
3049 const static std::
3050 unordered_map<RoundingMode, CVC4::RoundingMode, RoundingModeHashFunction>
3051 s_rmodes{
3052 {ROUND_NEAREST_TIES_TO_EVEN,
3053 CVC4::RoundingMode::roundNearestTiesToEven},
3054 {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::roundTowardPositive},
3055 {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::roundTowardNegative},
3056 {ROUND_TOWARD_ZERO, CVC4::RoundingMode::roundTowardZero},
3057 {ROUND_NEAREST_TIES_TO_AWAY,
3058 CVC4::RoundingMode::roundNearestTiesToAway},
3059 };
3060
3061 const static std::unordered_map<CVC4::RoundingMode,
3062 RoundingMode,
3063 CVC4::RoundingModeHashFunction>
3064 s_rmodes_internal{
3065 {CVC4::RoundingMode::roundNearestTiesToEven,
3066 ROUND_NEAREST_TIES_TO_EVEN},
3067 {CVC4::RoundingMode::roundTowardPositive, ROUND_TOWARD_POSITIVE},
3068 {CVC4::RoundingMode::roundTowardNegative, ROUND_TOWARD_NEGATIVE},
3069 {CVC4::RoundingMode::roundTowardZero, ROUND_TOWARD_ZERO},
3070 {CVC4::RoundingMode::roundNearestTiesToAway,
3071 ROUND_NEAREST_TIES_TO_AWAY},
3072 };
3073
3074 size_t RoundingModeHashFunction::operator()(const RoundingMode& rm) const
3075 {
3076 return size_t(rm);
3077 }
3078
3079 /* -------------------------------------------------------------------------- */
3080 /* Solver */
3081 /* -------------------------------------------------------------------------- */
3082
3083 Solver::Solver(Options* opts)
3084 {
3085 d_exprMgr.reset(new ExprManager);
3086 d_smtEngine.reset(new SmtEngine(d_exprMgr.get(), opts));
3087 d_smtEngine->setSolver(this);
3088 Options& o = d_smtEngine->getOptions();
3089 d_rng.reset(new Random(o[options::seed]));
3090 }
3091
3092 Solver::~Solver() {}
3093
3094 /* Helpers */
3095 /* -------------------------------------------------------------------------- */
3096
3097 /* Split out to avoid nested API calls (problematic with API tracing). */
3098 /* .......................................................................... */
3099
3100 template <typename T>
3101 Term Solver::mkValHelper(T t) const
3102 {
3103 NodeManagerScope scope(getNodeManager());
3104 Node res = getNodeManager()->mkConst(t);
3105 (void)res.getType(true); /* kick off type checking */
3106 return Term(this, res);
3107 }
3108
3109 Term Solver::mkRealFromStrHelper(const std::string& s) const
3110 {
3111 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
3112 * throws an std::invalid_argument exception. For consistency, we treat it
3113 * as invalid. */
3114 CVC4_API_ARG_CHECK_EXPECTED(s != ".", s)
3115 << "a string representing an integer, real or rational value.";
3116
3117 CVC4::Rational r = s.find('/') != std::string::npos
3118 ? CVC4::Rational(s)
3119 : CVC4::Rational::fromDecimal(s);
3120 return mkValHelper<CVC4::Rational>(r);
3121 }
3122
3123 Term Solver::mkBVFromIntHelper(uint32_t size, uint64_t val) const
3124 {
3125 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3126 CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "a bit-width > 0";
3127
3128 return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
3129
3130 CVC4_API_SOLVER_TRY_CATCH_END;
3131 }
3132
3133 Term Solver::mkBVFromStrHelper(const std::string& s, uint32_t base) const
3134 {
3135 CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
3136 CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base)
3137 << "base 2, 10, or 16";
3138
3139 return mkValHelper<CVC4::BitVector>(CVC4::BitVector(s, base));
3140 }
3141
3142 Term Solver::mkBVFromStrHelper(uint32_t size,
3143 const std::string& s,
3144 uint32_t base) const
3145 {
3146 CVC4_API_ARG_CHECK_EXPECTED(!s.empty(), s) << "a non-empty string";
3147 CVC4_API_ARG_CHECK_EXPECTED(base == 2 || base == 10 || base == 16, base)
3148 << "base 2, 10, or 16";
3149
3150 Integer val(s, base);
3151
3152 if (val.strictlyNegative())
3153 {
3154 CVC4_API_CHECK(val >= -Integer("2", 10).pow(size - 1))
3155 << "Overflow in bitvector construction (specified bitvector size "
3156 << size << " too small to hold value " << s << ")";
3157 }
3158 else
3159 {
3160 CVC4_API_CHECK(val.modByPow2(size) == val)
3161 << "Overflow in bitvector construction (specified bitvector size "
3162 << size << " too small to hold value " << s << ")";
3163 }
3164
3165 return mkValHelper<CVC4::BitVector>(CVC4::BitVector(size, val));
3166 }
3167
3168 Term Solver::mkCharFromStrHelper(const std::string& s) const
3169 {
3170 CVC4_API_CHECK(s.find_first_not_of("0123456789abcdefABCDEF", 0)
3171 == std::string::npos
3172 && s.size() <= 5 && s.size() > 0)
3173 << "Unexpected string for hexadecimal character " << s;
3174 uint32_t val = static_cast<uint32_t>(std::stoul(s, 0, 16));
3175 CVC4_API_CHECK(val < String::num_codes())
3176 << "Not a valid code point for hexadecimal character " << s;
3177 std::vector<unsigned> cpts;
3178 cpts.push_back(val);
3179 return mkValHelper<CVC4::String>(CVC4::String(cpts));
3180 }
3181
3182 Term Solver::mkTermFromKind(Kind kind) const
3183 {
3184 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3185 CVC4_API_KIND_CHECK_EXPECTED(
3186 kind == PI || kind == REGEXP_EMPTY || kind == REGEXP_SIGMA, kind)
3187 << "PI or REGEXP_EMPTY or REGEXP_SIGMA";
3188
3189 Expr res;
3190 if (kind == REGEXP_EMPTY || kind == REGEXP_SIGMA)
3191 {
3192 CVC4::Kind k = extToIntKind(kind);
3193 Assert(isDefinedIntKind(k));
3194 res = d_exprMgr->mkExpr(k, std::vector<Expr>());
3195 }
3196 else
3197 {
3198 Assert(kind == PI);
3199 res = d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
3200 }
3201 (void)res.getType(true); /* kick off type checking */
3202 return Term(this, res);
3203
3204 CVC4_API_SOLVER_TRY_CATCH_END;
3205 }
3206
3207 Term Solver::mkTermHelper(Kind kind, const std::vector<Term>& children) const
3208 {
3209 NodeManagerScope scope(getNodeManager());
3210 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3211 for (size_t i = 0, size = children.size(); i < size; ++i)
3212 {
3213 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3214 !children[i].isNull(), "child term", children[i], i)
3215 << "non-null term";
3216 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3217 this == children[i].d_solver, "child term", children[i], i)
3218 << "a child term associated to this solver object";
3219 }
3220
3221 std::vector<Expr> echildren = termVectorToExprs(children);
3222 CVC4::Kind k = extToIntKind(kind);
3223 Assert(isDefinedIntKind(k))
3224 << "Not a defined internal kind : " << k << " " << kind;
3225
3226 Expr res;
3227 if (echildren.size() > 2)
3228 {
3229 if (kind == INTS_DIVISION || kind == XOR || kind == MINUS
3230 || kind == DIVISION || kind == HO_APPLY)
3231 {
3232 // left-associative, but CVC4 internally only supports 2 args
3233 res = d_exprMgr->mkLeftAssociative(k, echildren);
3234 }
3235 else if (kind == IMPLIES)
3236 {
3237 // right-associative, but CVC4 internally only supports 2 args
3238 res = d_exprMgr->mkRightAssociative(k, echildren);
3239 }
3240 else if (kind == EQUAL || kind == LT || kind == GT || kind == LEQ
3241 || kind == GEQ)
3242 {
3243 // "chainable", but CVC4 internally only supports 2 args
3244 res = d_exprMgr->mkChain(k, echildren);
3245 }
3246 else if (kind::isAssociative(k))
3247 {
3248 // mkAssociative has special treatment for associative operators with lots
3249 // of children
3250 res = d_exprMgr->mkAssociative(k, echildren);
3251 }
3252 else
3253 {
3254 // default case, must check kind
3255 checkMkTerm(kind, children.size());
3256 res = d_exprMgr->mkExpr(k, echildren);
3257 }
3258 }
3259 else if (kind::isAssociative(k))
3260 {
3261 // associative case, same as above
3262 res = d_exprMgr->mkAssociative(k, echildren);
3263 }
3264 else
3265 {
3266 // default case, same as above
3267 checkMkTerm(kind, children.size());
3268 res = d_exprMgr->mkExpr(k, echildren);
3269 }
3270
3271 (void)res.getType(true); /* kick off type checking */
3272 return Term(this, res);
3273 CVC4_API_SOLVER_TRY_CATCH_END;
3274 }
3275
3276 std::vector<Sort> Solver::mkDatatypeSortsInternal(
3277 const std::vector<DatatypeDecl>& dtypedecls,
3278 const std::set<Sort>& unresolvedSorts) const
3279 {
3280 NodeManagerScope scope(getNodeManager());
3281 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3282
3283 std::vector<CVC4::DType> datatypes;
3284 for (size_t i = 0, ndts = dtypedecls.size(); i < ndts; ++i)
3285 {
3286 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == dtypedecls[i].d_solver,
3287 "datatype declaration",
3288 dtypedecls[i],
3289 i)
3290 << "a datatype declaration associated to this solver object";
3291 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(dtypedecls[i].getNumConstructors() > 0,
3292 "datatype declaration",
3293 dtypedecls[i],
3294 i)
3295 << "a datatype declaration with at least one constructor";
3296 datatypes.push_back(dtypedecls[i].getDatatype());
3297 }
3298 for (auto& sort : unresolvedSorts)
3299 {
3300 CVC4_API_SOLVER_CHECK_SORT(sort);
3301 }
3302
3303 std::set<TypeNode> utypes;
3304 for (const Sort& s : unresolvedSorts)
3305 {
3306 utypes.insert(TypeNode::fromType(s.getType()));
3307 }
3308 std::vector<CVC4::TypeNode> dtypes =
3309 getNodeManager()->mkMutualDatatypeTypes(datatypes, utypes);
3310 std::vector<Sort> retTypes;
3311 for (CVC4::TypeNode t : dtypes)
3312 {
3313 retTypes.push_back(Sort(this, t.toType()));
3314 }
3315 return retTypes;
3316
3317 CVC4_API_SOLVER_TRY_CATCH_END;
3318 }
3319
3320 /* Helpers for converting vectors. */
3321 /* .......................................................................... */
3322
3323 std::vector<Type> Solver::sortVectorToTypes(
3324 const std::vector<Sort>& sorts) const
3325 {
3326 std::vector<Type> res;
3327 for (const Sort& s : sorts)
3328 {
3329 CVC4_API_SOLVER_CHECK_SORT(s);
3330 res.push_back(*s.d_type);
3331 }
3332 return res;
3333 }
3334
3335 std::vector<Expr> Solver::termVectorToExprs(
3336 const std::vector<Term>& terms) const
3337 {
3338 std::vector<Expr> res;
3339 for (const Term& t : terms)
3340 {
3341 CVC4_API_SOLVER_CHECK_TERM(t);
3342 res.push_back(t.d_node->toExpr());
3343 }
3344 return res;
3345 }
3346
3347 /* Helpers for mkTerm checks. */
3348 /* .......................................................................... */
3349
3350 void Solver::checkMkTerm(Kind kind, uint32_t nchildren) const
3351 {
3352 CVC4_API_KIND_CHECK(kind);
3353 Assert(isDefinedIntKind(extToIntKind(kind)));
3354 const CVC4::kind::MetaKind mk = kind::metaKindOf(extToIntKind(kind));
3355 CVC4_API_KIND_CHECK_EXPECTED(
3356 mk == kind::metakind::PARAMETERIZED || mk == kind::metakind::OPERATOR,
3357 kind)
3358 << "Only operator-style terms are created with mkTerm(), "
3359 "to create variables, constants and values see mkVar(), mkConst() "
3360 "and the respective theory-specific functions to create values, "
3361 "e.g., mkBitVector().";
3362 CVC4_API_KIND_CHECK_EXPECTED(
3363 nchildren >= minArity(kind) && nchildren <= maxArity(kind), kind)
3364 << "Terms with kind " << kindToString(kind) << " must have at least "
3365 << minArity(kind) << " children and at most " << maxArity(kind)
3366 << " children (the one under construction has " << nchildren << ")";
3367 }
3368
3369 /* Solver Configuration */
3370 /* -------------------------------------------------------------------------- */
3371
3372 bool Solver::supportsFloatingPoint() const
3373 {
3374 return Configuration::isBuiltWithSymFPU();
3375 }
3376
3377 /* Sorts Handling */
3378 /* -------------------------------------------------------------------------- */
3379
3380 Sort Solver::getNullSort(void) const
3381 {
3382 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3383 return Sort(this, Type());
3384 CVC4_API_SOLVER_TRY_CATCH_END;
3385 }
3386
3387 Sort Solver::getBooleanSort(void) const
3388 {
3389 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3390 return Sort(this, d_exprMgr->booleanType());
3391 CVC4_API_SOLVER_TRY_CATCH_END;
3392 }
3393
3394 Sort Solver::getIntegerSort(void) const
3395 {
3396 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3397 return Sort(this, d_exprMgr->integerType());
3398 CVC4_API_SOLVER_TRY_CATCH_END;
3399 }
3400
3401 Sort Solver::getRealSort(void) const
3402 {
3403 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3404 return Sort(this, d_exprMgr->realType());
3405 CVC4_API_SOLVER_TRY_CATCH_END;
3406 }
3407
3408 Sort Solver::getRegExpSort(void) const
3409 {
3410 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3411 return Sort(this, d_exprMgr->regExpType());
3412 CVC4_API_SOLVER_TRY_CATCH_END;
3413 }
3414
3415 Sort Solver::getStringSort(void) const
3416 {
3417 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3418 return Sort(this, d_exprMgr->stringType());
3419 CVC4_API_SOLVER_TRY_CATCH_END;
3420 }
3421
3422 Sort Solver::getRoundingModeSort(void) const
3423 {
3424 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3425 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3426 << "Expected CVC4 to be compiled with SymFPU support";
3427 return Sort(this, d_exprMgr->roundingModeType());
3428 CVC4_API_SOLVER_TRY_CATCH_END;
3429 }
3430
3431 /* Create sorts ------------------------------------------------------- */
3432
3433 Sort Solver::mkArraySort(Sort indexSort, Sort elemSort) const
3434 {
3435 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3436 CVC4_API_ARG_CHECK_EXPECTED(!indexSort.isNull(), indexSort)
3437 << "non-null index sort";
3438 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
3439 << "non-null element sort";
3440 CVC4_API_SOLVER_CHECK_SORT(indexSort);
3441 CVC4_API_SOLVER_CHECK_SORT(elemSort);
3442
3443 return Sort(this,
3444 d_exprMgr->mkArrayType(*indexSort.d_type, *elemSort.d_type));
3445
3446 CVC4_API_SOLVER_TRY_CATCH_END;
3447 }
3448
3449 Sort Solver::mkBitVectorSort(uint32_t size) const
3450 {
3451 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3452 CVC4_API_ARG_CHECK_EXPECTED(size > 0, size) << "size > 0";
3453
3454 return Sort(this, d_exprMgr->mkBitVectorType(size));
3455
3456 CVC4_API_SOLVER_TRY_CATCH_END;
3457 }
3458
3459 Sort Solver::mkFloatingPointSort(uint32_t exp, uint32_t sig) const
3460 {
3461 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3462 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3463 << "Expected CVC4 to be compiled with SymFPU support";
3464 CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "exponent size > 0";
3465 CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "significand size > 0";
3466
3467 return Sort(this, d_exprMgr->mkFloatingPointType(exp, sig));
3468
3469 CVC4_API_SOLVER_TRY_CATCH_END;
3470 }
3471
3472 Sort Solver::mkDatatypeSort(DatatypeDecl dtypedecl) const
3473 {
3474 NodeManagerScope scope(getNodeManager());
3475 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3476 CVC4_API_CHECK(this == dtypedecl.d_solver)
3477 << "Given datatype declaration is not associated with this solver";
3478 CVC4_API_ARG_CHECK_EXPECTED(dtypedecl.getNumConstructors() > 0, dtypedecl)
3479 << "a datatype declaration with at least one constructor";
3480
3481 return Sort(this,
3482 getNodeManager()->mkDatatypeType(*dtypedecl.d_dtype).toType());
3483
3484 CVC4_API_SOLVER_TRY_CATCH_END;
3485 }
3486
3487 std::vector<Sort> Solver::mkDatatypeSorts(
3488 std::vector<DatatypeDecl>& dtypedecls) const
3489 {
3490 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3491 std::set<Sort> unresolvedSorts;
3492 return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
3493 CVC4_API_SOLVER_TRY_CATCH_END;
3494 }
3495
3496 std::vector<Sort> Solver::mkDatatypeSorts(
3497 const std::vector<DatatypeDecl>& dtypedecls,
3498 const std::set<Sort>& unresolvedSorts) const
3499 {
3500 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3501 return mkDatatypeSortsInternal(dtypedecls, unresolvedSorts);
3502 CVC4_API_SOLVER_TRY_CATCH_END;
3503 }
3504
3505 Sort Solver::mkFunctionSort(Sort domain, Sort codomain) const
3506 {
3507 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3508 CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
3509 << "non-null codomain sort";
3510 CVC4_API_SOLVER_CHECK_SORT(domain);
3511 CVC4_API_SOLVER_CHECK_SORT(codomain);
3512 CVC4_API_ARG_CHECK_EXPECTED(domain.isFirstClass(), domain)
3513 << "first-class sort as domain sort for function sort";
3514 CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
3515 << "first-class sort as codomain sort for function sort";
3516 Assert(!codomain.isFunction()); /* A function sort is not first-class. */
3517
3518 return Sort(this,
3519 d_exprMgr->mkFunctionType(*domain.d_type, *codomain.d_type));
3520
3521 CVC4_API_SOLVER_TRY_CATCH_END;
3522 }
3523
3524 Sort Solver::mkFunctionSort(const std::vector<Sort>& sorts, Sort codomain) const
3525 {
3526 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3527 CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
3528 << "at least one parameter sort for function sort";
3529 for (size_t i = 0, size = sorts.size(); i < size; ++i)
3530 {
3531 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3532 !sorts[i].isNull(), "parameter sort", sorts[i], i)
3533 << "non-null sort";
3534 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3535 this == sorts[i].d_solver, "parameter sort", sorts[i], i)
3536 << "sort associated to this solver object";
3537 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3538 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
3539 << "first-class sort as parameter sort for function sort";
3540 }
3541 CVC4_API_ARG_CHECK_EXPECTED(!codomain.isNull(), codomain)
3542 << "non-null codomain sort";
3543 CVC4_API_SOLVER_CHECK_SORT(codomain);
3544 CVC4_API_ARG_CHECK_EXPECTED(codomain.isFirstClass(), codomain)
3545 << "first-class sort as codomain sort for function sort";
3546 Assert(!codomain.isFunction()); /* A function sort is not first-class. */
3547
3548 std::vector<Type> argTypes = sortVectorToTypes(sorts);
3549 return Sort(this, d_exprMgr->mkFunctionType(argTypes, *codomain.d_type));
3550
3551 CVC4_API_SOLVER_TRY_CATCH_END;
3552 }
3553
3554 Sort Solver::mkParamSort(const std::string& symbol) const
3555 {
3556 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3557 return Sort(this,
3558 d_exprMgr->mkSort(symbol, ExprManager::SORT_FLAG_PLACEHOLDER));
3559 CVC4_API_SOLVER_TRY_CATCH_END;
3560 }
3561
3562 Sort Solver::mkPredicateSort(const std::vector<Sort>& sorts) const
3563 {
3564 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3565 CVC4_API_ARG_SIZE_CHECK_EXPECTED(sorts.size() >= 1, sorts)
3566 << "at least one parameter sort for predicate sort";
3567 for (size_t i = 0, size = sorts.size(); i < size; ++i)
3568 {
3569 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3570 !sorts[i].isNull(), "parameter sort", sorts[i], i)
3571 << "non-null sort";
3572 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3573 this == sorts[i].d_solver, "parameter sort", sorts[i], i)
3574 << "sort associated to this solver object";
3575 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3576 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
3577 << "first-class sort as parameter sort for predicate sort";
3578 }
3579 std::vector<Type> types = sortVectorToTypes(sorts);
3580
3581 return Sort(this, d_exprMgr->mkPredicateType(types));
3582
3583 CVC4_API_SOLVER_TRY_CATCH_END;
3584 }
3585
3586 Sort Solver::mkRecordSort(
3587 const std::vector<std::pair<std::string, Sort>>& fields) const
3588 {
3589 NodeManagerScope scope(getNodeManager());
3590 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3591 std::vector<std::pair<std::string, Type>> f;
3592 size_t i = 0;
3593 for (const auto& p : fields)
3594 {
3595 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3596 !p.second.isNull(), "parameter sort", p.second, i)
3597 << "non-null sort";
3598 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3599 this == p.second.d_solver, "parameter sort", p.second, i)
3600 << "sort associated to this solver object";
3601 i += 1;
3602 f.emplace_back(p.first, *p.second.d_type);
3603 }
3604
3605 return Sort(this, getNodeManager()->mkRecordType(Record(f)).toType());
3606
3607 CVC4_API_SOLVER_TRY_CATCH_END;
3608 }
3609
3610 Sort Solver::mkSetSort(Sort elemSort) const
3611 {
3612 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3613 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
3614 << "non-null element sort";
3615 CVC4_API_SOLVER_CHECK_SORT(elemSort);
3616
3617 return Sort(this, d_exprMgr->mkSetType(*elemSort.d_type));
3618
3619 CVC4_API_SOLVER_TRY_CATCH_END;
3620 }
3621
3622 Sort Solver::mkBagSort(Sort elemSort) const
3623 {
3624 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3625 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
3626 << "non-null element sort";
3627 CVC4_API_SOLVER_CHECK_SORT(elemSort);
3628
3629 TypeNode typeNode = TypeNode::fromType(*elemSort.d_type);
3630 Type type = getNodeManager()->mkBagType(typeNode).toType();
3631 return Sort(this, type);
3632
3633 CVC4_API_SOLVER_TRY_CATCH_END;
3634 }
3635
3636 Sort Solver::mkSequenceSort(Sort elemSort) const
3637 {
3638 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3639 CVC4_API_ARG_CHECK_EXPECTED(!elemSort.isNull(), elemSort)
3640 << "non-null element sort";
3641 CVC4_API_SOLVER_CHECK_SORT(elemSort);
3642
3643 return Sort(this, d_exprMgr->mkSequenceType(*elemSort.d_type));
3644
3645 CVC4_API_SOLVER_TRY_CATCH_END;
3646 }
3647
3648 Sort Solver::mkUninterpretedSort(const std::string& symbol) const
3649 {
3650 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3651 return Sort(this, d_exprMgr->mkSort(symbol));
3652 CVC4_API_SOLVER_TRY_CATCH_END;
3653 }
3654
3655 Sort Solver::mkSortConstructorSort(const std::string& symbol,
3656 size_t arity) const
3657 {
3658 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3659 CVC4_API_ARG_CHECK_EXPECTED(arity > 0, arity) << "an arity > 0";
3660
3661 return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
3662
3663 CVC4_API_SOLVER_TRY_CATCH_END;
3664 }
3665
3666 Sort Solver::mkTupleSort(const std::vector<Sort>& sorts) const
3667 {
3668 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3669 for (size_t i = 0, size = sorts.size(); i < size; ++i)
3670 {
3671 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3672 !sorts[i].isNull(), "parameter sort", sorts[i], i)
3673 << "non-null sort";
3674 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3675 this == sorts[i].d_solver, "parameter sort", sorts[i], i)
3676 << "sort associated to this solver object";
3677 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
3678 !sorts[i].isFunctionLike(), "parameter sort", sorts[i], i)
3679 << "non-function-like sort as parameter sort for tuple sort";
3680 }
3681 std::vector<TypeNode> typeNodes;
3682 for (const Sort& s : sorts)
3683 {
3684 typeNodes.push_back(TypeNode::fromType(*s.d_type));
3685 }
3686 return Sort(this, getNodeManager()->mkTupleType(typeNodes).toType());
3687
3688 CVC4_API_SOLVER_TRY_CATCH_END;
3689 }
3690
3691 /* Create consts */
3692 /* -------------------------------------------------------------------------- */
3693
3694 Term Solver::mkTrue(void) const
3695 {
3696 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3697 return Term(this, d_exprMgr->mkConst<bool>(true));
3698 CVC4_API_SOLVER_TRY_CATCH_END;
3699 }
3700
3701 Term Solver::mkFalse(void) const
3702 {
3703 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3704 return Term(this, d_exprMgr->mkConst<bool>(false));
3705 CVC4_API_SOLVER_TRY_CATCH_END;
3706 }
3707
3708 Term Solver::mkBoolean(bool val) const
3709 {
3710 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3711 return Term(this, d_exprMgr->mkConst<bool>(val));
3712 CVC4_API_SOLVER_TRY_CATCH_END;
3713 }
3714
3715 Term Solver::mkPi() const
3716 {
3717 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3718
3719 Expr res =
3720 d_exprMgr->mkNullaryOperator(d_exprMgr->realType(), CVC4::kind::PI);
3721 (void)res.getType(true); /* kick off type checking */
3722 return Term(this, res);
3723
3724 CVC4_API_SOLVER_TRY_CATCH_END;
3725 }
3726
3727 Term Solver::mkReal(const std::string& s) const
3728 {
3729 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3730 return mkRealFromStrHelper(s);
3731 CVC4_API_SOLVER_TRY_CATCH_END;
3732 }
3733
3734 Term Solver::mkReal(int64_t val) const
3735 {
3736 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3737 return mkValHelper<CVC4::Rational>(CVC4::Rational(val));
3738 CVC4_API_SOLVER_TRY_CATCH_END;
3739 }
3740
3741 Term Solver::mkReal(int64_t num, int64_t den) const
3742 {
3743 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3744 return mkValHelper<CVC4::Rational>(CVC4::Rational(num, den));
3745 CVC4_API_SOLVER_TRY_CATCH_END;
3746 }
3747
3748 Term Solver::mkRegexpEmpty() const
3749 {
3750 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3751
3752 Expr res =
3753 d_exprMgr->mkExpr(CVC4::kind::REGEXP_EMPTY, std::vector<CVC4::Expr>());
3754 (void)res.getType(true); /* kick off type checking */
3755 return Term(this, res);
3756
3757 CVC4_API_SOLVER_TRY_CATCH_END;
3758 }
3759
3760 Term Solver::mkRegexpSigma() const
3761 {
3762 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3763
3764 Expr res =
3765 d_exprMgr->mkExpr(CVC4::kind::REGEXP_SIGMA, std::vector<CVC4::Expr>());
3766 (void)res.getType(true); /* kick off type checking */
3767 return Term(this, res);
3768
3769 CVC4_API_SOLVER_TRY_CATCH_END;
3770 }
3771
3772 Term Solver::mkEmptySet(Sort s) const
3773 {
3774 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3775 CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isSet(), s)
3776 << "null sort or set sort";
3777 CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
3778 << "set sort associated to this solver object";
3779
3780 return mkValHelper<CVC4::EmptySet>(
3781 CVC4::EmptySet(TypeNode::fromType(*s.d_type)));
3782
3783 CVC4_API_SOLVER_TRY_CATCH_END;
3784 }
3785
3786 Term Solver::mkSingleton(Sort s, Term t) const
3787 {
3788 NodeManagerScope scope(getNodeManager());
3789
3790 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3791 CVC4_API_ARG_CHECK_EXPECTED(!t.isNull(), t) << "non-null term";
3792 CVC4_API_SOLVER_CHECK_TERM(t);
3793 checkMkTerm(SINGLETON, 1);
3794
3795 TypeNode typeNode = TypeNode::fromType(*s.d_type);
3796 Node res = getNodeManager()->mkSingleton(typeNode, *t.d_node);
3797 (void)res.getType(true); /* kick off type checking */
3798 return Term(this, res);
3799
3800 CVC4_API_SOLVER_TRY_CATCH_END;
3801 }
3802
3803 Term Solver::mkEmptyBag(Sort s) const
3804 {
3805 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3806 CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || s.isBag(), s)
3807 << "null sort or bag sort";
3808
3809 CVC4_API_ARG_CHECK_EXPECTED(s.isNull() || this == s.d_solver, s)
3810 << "bag sort associated to this solver object";
3811
3812 return mkValHelper<CVC4::EmptyBag>(
3813 CVC4::EmptyBag(TypeNode::fromType(*s.d_type)));
3814
3815 CVC4_API_SOLVER_TRY_CATCH_END;
3816 }
3817
3818 Term Solver::mkSepNil(Sort sort) const
3819 {
3820 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3821 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
3822 CVC4_API_SOLVER_CHECK_SORT(sort);
3823
3824 Expr res = d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::SEP_NIL);
3825 (void)res.getType(true); /* kick off type checking */
3826 return Term(this, res);
3827
3828 CVC4_API_SOLVER_TRY_CATCH_END;
3829 }
3830
3831 Term Solver::mkString(const std::string& s, bool useEscSequences) const
3832 {
3833 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3834 return mkValHelper<CVC4::String>(CVC4::String(s, useEscSequences));
3835 CVC4_API_SOLVER_TRY_CATCH_END;
3836 }
3837
3838 Term Solver::mkString(const unsigned char c) const
3839 {
3840 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3841 return mkValHelper<CVC4::String>(CVC4::String(std::string(1, c)));
3842 CVC4_API_SOLVER_TRY_CATCH_END;
3843 }
3844
3845 Term Solver::mkString(const std::vector<unsigned>& s) const
3846 {
3847 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3848 return mkValHelper<CVC4::String>(CVC4::String(s));
3849 CVC4_API_SOLVER_TRY_CATCH_END;
3850 }
3851
3852 Term Solver::mkChar(const std::string& s) const
3853 {
3854 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3855 return mkCharFromStrHelper(s);
3856 CVC4_API_SOLVER_TRY_CATCH_END;
3857 }
3858
3859 Term Solver::mkEmptySequence(Sort sort) const
3860 {
3861 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3862 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
3863 CVC4_API_SOLVER_CHECK_SORT(sort);
3864
3865 std::vector<Node> seq;
3866 Expr res =
3867 d_exprMgr->mkConst(Sequence(TypeNode::fromType(*sort.d_type), seq));
3868 return Term(this, res);
3869
3870 CVC4_API_SOLVER_TRY_CATCH_END;
3871 }
3872
3873 Term Solver::mkUniverseSet(Sort sort) const
3874 {
3875 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3876 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
3877 CVC4_API_SOLVER_CHECK_SORT(sort);
3878
3879 Expr res =
3880 d_exprMgr->mkNullaryOperator(*sort.d_type, CVC4::kind::UNIVERSE_SET);
3881 // TODO(#2771): Reenable?
3882 // (void)res->getType(true); /* kick off type checking */
3883 return Term(this, res);
3884
3885 CVC4_API_SOLVER_TRY_CATCH_END;
3886 }
3887
3888 Term Solver::mkBitVector(uint32_t size, uint64_t val) const
3889 {
3890 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3891 return mkBVFromIntHelper(size, val);
3892 CVC4_API_SOLVER_TRY_CATCH_END;
3893 }
3894
3895 Term Solver::mkBitVector(const std::string& s, uint32_t base) const
3896 {
3897 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3898 return mkBVFromStrHelper(s, base);
3899 CVC4_API_SOLVER_TRY_CATCH_END;
3900 }
3901
3902 Term Solver::mkBitVector(uint32_t size,
3903 const std::string& s,
3904 uint32_t base) const
3905 {
3906 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3907 return mkBVFromStrHelper(size, s, base);
3908 CVC4_API_SOLVER_TRY_CATCH_END;
3909 }
3910
3911 Term Solver::mkConstArray(Sort sort, Term val) const
3912 {
3913 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3914 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
3915 CVC4_API_ARG_CHECK_NOT_NULL(sort);
3916 CVC4_API_ARG_CHECK_NOT_NULL(val);
3917 CVC4_API_SOLVER_CHECK_SORT(sort);
3918 CVC4_API_SOLVER_CHECK_TERM(val);
3919 CVC4_API_CHECK(sort.isArray()) << "Not an array sort.";
3920 CVC4_API_CHECK(sort.getArrayElementSort().isComparableTo(val.getSort()))
3921 << "Value does not match element sort.";
3922 Term res = mkValHelper<CVC4::ArrayStoreAll>(CVC4::ArrayStoreAll(
3923 TypeNode::fromType(*sort.d_type), Node::fromExpr(val.d_node->toExpr())));
3924 return res;
3925 CVC4_API_SOLVER_TRY_CATCH_END;
3926 }
3927
3928 Term Solver::mkPosInf(uint32_t exp, uint32_t sig) const
3929 {
3930 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3931 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3932 << "Expected CVC4 to be compiled with SymFPU support";
3933
3934 return mkValHelper<CVC4::FloatingPoint>(
3935 FloatingPoint::makeInf(FloatingPointSize(exp, sig), false));
3936
3937 CVC4_API_SOLVER_TRY_CATCH_END;
3938 }
3939
3940 Term Solver::mkNegInf(uint32_t exp, uint32_t sig) const
3941 {
3942 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3943 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3944 << "Expected CVC4 to be compiled with SymFPU support";
3945
3946 return mkValHelper<CVC4::FloatingPoint>(
3947 FloatingPoint::makeInf(FloatingPointSize(exp, sig), true));
3948
3949 CVC4_API_SOLVER_TRY_CATCH_END;
3950 }
3951
3952 Term Solver::mkNaN(uint32_t exp, uint32_t sig) const
3953 {
3954 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3955 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3956 << "Expected CVC4 to be compiled with SymFPU support";
3957
3958 return mkValHelper<CVC4::FloatingPoint>(
3959 FloatingPoint::makeNaN(FloatingPointSize(exp, sig)));
3960
3961 CVC4_API_SOLVER_TRY_CATCH_END;
3962 }
3963
3964 Term Solver::mkPosZero(uint32_t exp, uint32_t sig) const
3965 {
3966 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3967 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3968 << "Expected CVC4 to be compiled with SymFPU support";
3969
3970 return mkValHelper<CVC4::FloatingPoint>(
3971 FloatingPoint::makeZero(FloatingPointSize(exp, sig), false));
3972
3973 CVC4_API_SOLVER_TRY_CATCH_END;
3974 }
3975
3976 Term Solver::mkNegZero(uint32_t exp, uint32_t sig) const
3977 {
3978 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3979 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3980 << "Expected CVC4 to be compiled with SymFPU support";
3981
3982 return mkValHelper<CVC4::FloatingPoint>(
3983 FloatingPoint::makeZero(FloatingPointSize(exp, sig), true));
3984
3985 CVC4_API_SOLVER_TRY_CATCH_END;
3986 }
3987
3988 Term Solver::mkRoundingMode(RoundingMode rm) const
3989 {
3990 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
3991 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
3992 << "Expected CVC4 to be compiled with SymFPU support";
3993 return mkValHelper<CVC4::RoundingMode>(s_rmodes.at(rm));
3994 CVC4_API_SOLVER_TRY_CATCH_END;
3995 }
3996
3997 Term Solver::mkUninterpretedConst(Sort sort, int32_t index) const
3998 {
3999 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4000 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
4001 CVC4_API_SOLVER_CHECK_SORT(sort);
4002
4003 return mkValHelper<CVC4::UninterpretedConstant>(
4004 CVC4::UninterpretedConstant(TypeNode::fromType(*sort.d_type), index));
4005
4006 CVC4_API_SOLVER_TRY_CATCH_END;
4007 }
4008
4009 Term Solver::mkAbstractValue(const std::string& index) const
4010 {
4011 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4012 CVC4_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
4013
4014 CVC4::Integer idx(index, 10);
4015 CVC4_API_ARG_CHECK_EXPECTED(idx > 0, index)
4016 << "a string representing an integer > 0";
4017 return Term(this, getNodeManager()->mkConst(CVC4::AbstractValue(idx)));
4018 // do not call getType(), for abstract values, type can not be computed
4019 // until it is substituted away
4020 CVC4_API_SOLVER_TRY_CATCH_END;
4021 }
4022
4023 Term Solver::mkAbstractValue(uint64_t index) const
4024 {
4025 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4026 CVC4_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
4027
4028 return Term(this,
4029 getNodeManager()->mkConst(CVC4::AbstractValue(Integer(index))));
4030 // do not call getType(), for abstract values, type can not be computed
4031 // until it is substituted away
4032 CVC4_API_SOLVER_TRY_CATCH_END;
4033 }
4034
4035 Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
4036 {
4037 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4038 CVC4_API_CHECK(Configuration::isBuiltWithSymFPU())
4039 << "Expected CVC4 to be compiled with SymFPU support";
4040 CVC4_API_ARG_CHECK_EXPECTED(exp > 0, exp) << "a value > 0";
4041 CVC4_API_ARG_CHECK_EXPECTED(sig > 0, sig) << "a value > 0";
4042 uint32_t bw = exp + sig;
4043 CVC4_API_ARG_CHECK_EXPECTED(bw == val.getSort().getBVSize(), val)
4044 << "a bit-vector constant with bit-width '" << bw << "'";
4045 CVC4_API_ARG_CHECK_EXPECTED(!val.isNull(), val) << "non-null term";
4046 CVC4_API_SOLVER_CHECK_TERM(val);
4047 CVC4_API_ARG_CHECK_EXPECTED(
4048 val.getSort().isBitVector() && val.d_node->isConst(), val)
4049 << "bit-vector constant";
4050
4051 return mkValHelper<CVC4::FloatingPoint>(
4052 CVC4::FloatingPoint(exp, sig, val.d_node->getConst<BitVector>()));
4053
4054 CVC4_API_SOLVER_TRY_CATCH_END;
4055 }
4056
4057 /* Create constants */
4058 /* -------------------------------------------------------------------------- */
4059
4060 Term Solver::mkConst(Sort sort, const std::string& symbol) const
4061 {
4062 NodeManagerScope scope(getNodeManager());
4063 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4064 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
4065 CVC4_API_SOLVER_CHECK_SORT(sort);
4066
4067 Expr res = symbol.empty() ? d_exprMgr->mkVar(*sort.d_type)
4068 : d_exprMgr->mkVar(symbol, *sort.d_type);
4069 (void)res.getType(true); /* kick off type checking */
4070 return Term(this, res);
4071
4072 CVC4_API_SOLVER_TRY_CATCH_END;
4073 }
4074
4075 /* Create variables */
4076 /* -------------------------------------------------------------------------- */
4077
4078 Term Solver::mkVar(Sort sort, const std::string& symbol) const
4079 {
4080 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4081 CVC4_API_ARG_CHECK_EXPECTED(!sort.isNull(), sort) << "non-null sort";
4082 CVC4_API_SOLVER_CHECK_SORT(sort);
4083
4084 Expr res = symbol.empty() ? d_exprMgr->mkBoundVar(*sort.d_type)
4085 : d_exprMgr->mkBoundVar(symbol, *sort.d_type);
4086 (void)res.getType(true); /* kick off type checking */
4087 return Term(this, res);
4088
4089 CVC4_API_SOLVER_TRY_CATCH_END;
4090 }
4091
4092 /* Create datatype constructor declarations */
4093 /* -------------------------------------------------------------------------- */
4094
4095 DatatypeConstructorDecl Solver::mkDatatypeConstructorDecl(
4096 const std::string& name)
4097 {
4098 NodeManagerScope scope(getNodeManager());
4099 return DatatypeConstructorDecl(this, name);
4100 }
4101
4102 /* Create datatype declarations */
4103 /* -------------------------------------------------------------------------- */
4104
4105 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name, bool isCoDatatype)
4106 {
4107 NodeManagerScope scope(getNodeManager());
4108 return DatatypeDecl(this, name, isCoDatatype);
4109 }
4110
4111 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
4112 Sort param,
4113 bool isCoDatatype)
4114 {
4115 NodeManagerScope scope(getNodeManager());
4116 return DatatypeDecl(this, name, param, isCoDatatype);
4117 }
4118
4119 DatatypeDecl Solver::mkDatatypeDecl(const std::string& name,
4120 const std::vector<Sort>& params,
4121 bool isCoDatatype)
4122 {
4123 NodeManagerScope scope(getNodeManager());
4124 return DatatypeDecl(this, name, params, isCoDatatype);
4125 }
4126
4127 /* Create terms */
4128 /* -------------------------------------------------------------------------- */
4129
4130 Term Solver::mkTerm(Kind kind) const
4131 {
4132 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4133 return mkTermFromKind(kind);
4134 CVC4_API_SOLVER_TRY_CATCH_END;
4135 }
4136
4137 Term Solver::mkTerm(Kind kind, Term child) const
4138 {
4139 NodeManagerScope scope(getNodeManager());
4140 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4141 CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
4142 CVC4_API_SOLVER_CHECK_TERM(child);
4143 checkMkTerm(kind, 1);
4144
4145 Node res = getNodeManager()->mkNode(extToIntKind(kind), *child.d_node);
4146 (void)res.getType(true); /* kick off type checking */
4147 return Term(this, res);
4148
4149 CVC4_API_SOLVER_TRY_CATCH_END;
4150 }
4151
4152 Term Solver::mkTerm(Kind kind, Term child1, Term child2) const
4153 {
4154 NodeManagerScope scope(getNodeManager());
4155 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4156 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
4157 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
4158 CVC4_API_SOLVER_CHECK_TERM(child1);
4159 CVC4_API_SOLVER_CHECK_TERM(child2);
4160 checkMkTerm(kind, 2);
4161
4162 Node res = getNodeManager()->mkNode(
4163 extToIntKind(kind), *child1.d_node, *child2.d_node);
4164 (void)res.getType(true); /* kick off type checking */
4165 return Term(this, res);
4166
4167 CVC4_API_SOLVER_TRY_CATCH_END;
4168 }
4169
4170 Term Solver::mkTerm(Kind kind, Term child1, Term child2, Term child3) const
4171 {
4172 // need to use internal term call to check e.g. associative construction
4173 return mkTermHelper(kind, std::vector<Term>{child1, child2, child3});
4174 }
4175
4176 Term Solver::mkTerm(Kind kind, const std::vector<Term>& children) const
4177 {
4178 return mkTermHelper(kind, children);
4179 }
4180
4181 Term Solver::mkTerm(Op op) const
4182 {
4183 NodeManagerScope scope(getNodeManager());
4184 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4185 CVC4_API_SOLVER_CHECK_OP(op);
4186 checkMkTerm(op.d_kind, 0);
4187
4188 Term res;
4189 if (op.isIndexedHelper())
4190 {
4191 const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4192 res = Term(this, getNodeManager()->mkNode(int_kind, *op.d_node));
4193 }
4194 else
4195 {
4196 res = mkTermFromKind(op.d_kind);
4197 }
4198
4199 (void)res.d_node->getType(true); /* kick off type checking */
4200 return res;
4201
4202 CVC4_API_SOLVER_TRY_CATCH_END;
4203 }
4204
4205 Term Solver::mkTerm(Op op, Term child) const
4206 {
4207 NodeManagerScope scope(getNodeManager());
4208 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4209 CVC4_API_SOLVER_CHECK_OP(op);
4210 CVC4_API_ARG_CHECK_EXPECTED(!child.isNull(), child) << "non-null term";
4211 CVC4_API_SOLVER_CHECK_TERM(child);
4212 checkMkTerm(op.d_kind, 1);
4213
4214 const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4215 Node res;
4216 if (op.isIndexedHelper())
4217 {
4218 res = getNodeManager()->mkNode(int_kind, *op.d_node, *child.d_node);
4219 }
4220 else
4221 {
4222 res = getNodeManager()->mkNode(int_kind, *child.d_node);
4223 }
4224
4225 (void)res.getType(true); /* kick off type checking */
4226 return Term(this, res);
4227
4228 CVC4_API_SOLVER_TRY_CATCH_END;
4229 }
4230
4231 Term Solver::mkTerm(Op op, Term child1, Term child2) const
4232 {
4233 NodeManagerScope scope(getNodeManager());
4234 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4235 CVC4_API_SOLVER_CHECK_OP(op);
4236 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
4237 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
4238 CVC4_API_SOLVER_CHECK_TERM(child1);
4239 CVC4_API_SOLVER_CHECK_TERM(child2);
4240 checkMkTerm(op.d_kind, 2);
4241
4242 const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4243 Node res;
4244 if (op.isIndexedHelper())
4245 {
4246 res = getNodeManager()->mkNode(
4247 int_kind, *op.d_node, *child1.d_node, *child2.d_node);
4248 }
4249 else
4250 {
4251 res = getNodeManager()->mkNode(int_kind, *child1.d_node, *child2.d_node);
4252 }
4253
4254 (void)res.getType(true); /* kick off type checking */
4255 return Term(this, res);
4256 CVC4_API_SOLVER_TRY_CATCH_END;
4257 }
4258
4259 Term Solver::mkTerm(Op op, Term child1, Term child2, Term child3) const
4260 {
4261 NodeManagerScope scope(getNodeManager());
4262 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4263 CVC4_API_SOLVER_CHECK_OP(op);
4264 CVC4_API_ARG_CHECK_EXPECTED(!child1.isNull(), child1) << "non-null term";
4265 CVC4_API_ARG_CHECK_EXPECTED(!child2.isNull(), child2) << "non-null term";
4266 CVC4_API_ARG_CHECK_EXPECTED(!child3.isNull(), child3) << "non-null term";
4267 CVC4_API_SOLVER_CHECK_TERM(child1);
4268 CVC4_API_SOLVER_CHECK_TERM(child2);
4269 CVC4_API_SOLVER_CHECK_TERM(child3);
4270 checkMkTerm(op.d_kind, 3);
4271
4272 const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4273 Node res;
4274 if (op.isIndexedHelper())
4275 {
4276 res = getNodeManager()->mkNode(
4277 int_kind, *op.d_node, *child1.d_node, *child2.d_node, *child3.d_node);
4278 }
4279 else
4280 {
4281 res = getNodeManager()->mkNode(
4282 int_kind, *child1.d_node, *child2.d_node, *child3.d_node);
4283 }
4284
4285 (void)res.getType(true); /* kick off type checking */
4286 return Term(this, res);
4287
4288 CVC4_API_SOLVER_TRY_CATCH_END;
4289 }
4290
4291 Term Solver::mkTerm(Op op, const std::vector<Term>& children) const
4292 {
4293 NodeManagerScope scope(getNodeManager());
4294 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4295 CVC4_API_SOLVER_CHECK_OP(op);
4296 checkMkTerm(op.d_kind, children.size());
4297 for (size_t i = 0, size = children.size(); i < size; ++i)
4298 {
4299 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4300 !children[i].isNull(), "child term", children[i], i)
4301 << "non-null term";
4302 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4303 this == children[i].d_solver, "child term", children[i], i)
4304 << "child term associated to this solver object";
4305 }
4306
4307 const CVC4::Kind int_kind = extToIntKind(op.d_kind);
4308 std::vector<Node> echildren = termVectorToNodes(children);
4309 Node res;
4310 if (op.isIndexedHelper())
4311 {
4312 NodeBuilder<> nb(int_kind);
4313 nb << *op.d_node;
4314 nb.append(echildren);
4315 res = nb.constructNode();
4316 }
4317 else
4318 {
4319 res = getNodeManager()->mkNode(int_kind, echildren);
4320 }
4321
4322 (void)res.getType(true); /* kick off type checking */
4323 return Term(this, res);
4324
4325 CVC4_API_SOLVER_TRY_CATCH_END;
4326 }
4327
4328 Term Solver::mkTuple(const std::vector<Sort>& sorts,
4329 const std::vector<Term>& terms) const
4330 {
4331 NodeManagerScope scope(getNodeManager());
4332 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4333 CVC4_API_CHECK(sorts.size() == terms.size())
4334 << "Expected the same number of sorts and elements";
4335 std::vector<CVC4::Node> args;
4336 for (size_t i = 0, size = sorts.size(); i < size; i++)
4337 {
4338 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4339 this == terms[i].d_solver, "child term", terms[i], i)
4340 << "child term associated to this solver object";
4341 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4342 this == sorts[i].d_solver, "child sort", sorts[i], i)
4343 << "child sort associated to this solver object";
4344 args.push_back(*(ensureTermSort(terms[i], sorts[i])).d_node);
4345 }
4346
4347 Sort s = mkTupleSort(sorts);
4348 Datatype dt = s.getDatatype();
4349 NodeBuilder<> nb(extToIntKind(APPLY_CONSTRUCTOR));
4350 nb << *dt[0].getConstructorTerm().d_node;
4351 nb.append(args);
4352 Node res = nb.constructNode();
4353 (void)res.getType(true); /* kick off type checking */
4354 return Term(this, res);
4355
4356 CVC4_API_SOLVER_TRY_CATCH_END;
4357 }
4358
4359 /* Create operators */
4360 /* -------------------------------------------------------------------------- */
4361
4362 Op Solver::mkOp(Kind kind) const
4363 {
4364 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4365 CVC4_API_CHECK(s_indexed_kinds.find(kind) == s_indexed_kinds.end())
4366 << "Expected a kind for a non-indexed operator.";
4367 return Op(this, kind);
4368 CVC4_API_SOLVER_TRY_CATCH_END
4369 }
4370
4371 Op Solver::mkOp(Kind kind, const std::string& arg) const
4372 {
4373 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4374 CVC4_API_KIND_CHECK_EXPECTED((kind == RECORD_UPDATE) || (kind == DIVISIBLE),
4375 kind)
4376 << "RECORD_UPDATE or DIVISIBLE";
4377 Op res;
4378 if (kind == RECORD_UPDATE)
4379 {
4380 res = Op(this,
4381 kind,
4382 *mkValHelper<CVC4::RecordUpdate>(CVC4::RecordUpdate(arg)).d_node);
4383 }
4384 else
4385 {
4386 /* CLN and GMP handle this case differently, CLN interprets it as 0, GMP
4387 * throws an std::invalid_argument exception. For consistency, we treat it
4388 * as invalid. */
4389 CVC4_API_ARG_CHECK_EXPECTED(arg != ".", arg)
4390 << "a string representing an integer, real or rational value.";
4391 res = Op(this,
4392 kind,
4393 *mkValHelper<CVC4::Divisible>(CVC4::Divisible(CVC4::Integer(arg)))
4394 .d_node);
4395 }
4396 return res;
4397
4398 CVC4_API_SOLVER_TRY_CATCH_END;
4399 }
4400
4401 Op Solver::mkOp(Kind kind, uint32_t arg) const
4402 {
4403 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4404 CVC4_API_KIND_CHECK(kind);
4405
4406 Op res;
4407 switch (kind)
4408 {
4409 case DIVISIBLE:
4410 res = Op(this,
4411 kind,
4412 *mkValHelper<CVC4::Divisible>(CVC4::Divisible(arg)).d_node);
4413 break;
4414 case BITVECTOR_REPEAT:
4415 res = Op(this,
4416 kind,
4417 mkValHelper<CVC4::BitVectorRepeat>(CVC4::BitVectorRepeat(arg))
4418 .d_node->toExpr());
4419 break;
4420 case BITVECTOR_ZERO_EXTEND:
4421 res = Op(this,
4422 kind,
4423 *mkValHelper<CVC4::BitVectorZeroExtend>(
4424 CVC4::BitVectorZeroExtend(arg))
4425 .d_node);
4426 break;
4427 case BITVECTOR_SIGN_EXTEND:
4428 res = Op(this,
4429 kind,
4430 *mkValHelper<CVC4::BitVectorSignExtend>(
4431 CVC4::BitVectorSignExtend(arg))
4432 .d_node);
4433 break;
4434 case BITVECTOR_ROTATE_LEFT:
4435 res = Op(this,
4436 kind,
4437 *mkValHelper<CVC4::BitVectorRotateLeft>(
4438 CVC4::BitVectorRotateLeft(arg))
4439 .d_node);
4440 break;
4441 case BITVECTOR_ROTATE_RIGHT:
4442 res = Op(this,
4443 kind,
4444 *mkValHelper<CVC4::BitVectorRotateRight>(
4445 CVC4::BitVectorRotateRight(arg))
4446 .d_node);
4447 break;
4448 case INT_TO_BITVECTOR:
4449 res = Op(
4450 this,
4451 kind,
4452 *mkValHelper<CVC4::IntToBitVector>(CVC4::IntToBitVector(arg)).d_node);
4453 break;
4454 case IAND:
4455 res =
4456 Op(this, kind, *mkValHelper<CVC4::IntAnd>(CVC4::IntAnd(arg)).d_node);
4457 break;
4458 case FLOATINGPOINT_TO_UBV:
4459 res = Op(
4460 this,
4461 kind,
4462 *mkValHelper<CVC4::FloatingPointToUBV>(CVC4::FloatingPointToUBV(arg))
4463 .d_node);
4464 break;
4465 case FLOATINGPOINT_TO_SBV:
4466 res = Op(
4467 this,
4468 kind,
4469 *mkValHelper<CVC4::FloatingPointToSBV>(CVC4::FloatingPointToSBV(arg))
4470 .d_node);
4471 break;
4472 case TUPLE_UPDATE:
4473 res = Op(this,
4474 kind,
4475 *mkValHelper<CVC4::TupleUpdate>(CVC4::TupleUpdate(arg)).d_node);
4476 break;
4477 case REGEXP_REPEAT:
4478 res =
4479 Op(this,
4480 kind,
4481 *mkValHelper<CVC4::RegExpRepeat>(CVC4::RegExpRepeat(arg)).d_node);
4482 break;
4483 default:
4484 CVC4_API_KIND_CHECK_EXPECTED(false, kind)
4485 << "operator kind with uint32_t argument";
4486 }
4487 Assert(!res.isNull());
4488 return res;
4489
4490 CVC4_API_SOLVER_TRY_CATCH_END;
4491 }
4492
4493 Op Solver::mkOp(Kind kind, uint32_t arg1, uint32_t arg2) const
4494 {
4495 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4496 CVC4_API_KIND_CHECK(kind);
4497
4498 Op res;
4499 switch (kind)
4500 {
4501 case BITVECTOR_EXTRACT:
4502 res = Op(this,
4503 kind,
4504 *mkValHelper<CVC4::BitVectorExtract>(
4505 CVC4::BitVectorExtract(arg1, arg2))
4506 .d_node);
4507 break;
4508 case FLOATINGPOINT_TO_FP_IEEE_BITVECTOR:
4509 res = Op(this,
4510 kind,
4511 *mkValHelper<CVC4::FloatingPointToFPIEEEBitVector>(
4512 CVC4::FloatingPointToFPIEEEBitVector(arg1, arg2))
4513 .d_node);
4514 break;
4515 case FLOATINGPOINT_TO_FP_FLOATINGPOINT:
4516 res = Op(this,
4517 kind,
4518 *mkValHelper<CVC4::FloatingPointToFPFloatingPoint>(
4519 CVC4::FloatingPointToFPFloatingPoint(arg1, arg2))
4520 .d_node);
4521 break;
4522 case FLOATINGPOINT_TO_FP_REAL:
4523 res = Op(this,
4524 kind,
4525 *mkValHelper<CVC4::FloatingPointToFPReal>(
4526 CVC4::FloatingPointToFPReal(arg1, arg2))
4527 .d_node);
4528 break;
4529 case FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR:
4530 res = Op(this,
4531 kind,
4532 *mkValHelper<CVC4::FloatingPointToFPSignedBitVector>(
4533 CVC4::FloatingPointToFPSignedBitVector(arg1, arg2))
4534 .d_node);
4535 break;
4536 case FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR:
4537 res = Op(this,
4538 kind,
4539 *mkValHelper<CVC4::FloatingPointToFPUnsignedBitVector>(
4540 CVC4::FloatingPointToFPUnsignedBitVector(arg1, arg2))
4541 .d_node);
4542 break;
4543 case FLOATINGPOINT_TO_FP_GENERIC:
4544 res = Op(this,
4545 kind,
4546 *mkValHelper<CVC4::FloatingPointToFPGeneric>(
4547 CVC4::FloatingPointToFPGeneric(arg1, arg2))
4548 .d_node);
4549 break;
4550 case REGEXP_LOOP:
4551 res = Op(
4552 this,
4553 kind,
4554 *mkValHelper<CVC4::RegExpLoop>(CVC4::RegExpLoop(arg1, arg2)).d_node);
4555 break;
4556 default:
4557 CVC4_API_KIND_CHECK_EXPECTED(false, kind)
4558 << "operator kind with two uint32_t arguments";
4559 }
4560 Assert(!res.isNull());
4561 return res;
4562
4563 CVC4_API_SOLVER_TRY_CATCH_END;
4564 }
4565
4566 /* Non-SMT-LIB commands */
4567 /* -------------------------------------------------------------------------- */
4568
4569 Term Solver::simplify(const Term& term)
4570 {
4571 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4572 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4573 CVC4_API_ARG_CHECK_NOT_NULL(term);
4574 CVC4_API_SOLVER_CHECK_TERM(term);
4575
4576 return Term(this, d_smtEngine->simplify(term.d_node->toExpr()));
4577
4578 CVC4_API_SOLVER_TRY_CATCH_END;
4579 }
4580
4581 Result Solver::checkEntailed(Term term) const
4582 {
4583 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4584 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4585 CVC4_API_CHECK(!d_smtEngine->isQueryMade()
4586 || d_smtEngine->getOptions()[options::incrementalSolving])
4587 << "Cannot make multiple queries unless incremental solving is enabled "
4588 "(try --incremental)";
4589 CVC4_API_ARG_CHECK_NOT_NULL(term);
4590 CVC4_API_SOLVER_CHECK_TERM(term);
4591
4592 CVC4::Result r = d_smtEngine->checkEntailed(*term.d_node);
4593 return Result(r);
4594
4595 CVC4_API_SOLVER_TRY_CATCH_END;
4596 }
4597
4598 Result Solver::checkEntailed(const std::vector<Term>& terms) const
4599 {
4600 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4601 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4602 CVC4_API_CHECK(!d_smtEngine->isQueryMade()
4603 || d_smtEngine->getOptions()[options::incrementalSolving])
4604 << "Cannot make multiple queries unless incremental solving is enabled "
4605 "(try --incremental)";
4606 for (const Term& term : terms)
4607 {
4608 CVC4_API_SOLVER_CHECK_TERM(term);
4609 CVC4_API_ARG_CHECK_NOT_NULL(term);
4610 }
4611
4612 std::vector<Node> exprs = termVectorToNodes(terms);
4613 CVC4::Result r = d_smtEngine->checkEntailed(exprs);
4614 return Result(r);
4615
4616 CVC4_API_SOLVER_TRY_CATCH_END;
4617 }
4618
4619 /* SMT-LIB commands */
4620 /* -------------------------------------------------------------------------- */
4621
4622 /**
4623 * ( assert <term> )
4624 */
4625 void Solver::assertFormula(Term term) const
4626 {
4627 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4628 CVC4_API_SOLVER_CHECK_TERM(term);
4629 CVC4_API_ARG_CHECK_NOT_NULL(term);
4630 d_smtEngine->assertFormula(*term.d_node);
4631 CVC4_API_SOLVER_TRY_CATCH_END;
4632 }
4633
4634 /**
4635 * ( check-sat )
4636 */
4637 Result Solver::checkSat(void) const
4638 {
4639 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4640 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4641 CVC4_API_CHECK(!d_smtEngine->isQueryMade()
4642 || d_smtEngine->getOptions()[options::incrementalSolving])
4643 << "Cannot make multiple queries unless incremental solving is enabled "
4644 "(try --incremental)";
4645 CVC4::Result r = d_smtEngine->checkSat();
4646 return Result(r);
4647 CVC4_API_SOLVER_TRY_CATCH_END;
4648 }
4649
4650 /**
4651 * ( check-sat-assuming ( <prop_literal> ) )
4652 */
4653 Result Solver::checkSatAssuming(Term assumption) const
4654 {
4655 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4656 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4657 CVC4_API_CHECK(!d_smtEngine->isQueryMade()
4658 || d_smtEngine->getOptions()[options::incrementalSolving])
4659 << "Cannot make multiple queries unless incremental solving is enabled "
4660 "(try --incremental)";
4661 CVC4_API_SOLVER_CHECK_TERM(assumption);
4662 CVC4::Result r = d_smtEngine->checkSat(*assumption.d_node);
4663 return Result(r);
4664 CVC4_API_SOLVER_TRY_CATCH_END;
4665 }
4666
4667 /**
4668 * ( check-sat-assuming ( <prop_literal>* ) )
4669 */
4670 Result Solver::checkSatAssuming(const std::vector<Term>& assumptions) const
4671 {
4672 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4673 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
4674 CVC4_API_CHECK(!d_smtEngine->isQueryMade() || assumptions.size() == 0
4675 || d_smtEngine->getOptions()[options::incrementalSolving])
4676 << "Cannot make multiple queries unless incremental solving is enabled "
4677 "(try --incremental)";
4678 for (const Term& term : assumptions)
4679 {
4680 CVC4_API_SOLVER_CHECK_TERM(term);
4681 CVC4_API_ARG_CHECK_NOT_NULL(term);
4682 }
4683 std::vector<Node> eassumptions = termVectorToNodes(assumptions);
4684 CVC4::Result r = d_smtEngine->checkSat(eassumptions);
4685 return Result(r);
4686 CVC4_API_SOLVER_TRY_CATCH_END;
4687 }
4688
4689 /**
4690 * ( declare-datatype <symbol> <datatype_decl> )
4691 */
4692 Sort Solver::declareDatatype(
4693 const std::string& symbol,
4694 const std::vector<DatatypeConstructorDecl>& ctors) const
4695 {
4696 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4697 CVC4_API_ARG_CHECK_EXPECTED(ctors.size() > 0, ctors)
4698 << "a datatype declaration with at least one constructor";
4699 DatatypeDecl dtdecl(this, symbol);
4700 for (size_t i = 0, size = ctors.size(); i < size; i++)
4701 {
4702 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(this == ctors[i].d_solver,
4703 "datatype constructor declaration",
4704 ctors[i],
4705 i)
4706 << "datatype constructor declaration associated to this solver object";
4707 dtdecl.addConstructor(ctors[i]);
4708 }
4709 return Sort(this, getNodeManager()->mkDatatypeType(*dtdecl.d_dtype).toType());
4710 CVC4_API_SOLVER_TRY_CATCH_END;
4711 }
4712
4713 /**
4714 * ( declare-fun <symbol> ( <sort>* ) <sort> )
4715 */
4716 Term Solver::declareFun(const std::string& symbol,
4717 const std::vector<Sort>& sorts,
4718 Sort sort) const
4719 {
4720 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4721 for (size_t i = 0, size = sorts.size(); i < size; ++i)
4722 {
4723 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4724 this == sorts[i].d_solver, "parameter sort", sorts[i], i)
4725 << "parameter sort associated to this solver object";
4726 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4727 sorts[i].isFirstClass(), "parameter sort", sorts[i], i)
4728 << "first-class sort as parameter sort for function sort";
4729 }
4730 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
4731 << "first-class sort as function codomain sort";
4732 CVC4_API_SOLVER_CHECK_SORT(sort);
4733 Assert(!sort.isFunction()); /* A function sort is not first-class. */
4734 Type type = *sort.d_type;
4735 if (!sorts.empty())
4736 {
4737 std::vector<Type> types = sortVectorToTypes(sorts);
4738 type = d_exprMgr->mkFunctionType(types, type);
4739 }
4740 return Term(this, d_exprMgr->mkVar(symbol, type));
4741 CVC4_API_SOLVER_TRY_CATCH_END;
4742 }
4743
4744 /**
4745 * ( declare-sort <symbol> <numeral> )
4746 */
4747 Sort Solver::declareSort(const std::string& symbol, uint32_t arity) const
4748 {
4749 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4750 if (arity == 0) return Sort(this, d_exprMgr->mkSort(symbol));
4751 return Sort(this, d_exprMgr->mkSortConstructor(symbol, arity));
4752 CVC4_API_SOLVER_TRY_CATCH_END;
4753 }
4754
4755 /**
4756 * ( define-fun <function_def> )
4757 */
4758 Term Solver::defineFun(const std::string& symbol,
4759 const std::vector<Term>& bound_vars,
4760 Sort sort,
4761 Term term,
4762 bool global) const
4763 {
4764 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4765 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
4766 << "first-class sort as codomain sort for function sort";
4767 std::vector<TypeNode> domain_types;
4768 for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
4769 {
4770 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4771 this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
4772 << "bound variable associated to this solver object";
4773 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4774 bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
4775 "bound variable",
4776 bound_vars[i],
4777 i)
4778 << "a bound variable";
4779 CVC4::Type t = bound_vars[i].d_node->getType().toType();
4780 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4781 t.isFirstClass(), "sort of parameter", bound_vars[i], i)
4782 << "first-class sort of parameter of defined function";
4783 domain_types.push_back(TypeNode::fromType(t));
4784 }
4785 CVC4_API_SOLVER_CHECK_SORT(sort);
4786 CVC4_API_CHECK(sort == term.getSort())
4787 << "Invalid sort of function body '" << term << "', expected '" << sort
4788 << "'";
4789 NodeManager* nm = getNodeManager();
4790 TypeNode type = TypeNode::fromType(*sort.d_type);
4791 if (!domain_types.empty())
4792 {
4793 type = nm->mkFunctionType(domain_types, type);
4794 }
4795 Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
4796 std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
4797 d_smtEngine->defineFunction(fun, ebound_vars, *term.d_node, global);
4798 return Term(this, fun);
4799 CVC4_API_SOLVER_TRY_CATCH_END;
4800 }
4801
4802 Term Solver::defineFun(Term fun,
4803 const std::vector<Term>& bound_vars,
4804 Term term,
4805 bool global) const
4806 {
4807 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4808
4809 if (fun.getSort().isFunction())
4810 {
4811 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
4812 size_t size = bound_vars.size();
4813 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
4814 << "'" << domain_sorts.size() << "'";
4815 for (size_t i = 0; i < size; ++i)
4816 {
4817 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4818 this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
4819 << "bound variable associated to this solver object";
4820 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4821 bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
4822 "bound variable",
4823 bound_vars[i],
4824 i)
4825 << "a bound variable";
4826 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4827 domain_sorts[i] == bound_vars[i].getSort(),
4828 "sort of parameter",
4829 bound_vars[i],
4830 i)
4831 << "'" << domain_sorts[i] << "'";
4832 }
4833 Sort codomain = fun.getSort().getFunctionCodomainSort();
4834 CVC4_API_CHECK(codomain == term.getSort())
4835 << "Invalid sort of function body '" << term << "', expected '"
4836 << codomain << "'";
4837 }
4838 else
4839 {
4840 CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun)
4841 << "function or nullary symbol";
4842 }
4843
4844 CVC4_API_SOLVER_CHECK_TERM(term);
4845
4846 std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
4847 d_smtEngine->defineFunction(*fun.d_node, ebound_vars, *term.d_node, global);
4848 return fun;
4849 CVC4_API_SOLVER_TRY_CATCH_END;
4850 }
4851
4852 /**
4853 * ( define-fun-rec <function_def> )
4854 */
4855 Term Solver::defineFunRec(const std::string& symbol,
4856 const std::vector<Term>& bound_vars,
4857 Sort sort,
4858 Term term,
4859 bool global) const
4860 {
4861 NodeManagerScope scope(getNodeManager());
4862 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4863
4864 CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
4865 << "recursive function definitions require a logic with quantifiers";
4866 CVC4_API_CHECK(
4867 d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
4868 << "recursive function definitions require a logic with uninterpreted "
4869 "functions";
4870
4871 CVC4_API_ARG_CHECK_EXPECTED(sort.isFirstClass(), sort)
4872 << "first-class sort as function codomain sort";
4873 Assert(!sort.isFunction()); /* A function sort is not first-class. */
4874 std::vector<TypeNode> domain_types;
4875 for (size_t i = 0, size = bound_vars.size(); i < size; ++i)
4876 {
4877 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4878 this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
4879 << "bound variable associated to this solver object";
4880 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4881 bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
4882 "bound variable",
4883 bound_vars[i],
4884 i)
4885 << "a bound variable";
4886 CVC4::TypeNode t = bound_vars[i].d_node->getType();
4887 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4888 t.isFirstClass(), "sort of parameter", bound_vars[i], i)
4889 << "first-class sort of parameter of defined function";
4890 domain_types.push_back(t);
4891 }
4892 CVC4_API_SOLVER_CHECK_SORT(sort);
4893 CVC4_API_CHECK(sort == term.getSort())
4894 << "Invalid sort of function body '" << term << "', expected '" << sort
4895 << "'";
4896 CVC4_API_SOLVER_CHECK_TERM(term);
4897 NodeManager* nm = getNodeManager();
4898 TypeNode type = TypeNode::fromType(*sort.d_type);
4899 if (!domain_types.empty())
4900 {
4901 type = nm->mkFunctionType(domain_types, type);
4902 }
4903 Node fun = Node::fromExpr(d_exprMgr->mkVar(symbol, type.toType()));
4904 std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
4905 d_smtEngine->defineFunctionRec(
4906 fun, ebound_vars, term.d_node->toExpr(), global);
4907 return Term(this, fun);
4908 CVC4_API_SOLVER_TRY_CATCH_END;
4909 }
4910
4911 Term Solver::defineFunRec(Term fun,
4912 const std::vector<Term>& bound_vars,
4913 Term term,
4914 bool global) const
4915 {
4916 NodeManagerScope scope(getNodeManager());
4917 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4918
4919 CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
4920 << "recursive function definitions require a logic with quantifiers";
4921 CVC4_API_CHECK(
4922 d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
4923 << "recursive function definitions require a logic with uninterpreted "
4924 "functions";
4925
4926 if (fun.getSort().isFunction())
4927 {
4928 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
4929 size_t size = bound_vars.size();
4930 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars)
4931 << "'" << domain_sorts.size() << "'";
4932 for (size_t i = 0; i < size; ++i)
4933 {
4934 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4935 this == bound_vars[i].d_solver, "bound variable", bound_vars[i], i)
4936 << "bound variable associated to this solver object";
4937 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4938 bound_vars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
4939 "bound variable",
4940 bound_vars[i],
4941 i)
4942 << "a bound variable";
4943 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4944 domain_sorts[i] == bound_vars[i].getSort(),
4945 "sort of parameter",
4946 bound_vars[i],
4947 i)
4948 << "'" << domain_sorts[i] << "'";
4949 }
4950 Sort codomain = fun.getSort().getFunctionCodomainSort();
4951 CVC4_API_CHECK(codomain == term.getSort())
4952 << "Invalid sort of function body '" << term << "', expected '"
4953 << codomain << "'";
4954 }
4955 else
4956 {
4957 CVC4_API_ARG_CHECK_EXPECTED(bound_vars.size() == 0, fun)
4958 << "function or nullary symbol";
4959 }
4960
4961 CVC4_API_SOLVER_CHECK_TERM(term);
4962 std::vector<Node> ebound_vars = termVectorToNodes(bound_vars);
4963 d_smtEngine->defineFunctionRec(
4964 *fun.d_node, ebound_vars, *term.d_node, global);
4965 return fun;
4966 CVC4_API_SOLVER_TRY_CATCH_END;
4967 }
4968
4969 /**
4970 * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
4971 */
4972 void Solver::defineFunsRec(const std::vector<Term>& funs,
4973 const std::vector<std::vector<Term>>& bound_vars,
4974 const std::vector<Term>& terms,
4975 bool global) const
4976 {
4977 NodeManagerScope scope(getNodeManager());
4978 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
4979
4980 CVC4_API_CHECK(d_smtEngine->getUserLogicInfo().isQuantified())
4981 << "recursive function definitions require a logic with quantifiers";
4982 CVC4_API_CHECK(
4983 d_smtEngine->getUserLogicInfo().isTheoryEnabled(theory::THEORY_UF))
4984 << "recursive function definitions require a logic with uninterpreted "
4985 "functions";
4986
4987 size_t funs_size = funs.size();
4988 CVC4_API_ARG_SIZE_CHECK_EXPECTED(funs_size == bound_vars.size(), bound_vars)
4989 << "'" << funs_size << "'";
4990 for (size_t j = 0; j < funs_size; ++j)
4991 {
4992 const Term& fun = funs[j];
4993 const std::vector<Term>& bvars = bound_vars[j];
4994 const Term& term = terms[j];
4995
4996 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
4997 this == fun.d_solver, "function", fun, j)
4998 << "function associated to this solver object";
4999 CVC4_API_SOLVER_CHECK_TERM(term);
5000
5001 if (fun.getSort().isFunction())
5002 {
5003 std::vector<Sort> domain_sorts = fun.getSort().getFunctionDomainSorts();
5004 size_t size = bvars.size();
5005 CVC4_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bvars)
5006 << "'" << domain_sorts.size() << "'";
5007 for (size_t i = 0; i < size; ++i)
5008 {
5009 for (size_t k = 0, nbvars = bvars.size(); k < nbvars; ++k)
5010 {
5011 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5012 this == bvars[k].d_solver, "bound variable", bvars[k], k)
5013 << "bound variable associated to this solver object";
5014 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5015 bvars[k].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
5016 "bound variable",
5017 bvars[k],
5018 k)
5019 << "a bound variable";
5020 }
5021 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5022 domain_sorts[i] == bvars[i].getSort(),
5023 "sort of parameter",
5024 bvars[i],
5025 i)
5026 << "'" << domain_sorts[i] << "' in parameter bound_vars[" << j
5027 << "]";
5028 }
5029 Sort codomain = fun.getSort().getFunctionCodomainSort();
5030 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5031 codomain == term.getSort(), "sort of function body", term, j)
5032 << "'" << codomain << "'";
5033 }
5034 else
5035 {
5036 CVC4_API_ARG_CHECK_EXPECTED(bvars.size() == 0, fun)
5037 << "function or nullary symbol";
5038 }
5039 }
5040 std::vector<Node> efuns = termVectorToNodes(funs);
5041 std::vector<std::vector<Node>> ebound_vars;
5042 for (const auto& v : bound_vars)
5043 {
5044 ebound_vars.push_back(termVectorToNodes(v));
5045 }
5046 std::vector<Node> exprs = termVectorToNodes(terms);
5047 d_smtEngine->defineFunctionsRec(efuns, ebound_vars, exprs, global);
5048 CVC4_API_SOLVER_TRY_CATCH_END;
5049 }
5050
5051 /**
5052 * ( echo <std::string> )
5053 */
5054 void Solver::echo(std::ostream& out, const std::string& str) const
5055 {
5056 out << str;
5057 }
5058
5059 /**
5060 * ( get-assertions )
5061 */
5062 std::vector<Term> Solver::getAssertions(void) const
5063 {
5064 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5065 std::vector<Node> assertions = d_smtEngine->getAssertions();
5066 /* Can not use
5067 * return std::vector<Term>(assertions.begin(), assertions.end());
5068 * here since constructor is private */
5069 std::vector<Term> res;
5070 for (const Node& e : assertions)
5071 {
5072 res.push_back(Term(this, e));
5073 }
5074 return res;
5075 CVC4_API_SOLVER_TRY_CATCH_END;
5076 }
5077
5078 /**
5079 * ( get-info <info_flag> )
5080 */
5081 std::string Solver::getInfo(const std::string& flag) const
5082 {
5083 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5084 CVC4_API_CHECK(d_smtEngine->isValidGetInfoFlag(flag))
5085 << "Unrecognized flag for getInfo.";
5086
5087 return d_smtEngine->getInfo(flag).toString();
5088 CVC4_API_SOLVER_TRY_CATCH_END;
5089 }
5090
5091 /**
5092 * ( get-option <keyword> )
5093 */
5094 std::string Solver::getOption(const std::string& option) const
5095 {
5096 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5097 SExpr res = d_smtEngine->getOption(option);
5098 return res.toString();
5099 CVC4_API_SOLVER_TRY_CATCH_END;
5100 }
5101
5102 /**
5103 * ( get-unsat-assumptions )
5104 */
5105 std::vector<Term> Solver::getUnsatAssumptions(void) const
5106 {
5107 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5108 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5109 CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
5110 << "Cannot get unsat assumptions unless incremental solving is enabled "
5111 "(try --incremental)";
5112 CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatAssumptions])
5113 << "Cannot get unsat assumptions unless explicitly enabled "
5114 "(try --produce-unsat-assumptions)";
5115 CVC4_API_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
5116 << "Cannot get unsat assumptions unless in unsat mode.";
5117
5118 std::vector<Node> uassumptions = d_smtEngine->getUnsatAssumptions();
5119 /* Can not use
5120 * return std::vector<Term>(uassumptions.begin(), uassumptions.end());
5121 * here since constructor is private */
5122 std::vector<Term> res;
5123 for (const Node& e : uassumptions)
5124 {
5125 res.push_back(Term(this, e.toExpr()));
5126 }
5127 return res;
5128 CVC4_API_SOLVER_TRY_CATCH_END;
5129 }
5130
5131 /**
5132 * ( get-unsat-core )
5133 */
5134 std::vector<Term> Solver::getUnsatCore(void) const
5135 {
5136 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5137 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5138 CVC4_API_CHECK(d_smtEngine->getOptions()[options::unsatCores])
5139 << "Cannot get unsat core unless explicitly enabled "
5140 "(try --produce-unsat-cores)";
5141 CVC4_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
5142 << "Cannot get unsat core unless in unsat mode.";
5143 UnsatCore core = d_smtEngine->getUnsatCore();
5144 /* Can not use
5145 * return std::vector<Term>(core.begin(), core.end());
5146 * here since constructor is private */
5147 std::vector<Term> res;
5148 for (const Expr& e : core)
5149 {
5150 res.push_back(Term(this, e));
5151 }
5152 return res;
5153 CVC4_API_SOLVER_TRY_CATCH_END;
5154 }
5155
5156 /**
5157 * ( get-value ( <term> ) )
5158 */
5159 Term Solver::getValue(Term term) const
5160 {
5161 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5162 CVC4_API_SOLVER_CHECK_TERM(term);
5163 return Term(this, d_smtEngine->getValue(*term.d_node));
5164 CVC4_API_SOLVER_TRY_CATCH_END;
5165 }
5166
5167 /**
5168 * ( get-value ( <term>+ ) )
5169 */
5170 std::vector<Term> Solver::getValue(const std::vector<Term>& terms) const
5171 {
5172 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5173 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5174 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5175 << "Cannot get value unless model generation is enabled "
5176 "(try --produce-models)";
5177 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5178 << "Cannot get value when in unsat mode.";
5179 std::vector<Term> res;
5180 for (size_t i = 0, n = terms.size(); i < n; ++i)
5181 {
5182 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5183 this == terms[i].d_solver, "term", terms[i], i)
5184 << "term associated to this solver object";
5185 /* Can not use emplace_back here since constructor is private. */
5186 res.push_back(Term(this, d_smtEngine->getValue(terms[i].d_node->toExpr())));
5187 }
5188 return res;
5189 CVC4_API_SOLVER_TRY_CATCH_END;
5190 }
5191
5192 Term Solver::getQuantifierElimination(api::Term q) const
5193 {
5194 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5195 CVC4_API_ARG_CHECK_NOT_NULL(q);
5196 CVC4_API_SOLVER_CHECK_TERM(q);
5197 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5198 return Term(this,
5199 d_smtEngine->getQuantifierElimination(q.getNode(), true, true));
5200 CVC4_API_SOLVER_TRY_CATCH_END;
5201 }
5202
5203 Term Solver::getQuantifierEliminationDisjunct(api::Term q) const
5204 {
5205 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5206 CVC4_API_ARG_CHECK_NOT_NULL(q);
5207 CVC4_API_SOLVER_CHECK_TERM(q);
5208 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5209 return Term(
5210 this, d_smtEngine->getQuantifierElimination(q.getNode(), false, true));
5211 CVC4_API_SOLVER_TRY_CATCH_END;
5212 }
5213
5214 Term Solver::getSeparationHeap() const
5215 {
5216 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5217 CVC4_API_CHECK(
5218 d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
5219 << "Cannot obtain separation logic expressions if not using the "
5220 "separation logic theory.";
5221 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5222 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5223 << "Cannot get separation heap term unless model generation is enabled "
5224 "(try --produce-models)";
5225 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5226 << "Cannot get separtion heap term when in unsat mode.";
5227 return Term(this, d_smtEngine->getSepHeapExpr());
5228 CVC4_API_SOLVER_TRY_CATCH_END;
5229 }
5230
5231 Term Solver::getSeparationNilTerm() const
5232 {
5233 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5234 CVC4_API_CHECK(
5235 d_smtEngine->getLogicInfo().isTheoryEnabled(theory::THEORY_SEP))
5236 << "Cannot obtain separation logic expressions if not using the "
5237 "separation logic theory.";
5238 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5239 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5240 << "Cannot get separation nil term unless model generation is enabled "
5241 "(try --produce-models)";
5242 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5243 << "Cannot get separtion nil term when in unsat mode.";
5244 return Term(this, d_smtEngine->getSepNilExpr());
5245 CVC4_API_SOLVER_TRY_CATCH_END;
5246 }
5247
5248 /**
5249 * ( pop <numeral> )
5250 */
5251 void Solver::pop(uint32_t nscopes) const
5252 {
5253 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5254 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5255 CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
5256 << "Cannot pop when not solving incrementally (use --incremental)";
5257 CVC4_API_CHECK(nscopes <= d_smtEngine->getNumUserLevels())
5258 << "Cannot pop beyond first pushed context";
5259
5260 for (uint32_t n = 0; n < nscopes; ++n)
5261 {
5262 d_smtEngine->pop();
5263 }
5264
5265 CVC4_API_SOLVER_TRY_CATCH_END;
5266 }
5267
5268 bool Solver::getInterpolant(Term conj, Term& output) const
5269 {
5270 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5271 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5272 Node result;
5273 bool success = d_smtEngine->getInterpol(*conj.d_node, result);
5274 if (success)
5275 {
5276 output = Term(this, result);
5277 }
5278 return success;
5279 CVC4_API_SOLVER_TRY_CATCH_END;
5280 }
5281
5282 bool Solver::getInterpolant(Term conj, Grammar& g, Term& output) const
5283 {
5284 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5285 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5286 Node result;
5287 bool success = d_smtEngine->getInterpol(
5288 *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
5289 if (success)
5290 {
5291 output = Term(this, result);
5292 }
5293 return success;
5294 CVC4_API_SOLVER_TRY_CATCH_END;
5295 }
5296
5297 bool Solver::getAbduct(Term conj, Term& output) const
5298 {
5299 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5300 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5301 Node result;
5302 bool success = d_smtEngine->getAbduct(*conj.d_node, result);
5303 if (success)
5304 {
5305 output = Term(this, result);
5306 }
5307 return success;
5308 CVC4_API_SOLVER_TRY_CATCH_END;
5309 }
5310
5311 bool Solver::getAbduct(Term conj, Grammar& g, Term& output) const
5312 {
5313 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5314 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5315 Node result;
5316 bool success = d_smtEngine->getAbduct(
5317 *conj.d_node, TypeNode::fromType(*g.resolve().d_type), result);
5318 if (success)
5319 {
5320 output = Term(this, result);
5321 }
5322 return success;
5323 CVC4_API_SOLVER_TRY_CATCH_END;
5324 }
5325
5326 void Solver::printModel(std::ostream& out) const
5327 {
5328 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5329 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5330 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5331 << "Cannot get value unless model generation is enabled "
5332 "(try --produce-models)";
5333 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5334 << "Cannot get value when in unsat mode.";
5335 out << *d_smtEngine->getModel();
5336 CVC4_API_SOLVER_TRY_CATCH_END;
5337 }
5338
5339 void Solver::blockModel() const
5340 {
5341 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5342 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5343 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5344 << "Cannot get value unless model generation is enabled "
5345 "(try --produce-models)";
5346 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5347 << "Cannot get value when in unsat mode.";
5348 d_smtEngine->blockModel();
5349 CVC4_API_SOLVER_TRY_CATCH_END;
5350 }
5351
5352 void Solver::blockModelValues(const std::vector<Term>& terms) const
5353 {
5354 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5355 CVC4_API_CHECK(d_smtEngine->getOptions()[options::produceModels])
5356 << "Cannot get value unless model generation is enabled "
5357 "(try --produce-models)";
5358 CVC4_API_CHECK(d_smtEngine->getSmtMode() != SmtMode::UNSAT)
5359 << "Cannot get value when in unsat mode.";
5360 CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms)
5361 << "a non-empty set of terms";
5362 for (size_t i = 0, tsize = terms.size(); i < tsize; ++i)
5363 {
5364 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5365 !terms[i].isNull(), "term", terms[i], i)
5366 << "a non-null term";
5367 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5368 this == terms[i].d_solver, "term", terms[i], i)
5369 << "a term associated to this solver object";
5370 }
5371 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5372 d_smtEngine->blockModelValues(termVectorToNodes(terms));
5373 CVC4_API_SOLVER_TRY_CATCH_END;
5374 }
5375
5376 void Solver::printInstantiations(std::ostream& out) const
5377 {
5378 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5379 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5380 d_smtEngine->printInstantiations(out);
5381 CVC4_API_SOLVER_TRY_CATCH_END;
5382 }
5383
5384 /**
5385 * ( push <numeral> )
5386 */
5387 void Solver::push(uint32_t nscopes) const
5388 {
5389 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5390 CVC4::ExprManagerScope exmgrs(*(d_exprMgr.get()));
5391 CVC4_API_CHECK(d_smtEngine->getOptions()[options::incrementalSolving])
5392 << "Cannot push when not solving incrementally (use --incremental)";
5393
5394 for (uint32_t n = 0; n < nscopes; ++n)
5395 {
5396 d_smtEngine->push();
5397 }
5398
5399 CVC4_API_SOLVER_TRY_CATCH_END;
5400 }
5401
5402 /**
5403 * ( reset-assertions )
5404 */
5405 void Solver::resetAssertions(void) const
5406 {
5407 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5408 d_smtEngine->resetAssertions();
5409 CVC4_API_SOLVER_TRY_CATCH_END;
5410 }
5411
5412 /**
5413 * ( set-info <attribute> )
5414 */
5415 void Solver::setInfo(const std::string& keyword, const std::string& value) const
5416 {
5417 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5418 CVC4_API_ARG_CHECK_EXPECTED(
5419 keyword == "source" || keyword == "category" || keyword == "difficulty"
5420 || keyword == "filename" || keyword == "license" || keyword == "name"
5421 || keyword == "notes" || keyword == "smt-lib-version"
5422 || keyword == "status",
5423 keyword)
5424 << "'source', 'category', 'difficulty', 'filename', 'license', 'name', "
5425 "'notes', 'smt-lib-version' or 'status'";
5426 CVC4_API_ARG_CHECK_EXPECTED(keyword != "smt-lib-version" || value == "2"
5427 || value == "2.0" || value == "2.5"
5428 || value == "2.6",
5429 value)
5430 << "'2.0', '2.5', '2.6'";
5431 CVC4_API_ARG_CHECK_EXPECTED(keyword != "status" || value == "sat"
5432 || value == "unsat" || value == "unknown",
5433 value)
5434 << "'sat', 'unsat' or 'unknown'";
5435
5436 d_smtEngine->setInfo(keyword, value);
5437 CVC4_API_SOLVER_TRY_CATCH_END;
5438 }
5439
5440 /**
5441 * ( set-logic <symbol> )
5442 */
5443 void Solver::setLogic(const std::string& logic) const
5444 {
5445 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5446 CVC4_API_CHECK(!d_smtEngine->isFullyInited())
5447 << "Invalid call to 'setLogic', solver is already fully initialized";
5448 CVC4::LogicInfo logic_info(logic);
5449 d_smtEngine->setLogic(logic_info);
5450 CVC4_API_SOLVER_TRY_CATCH_END;
5451 }
5452
5453 /**
5454 * ( set-option <option> )
5455 */
5456 void Solver::setOption(const std::string& option,
5457 const std::string& value) const
5458 {
5459 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5460 CVC4_API_CHECK(!d_smtEngine->isFullyInited())
5461 << "Invalid call to 'setOption', solver is already fully initialized";
5462 d_smtEngine->setOption(option, value);
5463 CVC4_API_SOLVER_TRY_CATCH_END;
5464 }
5465
5466 Term Solver::ensureTermSort(const Term& term, const Sort& sort) const
5467 {
5468 CVC4_API_CHECK(term.getSort() == sort
5469 || (term.getSort().isInteger() && sort.isReal()))
5470 << "Expected conversion from Int to Real";
5471
5472 Sort t = term.getSort();
5473 if (term.getSort() == sort)
5474 {
5475 return term;
5476 }
5477
5478 // Integers are reals, too
5479 Assert(t.isReal());
5480 Term res = term;
5481 if (t.isInteger())
5482 {
5483 // Must cast to Real to ensure correct type is passed to parametric type
5484 // constructors. We do this cast using division with 1. This has the
5485 // advantage wrt using TO_REAL since (constant) division is always included
5486 // in the theory.
5487 res = Term(this,
5488 d_exprMgr->mkExpr(extToIntKind(DIVISION),
5489 res.d_node->toExpr(),
5490 d_exprMgr->mkConst(CVC4::Rational(1))));
5491 }
5492 Assert(res.getSort() == sort);
5493 return res;
5494 }
5495
5496 Term Solver::mkSygusVar(Sort sort, const std::string& symbol) const
5497 {
5498 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5499 CVC4_API_ARG_CHECK_NOT_NULL(sort);
5500 CVC4_API_SOLVER_CHECK_SORT(sort);
5501
5502 Expr res = d_exprMgr->mkBoundVar(symbol, *sort.d_type);
5503 (void)res.getType(true); /* kick off type checking */
5504
5505 d_smtEngine->declareSygusVar(symbol, res, TypeNode::fromType(*sort.d_type));
5506
5507 return Term(this, res);
5508
5509 CVC4_API_SOLVER_TRY_CATCH_END;
5510 }
5511
5512 Grammar Solver::mkSygusGrammar(const std::vector<Term>& boundVars,
5513 const std::vector<Term>& ntSymbols) const
5514 {
5515 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5516 CVC4_API_ARG_SIZE_CHECK_EXPECTED(!ntSymbols.empty(), ntSymbols)
5517 << "a non-empty vector";
5518
5519 for (size_t i = 0, n = boundVars.size(); i < n; ++i)
5520 {
5521 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5522 this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
5523 << "bound variable associated to this solver object";
5524 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5525 !boundVars[i].isNull(), "bound variable", boundVars[i], i)
5526 << "a non-null term";
5527 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5528 boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
5529 "bound variable",
5530 boundVars[i],
5531 i)
5532 << "a bound variable";
5533 }
5534
5535 for (size_t i = 0, n = ntSymbols.size(); i < n; ++i)
5536 {
5537 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5538 this == ntSymbols[i].d_solver, "non-terminal", ntSymbols[i], i)
5539 << "term associated to this solver object";
5540 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5541 !ntSymbols[i].isNull(), "non-terminal", ntSymbols[i], i)
5542 << "a non-null term";
5543 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5544 ntSymbols[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
5545 "non-terminal",
5546 ntSymbols[i],
5547 i)
5548 << "a bound variable";
5549 }
5550
5551 return Grammar(this, boundVars, ntSymbols);
5552 CVC4_API_SOLVER_TRY_CATCH_END;
5553 }
5554
5555 Term Solver::synthFun(const std::string& symbol,
5556 const std::vector<Term>& boundVars,
5557 Sort sort) const
5558 {
5559 return synthFunHelper(symbol, boundVars, sort);
5560 }
5561
5562 Term Solver::synthFun(const std::string& symbol,
5563 const std::vector<Term>& boundVars,
5564 Sort sort,
5565 Grammar& g) const
5566 {
5567 return synthFunHelper(symbol, boundVars, sort, false, &g);
5568 }
5569
5570 Term Solver::synthInv(const std::string& symbol,
5571 const std::vector<Term>& boundVars) const
5572 {
5573 return synthFunHelper(
5574 symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true);
5575 }
5576
5577 Term Solver::synthInv(const std::string& symbol,
5578 const std::vector<Term>& boundVars,
5579 Grammar& g) const
5580 {
5581 return synthFunHelper(
5582 symbol, boundVars, Sort(this, d_exprMgr->booleanType()), true, &g);
5583 }
5584
5585 Term Solver::synthFunHelper(const std::string& symbol,
5586 const std::vector<Term>& boundVars,
5587 const Sort& sort,
5588 bool isInv,
5589 Grammar* g) const
5590 {
5591 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5592 CVC4_API_ARG_CHECK_NOT_NULL(sort);
5593
5594 std::vector<Type> varTypes;
5595 for (size_t i = 0, n = boundVars.size(); i < n; ++i)
5596 {
5597 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5598 this == boundVars[i].d_solver, "bound variable", boundVars[i], i)
5599 << "bound variable associated to this solver object";
5600 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5601 !boundVars[i].isNull(), "bound variable", boundVars[i], i)
5602 << "a non-null term";
5603 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5604 boundVars[i].d_node->getKind() == CVC4::Kind::BOUND_VARIABLE,
5605 "bound variable",
5606 boundVars[i],
5607 i)
5608 << "a bound variable";
5609 varTypes.push_back(boundVars[i].d_node->getType().toType());
5610 }
5611 CVC4_API_SOLVER_CHECK_SORT(sort);
5612
5613 if (g != nullptr)
5614 {
5615 CVC4_API_CHECK(g->d_ntSyms[0].d_node->getType().toType() == *sort.d_type)
5616 << "Invalid Start symbol for Grammar g, Expected Start's sort to be "
5617 << *sort.d_type << " but found " << g->d_ntSyms[0].d_node->getType();
5618 }
5619
5620 Type funType = varTypes.empty()
5621 ? *sort.d_type
5622 : d_exprMgr->mkFunctionType(varTypes, *sort.d_type);
5623
5624 Node fun = getNodeManager()->mkBoundVar(symbol, TypeNode::fromType(funType));
5625 (void)fun.getType(true); /* kick off type checking */
5626
5627 std::vector<Node> bvns;
5628 for (const Term& t : boundVars)
5629 {
5630 bvns.push_back(*t.d_node);
5631 }
5632
5633 d_smtEngine->declareSynthFun(
5634 symbol,
5635 fun,
5636 TypeNode::fromType(g == nullptr ? funType : *g->resolve().d_type),
5637 isInv,
5638 bvns);
5639
5640 return Term(this, fun);
5641
5642 CVC4_API_SOLVER_TRY_CATCH_END;
5643 }
5644
5645 void Solver::addSygusConstraint(Term term) const
5646 {
5647 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5648 NodeManagerScope scope(getNodeManager());
5649 CVC4_API_ARG_CHECK_NOT_NULL(term);
5650 CVC4_API_SOLVER_CHECK_TERM(term);
5651 CVC4_API_ARG_CHECK_EXPECTED(
5652 term.d_node->getType() == getNodeManager()->booleanType(), term)
5653 << "boolean term";
5654
5655 d_smtEngine->assertSygusConstraint(*term.d_node);
5656 CVC4_API_SOLVER_TRY_CATCH_END;
5657 }
5658
5659 void Solver::addSygusInvConstraint(Term inv,
5660 Term pre,
5661 Term trans,
5662 Term post) const
5663 {
5664 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5665 CVC4_API_ARG_CHECK_NOT_NULL(inv);
5666 CVC4_API_SOLVER_CHECK_TERM(inv);
5667 CVC4_API_ARG_CHECK_NOT_NULL(pre);
5668 CVC4_API_SOLVER_CHECK_TERM(pre);
5669 CVC4_API_ARG_CHECK_NOT_NULL(trans);
5670 CVC4_API_SOLVER_CHECK_TERM(trans);
5671 CVC4_API_ARG_CHECK_NOT_NULL(post);
5672 CVC4_API_SOLVER_CHECK_TERM(post);
5673
5674 CVC4_API_ARG_CHECK_EXPECTED(inv.d_node->getType().isFunction(), inv)
5675 << "a function";
5676
5677 FunctionType invType = inv.d_node->getType().toType();
5678
5679 CVC4_API_ARG_CHECK_EXPECTED(invType.getRangeType().isBoolean(), inv)
5680 << "boolean range";
5681
5682 CVC4_API_CHECK(pre.d_node->getType().toType() == invType)
5683 << "Expected inv and pre to have the same sort";
5684
5685 CVC4_API_CHECK(post.d_node->getType().toType() == invType)
5686 << "Expected inv and post to have the same sort";
5687
5688 const std::vector<Type>& invArgTypes = invType.getArgTypes();
5689
5690 std::vector<Type> expectedTypes;
5691 expectedTypes.reserve(2 * invType.getArity() + 1);
5692
5693 for (size_t i = 0, n = invArgTypes.size(); i < 2 * n; i += 2)
5694 {
5695 expectedTypes.push_back(invArgTypes[i % n]);
5696 expectedTypes.push_back(invArgTypes[(i + 1) % n]);
5697 }
5698
5699 expectedTypes.push_back(invType.getRangeType());
5700 FunctionType expectedTransType = d_exprMgr->mkFunctionType(expectedTypes);
5701
5702 CVC4_API_CHECK(trans.d_node->toExpr().getType() == expectedTransType)
5703 << "Expected trans's sort to be " << invType;
5704
5705 d_smtEngine->assertSygusInvConstraint(inv.d_node->toExpr(),
5706 pre.d_node->toExpr(),
5707 trans.d_node->toExpr(),
5708 post.d_node->toExpr());
5709 CVC4_API_SOLVER_TRY_CATCH_END;
5710 }
5711
5712 Result Solver::checkSynth() const
5713 {
5714 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5715 return d_smtEngine->checkSynth();
5716 CVC4_API_SOLVER_TRY_CATCH_END;
5717 }
5718
5719 Term Solver::getSynthSolution(Term term) const
5720 {
5721 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5722 CVC4_API_ARG_CHECK_NOT_NULL(term);
5723 CVC4_API_SOLVER_CHECK_TERM(term);
5724
5725 std::map<CVC4::Node, CVC4::Node> map;
5726 CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
5727 << "The solver is not in a state immediately preceded by a "
5728 "successful call to checkSynth";
5729
5730 std::map<CVC4::Node, CVC4::Node>::const_iterator it = map.find(*term.d_node);
5731
5732 CVC4_API_CHECK(it != map.cend()) << "Synth solution not found for given term";
5733
5734 return Term(this, it->second);
5735 CVC4_API_SOLVER_TRY_CATCH_END;
5736 }
5737
5738 std::vector<Term> Solver::getSynthSolutions(
5739 const std::vector<Term>& terms) const
5740 {
5741 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5742 CVC4_API_ARG_SIZE_CHECK_EXPECTED(!terms.empty(), terms) << "non-empty vector";
5743
5744 for (size_t i = 0, n = terms.size(); i < n; ++i)
5745 {
5746 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5747 this == terms[i].d_solver, "parameter term", terms[i], i)
5748 << "parameter term associated to this solver object";
5749 CVC4_API_ARG_AT_INDEX_CHECK_EXPECTED(
5750 !terms[i].isNull(), "parameter term", terms[i], i)
5751 << "non-null term";
5752 }
5753
5754 std::map<CVC4::Node, CVC4::Node> map;
5755 CVC4_API_CHECK(d_smtEngine->getSynthSolutions(map))
5756 << "The solver is not in a state immediately preceded by a "
5757 "successful call to checkSynth";
5758
5759 std::vector<Term> synthSolution;
5760 synthSolution.reserve(terms.size());
5761
5762 for (size_t i = 0, n = terms.size(); i < n; ++i)
5763 {
5764 std::map<CVC4::Node, CVC4::Node>::const_iterator it =
5765 map.find(*terms[i].d_node);
5766
5767 CVC4_API_CHECK(it != map.cend())
5768 << "Synth solution not found for term at index " << i;
5769
5770 synthSolution.push_back(Term(this, it->second));
5771 }
5772
5773 return synthSolution;
5774 CVC4_API_SOLVER_TRY_CATCH_END;
5775 }
5776
5777 void Solver::printSynthSolution(std::ostream& out) const
5778 {
5779 CVC4_API_SOLVER_TRY_CATCH_BEGIN;
5780 d_smtEngine->printSynthSolution(out);
5781 CVC4_API_SOLVER_TRY_CATCH_END;
5782 }
5783
5784 /**
5785 * !!! This is only temporarily available until the parser is fully migrated to
5786 * the new API. !!!
5787 */
5788 ExprManager* Solver::getExprManager(void) const { return d_exprMgr.get(); }
5789
5790 /**
5791 * !!! This is only temporarily available until the parser is fully migrated to
5792 * the new API. !!!
5793 */
5794 NodeManager* Solver::getNodeManager(void) const
5795 {
5796 return d_exprMgr->getNodeManager();
5797 }
5798
5799 /**
5800 * !!! This is only temporarily available until the parser is fully migrated to
5801 * the new API. !!!
5802 */
5803 SmtEngine* Solver::getSmtEngine(void) const { return d_smtEngine.get(); }
5804
5805 /**
5806 * !!! This is only temporarily available until the parser is fully migrated to
5807 * the new API. !!!
5808 */
5809 Options& Solver::getOptions(void) { return d_smtEngine->getOptions(); }
5810
5811 /* -------------------------------------------------------------------------- */
5812 /* Conversions */
5813 /* -------------------------------------------------------------------------- */
5814
5815 std::vector<Expr> termVectorToExprs(const std::vector<Term>& terms)
5816 {
5817 std::vector<Expr> exprs;
5818 for (size_t i = 0, tsize = terms.size(); i < tsize; i++)
5819 {
5820 exprs.push_back(terms[i].getExpr());
5821 }
5822 return exprs;
5823 }
5824
5825 std::vector<Node> termVectorToNodes(const std::vector<Term>& terms)
5826 {
5827 std::vector<Node> res;
5828 for (const Term& t : terms)
5829 {
5830 res.push_back(t.getNode());
5831 }
5832 return res;
5833 }
5834
5835 std::vector<Type> sortVectorToTypes(const std::vector<Sort>& sorts)
5836 {
5837 std::vector<Type> types;
5838 for (size_t i = 0, ssize = sorts.size(); i < ssize; i++)
5839 {
5840 types.push_back(sorts[i].getType());
5841 }
5842 return types;
5843 }
5844
5845 std::vector<TypeNode> sortVectorToTypeNodes(const std::vector<Sort>& sorts)
5846 {
5847 std::vector<TypeNode> typeNodes;
5848 for (const Sort& sort : sorts)
5849 {
5850 typeNodes.push_back(TypeNode::fromType(sort.getType()));
5851 }
5852 return typeNodes;
5853 }
5854
5855 std::set<Type> sortSetToTypes(const std::set<Sort>& sorts)
5856 {
5857 std::set<Type> types;
5858 for (const Sort& s : sorts)
5859 {
5860 types.insert(s.getType());
5861 }
5862 return types;
5863 }
5864
5865 std::vector<Term> exprVectorToTerms(const Solver* slv,
5866 const std::vector<Expr>& exprs)
5867 {
5868 std::vector<Term> terms;
5869 for (size_t i = 0, esize = exprs.size(); i < esize; i++)
5870 {
5871 terms.push_back(Term(slv, exprs[i]));
5872 }
5873 return terms;
5874 }
5875
5876 std::vector<Sort> typeVectorToSorts(const Solver* slv,
5877 const std::vector<Type>& types)
5878 {
5879 std::vector<Sort> sorts;
5880 for (size_t i = 0, tsize = types.size(); i < tsize; i++)
5881 {
5882 sorts.push_back(Sort(slv, types[i]));
5883 }
5884 return sorts;
5885 }
5886
5887 } // namespace api
5888
5889 /* -------------------------------------------------------------------------- */
5890 /* Kind Conversions */
5891 /* -------------------------------------------------------------------------- */
5892
5893 CVC4::api::Kind intToExtKind(CVC4::Kind k)
5894 {
5895 auto it = api::s_kinds_internal.find(k);
5896 if (it == api::s_kinds_internal.end())
5897 {
5898 return api::INTERNAL_KIND;
5899 }
5900 return it->second;
5901 }
5902
5903 CVC4::Kind extToIntKind(CVC4::api::Kind k)
5904 {
5905 auto it = api::s_kinds.find(k);
5906 if (it == api::s_kinds.end())
5907 {
5908 return CVC4::Kind::UNDEFINED_KIND;
5909 }
5910 return it->second;
5911 }
5912
5913 } // namespace CVC4