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