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