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