Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Check macros for the cvc5 C++ API.
11 : : *
12 : : * These macros implement guards for the cvc5 C++ API functions.
13 : : */
14 : :
15 : : #include "cvc5_private.h"
16 : :
17 : : #ifndef CVC5__API__CHECKS_H
18 : : #define CVC5__API__CHECKS_H
19 : :
20 : : #include <cvc5/cvc5.h>
21 : :
22 : : #include <sstream>
23 : :
24 : : #include "base/modal_exception.h"
25 : : #include "options/option_exception.h"
26 : :
27 : : namespace cvc5 {
28 : :
29 : : #define CVC5_API_TRY_CATCH_BEGIN \
30 : : try \
31 : : {
32 : : #define CVC5_API_TRY_CATCH_END \
33 : : } \
34 : : catch (const internal::OptionException& e) \
35 : : { \
36 : : throw CVC5ApiOptionException(e.getMessage()); \
37 : : } \
38 : : catch (const internal::RecoverableModalException& e) \
39 : : { \
40 : : throw CVC5ApiRecoverableException(e.getMessage()); \
41 : : } \
42 : : catch (const internal::Exception& e) \
43 : : { \
44 : : throw CVC5ApiException(e.getMessage()); \
45 : : } \
46 : : catch (const std::invalid_argument& e) { throw CVC5ApiException(e.what()); }
47 : :
48 : : /* -------------------------------------------------------------------------- */
49 : : /* API guard helpers */
50 : : /* -------------------------------------------------------------------------- */
51 : :
52 : : class CVC5ApiExceptionStream
53 : : {
54 : : public:
55 : 1424 : CVC5ApiExceptionStream() {}
56 : : /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
57 : : * a destructor that throws an exception and in C++11 all destructors
58 : : * default to noexcept(true) (else this triggers a call to std::terminate). */
59 : 1424 : ~CVC5ApiExceptionStream() noexcept(false)
60 : : {
61 [ + - ]: 1424 : if (std::uncaught_exceptions() == 0)
62 : : {
63 : 1424 : throw CVC5ApiException(d_stream.str());
64 : : }
65 : 1424 : }
66 : :
67 : 1424 : std::ostream& ostream() { return d_stream; }
68 : :
69 : : private:
70 : : std::stringstream d_stream;
71 : : };
72 : :
73 : : class CVC5ApiRecoverableExceptionStream
74 : : {
75 : : public:
76 : 67 : CVC5ApiRecoverableExceptionStream() {}
77 : : /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
78 : : * a destructor that throws an exception and in C++11 all destructors
79 : : * default to noexcept(true) (else this triggers a call to std::terminate). */
80 : 67 : ~CVC5ApiRecoverableExceptionStream() noexcept(false)
81 : : {
82 [ + - ]: 67 : if (std::uncaught_exceptions() == 0)
83 : : {
84 : 67 : throw CVC5ApiRecoverableException(d_stream.str());
85 : : }
86 : 67 : }
87 : :
88 : 67 : std::ostream& ostream() { return d_stream; }
89 : :
90 : : private:
91 : : std::stringstream d_stream;
92 : : };
93 : :
94 : : class CVC5ApiUnsupportedExceptionStream
95 : : {
96 : : public:
97 : 54 : CVC5ApiUnsupportedExceptionStream() {}
98 : : /* Note: This needs to be explicitly set to 'noexcept(false)' since it is
99 : : * a destructor that throws an exception and in C++11 all destructors
100 : : * default to noexcept(true) (else this triggers a call to std::terminate). */
101 : 54 : ~CVC5ApiUnsupportedExceptionStream() noexcept(false)
102 : : {
103 [ + - ]: 54 : if (std::uncaught_exceptions() == 0)
104 : : {
105 : 54 : throw CVC5ApiUnsupportedException(d_stream.str());
106 : : }
107 : 54 : }
108 : :
109 : 54 : std::ostream& ostream() { return d_stream; }
110 : :
111 : : private:
112 : : std::stringstream d_stream;
113 : : };
114 : :
115 : : /* -------------------------------------------------------------------------- */
116 : : /* Basic check macros. */
117 : : /* -------------------------------------------------------------------------- */
118 : :
119 : : /**
120 : : * The base check macro.
121 : : * Throws a CVC5ApiException if 'cond' is false.
122 : : */
123 : : #define CVC5_API_CHECK(cond) \
124 : : CVC5_PREDICT_TRUE(cond) \
125 : : ? (void)0 \
126 : : : cvc5::internal::OstreamVoider() & cvc5::CVC5ApiExceptionStream().ostream()
127 : :
128 : : /**
129 : : * The base check macro for throwing recoverable exceptions.
130 : : * Throws a CVC5ApiRecoverableException if 'cond' is false.
131 : : */
132 : : #define CVC5_API_RECOVERABLE_CHECK(cond) \
133 : : CVC5_PREDICT_TRUE(cond) \
134 : : ? (void)0 \
135 : : : cvc5::internal::OstreamVoider() \
136 : : & cvc5::CVC5ApiRecoverableExceptionStream().ostream()
137 : :
138 : : /**
139 : : * The base check macro for throwing unsupported exceptions.
140 : : * Throws a CVC5ApiUnsupportedException if 'cond' is false.
141 : : */
142 : : #define CVC5_API_UNSUPPORTED_CHECK(cond) \
143 : : CVC5_PREDICT_TRUE(cond) \
144 : : ? (void)0 \
145 : : : cvc5::internal::OstreamVoider() \
146 : : & cvc5::CVC5ApiUnsupportedExceptionStream().ostream()
147 : :
148 : : /* -------------------------------------------------------------------------- */
149 : : /* Not null checks. */
150 : : /* -------------------------------------------------------------------------- */
151 : :
152 : : /** Check it 'this' is not a null object. */
153 : : #define CVC5_API_CHECK_NOT_NULL \
154 : : CVC5_API_CHECK(!isNullHelper()) \
155 : : << "invalid call to '" << __PRETTY_FUNCTION__ \
156 : : << "', expected non-null object"
157 : :
158 : : /** Check if given argument is not a null object. */
159 : : #define CVC5_API_ARG_CHECK_NOT_NULL(arg) \
160 : : CVC5_API_CHECK(!arg.isNull()) << "invalid null argument for '" << #arg << "'";
161 : :
162 : : /** Check if given argument is not a null pointer. */
163 : : #define CVC5_API_ARG_CHECK_NOT_NULLPTR(arg) \
164 : : CVC5_API_CHECK(arg != nullptr) << "invalid null argument for '" << #arg << "'"
165 : : /**
166 : : * Check if given argument at given index in container 'args' is not a null
167 : : * object.
168 : : */
169 : : #define CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL(what, arg, args, idx) \
170 : : CVC5_API_CHECK(!arg.isNull()) << "invalid null " << (what) << " in '" \
171 : : << #args << "' at index " << (idx)
172 : :
173 : : /* -------------------------------------------------------------------------- */
174 : : /* Kind checks. */
175 : : /* -------------------------------------------------------------------------- */
176 : :
177 : : /** Check if given kind is a valid kind. */
178 : : #define CVC5_API_KIND_CHECK(kind) \
179 : : CVC5_API_CHECK(isDefinedKind(kind)) \
180 : : << "invalid kind '" << std::to_string(kind) << "'"
181 : :
182 : : /**
183 : : * Check if given kind is a valid kind.
184 : : * Creates a stream to provide a message that identifies what kind was expected
185 : : * if given kind is invalid.
186 : : */
187 : : #define CVC5_API_KIND_CHECK_EXPECTED(cond, kind) \
188 : : CVC5_PREDICT_TRUE(cond) \
189 : : ? (void)0 \
190 : : : cvc5::internal::OstreamVoider() \
191 : : & CVC5ApiExceptionStream().ostream() \
192 : : << "invalid kind '" << std::to_string(kind) << "', expected "
193 : :
194 : : /* -------------------------------------------------------------------------- */
195 : : /* Argument checks. */
196 : : /* -------------------------------------------------------------------------- */
197 : :
198 : : /**
199 : : * Check condition 'cond' for given argument 'arg'.
200 : : * Creates a stream to provide a message that identifies what was expected to
201 : : * hold if condition is false and throws a non-recoverable exception.
202 : : */
203 : : #define CVC5_API_ARG_CHECK_EXPECTED(cond, arg) \
204 : : CVC5_PREDICT_TRUE(cond) \
205 : : ? (void)0 \
206 : : : cvc5::internal::OstreamVoider() \
207 : : & CVC5ApiExceptionStream().ostream() \
208 : : << "invalid argument '" << arg << "' for '" << #arg \
209 : : << "', expected "
210 : :
211 : : /**
212 : : * Check condition 'cond' for given argument 'arg'.
213 : : * Creates a stream to provide a message that identifies what was expected to
214 : : * hold if condition is false and throws a recoverable exception.
215 : : */
216 : : #define CVC5_API_RECOVERABLE_ARG_CHECK_EXPECTED(cond, arg) \
217 : : CVC5_PREDICT_TRUE(cond) \
218 : : ? (void)0 \
219 : : : cvc5::internal::OstreamVoider() \
220 : : & CVC5ApiRecoverableExceptionStream().ostream() \
221 : : << "invalid argument '" << arg << "' for '" << #arg \
222 : : << "', expected "
223 : :
224 : : /**
225 : : * Check condition 'cond' for given argument 'arg'.
226 : : * Provides a more specific error message than CVC5_API_ARG_CHECK_EXPECTED,
227 : : * it identifies that this check is a size check.
228 : : * Creates a stream to provide a message that identifies what was expected to
229 : : * hold if condition is false and throws a recoverable exception.
230 : : */
231 : : #define CVC5_API_ARG_SIZE_CHECK_EXPECTED(cond, arg) \
232 : : CVC5_PREDICT_TRUE(cond) \
233 : : ? (void)0 \
234 : : : cvc5::internal::OstreamVoider() \
235 : : & CVC5ApiExceptionStream().ostream() \
236 : : << "invalid size of argument '" << #arg << "', expected "
237 : :
238 : : /**
239 : : * Check condition 'cond' for the argument at given index in container 'args'.
240 : : * Argument 'what' identifies what is being checked (e.g., "term").
241 : : * Creates a stream to provide a message that identifies what was expected to
242 : : * hold if condition is false.
243 : : * Usage:
244 : : * CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(
245 : : * <condition>, "what", <container>, <idx>) << "message";
246 : : */
247 : : #define CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(cond, what, args, idx) \
248 : : CVC5_PREDICT_TRUE(cond) \
249 : : ? (void)0 \
250 : : : cvc5::internal::OstreamVoider() \
251 : : & CVC5ApiExceptionStream().ostream() \
252 : : << "invalid " << (what) << " in '" << #args << "' at index " \
253 : : << (idx) << ", expected "
254 : :
255 : : /**
256 : : * Check condition 'cond' for given operator index `index` in list of indices
257 : : * `args`. Creates a stream to provide a message that identifies what was
258 : : * expected to hold if condition is false and throws a non-recoverable
259 : : * exception.
260 : : */
261 : : #define CVC5_API_CHECK_OP_INDEX(cond, args, index) \
262 : : CVC5_PREDICT_TRUE(cond) \
263 : : ? (void)0 \
264 : : : cvc5::internal::OstreamVoider() \
265 : : & CVC5ApiExceptionStream().ostream() \
266 : : << "invalid value '" << args[index] << "' at index " << index \
267 : : << " for operator, expected "
268 : :
269 : : /* -------------------------------------------------------------------------- */
270 : : /* Term manager check. */
271 : : /* -------------------------------------------------------------------------- */
272 : :
273 : : /**
274 : : * Term manager check for member functions of classes other than class Solver.
275 : : * Check if given term manager matches the term manager this solver object is
276 : : * associated with.
277 : : */
278 : : #define CVC5_API_ARG_CHECK_TM(what, arg) \
279 : : CVC5_API_CHECK(d_nm == arg.d_nm) \
280 : : << "Given " << (what) \
281 : : << " is not associated with the term manager this " \
282 : : << "object is associated with"
283 : :
284 : : /* -------------------------------------------------------------------------- */
285 : : /* Sort checks. */
286 : : /* -------------------------------------------------------------------------- */
287 : :
288 : : /**
289 : : * Sort check for member functions of classes other than class Solver.
290 : : * Check if given sort is not null and associated with the term manager this
291 : : * object is associated with.
292 : : */
293 : : #define CVC5_API_CHECK_SORT(sort) \
294 : : do \
295 : : { \
296 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
297 : : CVC5_API_ARG_CHECK_TM("sort", sort); \
298 : : } while (0)
299 : :
300 : : /**
301 : : * Sort check for member functions of classes other than class Solver.
302 : : * Check if each sort in the given container of sorts is not null and
303 : : * associated with the term manager this object is associated with.
304 : : */
305 : : #define CVC5_API_CHECK_SORTS(sorts) \
306 : : do \
307 : : { \
308 : : size_t i = 0; \
309 : : for (const auto& s : sorts) \
310 : : { \
311 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \
312 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == s.d_nm, "sort", sorts, i) \
313 : : << "a sort associated with term manager this object is associated " \
314 : : "with"; \
315 : : i += 1; \
316 : : } \
317 : : } while (0)
318 : :
319 : : /**
320 : : * Sort check for member functions of classes other than class Solver.
321 : : * Check if each sort in the given container of sorts is not null, is
322 : : * associated with the term manager this object is associated with, and is a
323 : : * first-class sort.
324 : : */
325 : : #define CVC5_API_CHECK_DOMAIN_SORTS(sorts) \
326 : : do \
327 : : { \
328 : : size_t i = 0; \
329 : : for (const auto& s : sorts) \
330 : : { \
331 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", s, sorts, i); \
332 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == s.d_nm, "sort", sorts, i) \
333 : : << "a sort associated with the term manager this object is " \
334 : : "associated " \
335 : : "with"; \
336 : : CVC5_API_ARG_CHECK_EXPECTED(s.getTypeNode().isFirstClass(), s) \
337 : : << "first-class sort as domain sort"; \
338 : : i += 1; \
339 : : } \
340 : : } while (0)
341 : :
342 : : /* -------------------------------------------------------------------------- */
343 : : /* Term checks. */
344 : : /* -------------------------------------------------------------------------- */
345 : :
346 : : /**
347 : : * Term check for member functions of classes other than class Solver.
348 : : * Check if given term is not null and associated with the term manager this
349 : : * object is associated with.
350 : : */
351 : : #define CVC5_API_CHECK_TERM(term) \
352 : : do \
353 : : { \
354 : : CVC5_API_ARG_CHECK_NOT_NULL(term); \
355 : : CVC5_API_ARG_CHECK_TM("term", term); \
356 : : } while (0)
357 : :
358 : : /**
359 : : * Term check for member functions of classes other than class Solver.
360 : : * Check if each term in the given container of terms is not null and
361 : : * associated with the term manager this object is associated with.
362 : : */
363 : : #define CVC5_API_CHECK_TERMS(terms) \
364 : : do \
365 : : { \
366 : : size_t i = 0; \
367 : : for (const auto& s : terms) \
368 : : { \
369 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", s, terms, i); \
370 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == s.d_nm, "term", terms, i) \
371 : : << "a term associated with the term manager this object is " \
372 : : "associated " \
373 : : "with"; \
374 : : i += 1; \
375 : : } \
376 : : } while (0)
377 : :
378 : : /**
379 : : * Term check for member functions of classes other than class Solver.
380 : : * Check if each term and sort in the given map (which maps terms to sorts) is
381 : : * not null and associated with the term manager this object is associated
382 : : * with.
383 : : */
384 : : #define CVC5_API_CHECK_TERMS_MAP(map) \
385 : : do \
386 : : { \
387 : : size_t i = 0; \
388 : : for (const auto& p : map) \
389 : : { \
390 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", p.first, map, i); \
391 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
392 : : d_nm == p.first.d_nm, "term", map, i) \
393 : : << "a term associated with the term manager this object is " \
394 : : "associated " \
395 : : "with"; \
396 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", p.second, map, i); \
397 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
398 : : d_nm == p.second.d_nm, "sort", map, i) \
399 : : << "a sort associated with the term manager this object is " \
400 : : "associated " \
401 : : "with"; \
402 : : i += 1; \
403 : : } \
404 : : } while (0)
405 : :
406 : : /**
407 : : * Term check for member functions of classes other than class Solver.
408 : : * Check if each term in the given container is not null, associated with the
409 : : * term manager object this object is associated with, and of the given sort.
410 : : */
411 : : #define CVC5_API_CHECK_TERMS_WITH_SORT(terms, sort) \
412 : : do \
413 : : { \
414 : : size_t i = 0; \
415 : : for (const auto& t : terms) \
416 : : { \
417 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, i); \
418 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == t.d_nm, "term", terms, i) \
419 : : << "a term associated with the term manager this object is " \
420 : : "associated " \
421 : : "with"; \
422 : : CVC5_API_CHECK(CVC5_EQUAL(t.getSort(), sort)) \
423 : : << "Expected term with sort " << sort << " at index " << i << " in " \
424 : : << #terms; \
425 : : i += 1; \
426 : : } \
427 : : } while (0)
428 : :
429 : : /**
430 : : * Term check for member functions of classes other than class Solver.
431 : : * Check if each term in both the given container is not null, associated with
432 : : * the term manager this object is associated with, and their sorts are
433 : : * pairwise equal.
434 : : */
435 : : #define CVC5_API_TERM_CHECK_TERMS_WITH_TERMS_SORT_EQUAL_TO(terms1, terms2) \
436 : : do \
437 : : { \
438 : : size_t i = 0; \
439 : : for (const auto& t1 : terms1) \
440 : : { \
441 : : const auto& t2 = terms2[i]; \
442 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t1, terms1, i); \
443 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == t1.d_nm, "term", terms1, i) \
444 : : << "a term associated with the term manager this object is " \
445 : : "associated " \
446 : : "with"; \
447 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t2, terms2, i); \
448 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == t2.d_nm, "term", terms2, i) \
449 : : << "a term associated with the term manager this object is " \
450 : : "associated " \
451 : : "with"; \
452 : : CVC5_API_CHECK(CVC5_EQUAL(t1.getSort(), t2.getSort())) \
453 : : << "expecting terms of the same sort at index " << i; \
454 : : i += 1; \
455 : : } \
456 : : } while (0)
457 : :
458 : : /* -------------------------------------------------------------------------- */
459 : : /* DatatypeDecl checks. */
460 : : /* -------------------------------------------------------------------------- */
461 : :
462 : : /**
463 : : * DatatypeDecl check for member functions of classes other than class Solver.
464 : : * Check if given datatype declaration is not null and associated with the
465 : : * term manager this DatatypeDecl object is associated with.
466 : : */
467 : : #define CVC5_API_CHECK_DTDECL(decl) \
468 : : do \
469 : : { \
470 : : CVC5_API_ARG_CHECK_NOT_NULL(decl); \
471 : : CVC5_API_CHECK(d_nm == decl.d_nm) \
472 : : << "Given datatype declaration is not associated with the term " \
473 : : "manager this " \
474 : : << "object is associated with"; \
475 : : } while (0)
476 : :
477 : : /* -------------------------------------------------------------------------- */
478 : : /* Checks for class TermManager. */
479 : : /* -------------------------------------------------------------------------- */
480 : :
481 : : /**
482 : : * Term manager check for member functions of class TermManager.
483 : : * Check if given term manager matches the term manager this term manager.
484 : : */
485 : : #define CVC5_API_ARG_TM_CHECK_TM(what, arg) \
486 : : CVC5_API_CHECK(d_nm == arg.d_nm) \
487 : : << "Given " << (what) << " is not associated with this term manager"
488 : : /**
489 : : * Sort check for member functions of class TermManager.
490 : : * Check if given sort is not null and associated with this term manager.
491 : : */
492 : : #define CVC5_API_TM_CHECK_SORT(sort) \
493 : : do \
494 : : { \
495 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
496 : : CVC5_API_ARG_TM_CHECK_TM("sort", sort); \
497 : : } while (0)
498 : :
499 : : /**
500 : : * Sort check for member functions of class TermManager.
501 : : * Check if given sort at given index of given sorts is not null and associated
502 : : * with this term manager.
503 : : */
504 : : #define CVC5_API_TM_CHECK_SORT_AT_INDEX(sort, sorts, index) \
505 : : do \
506 : : { \
507 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sort", sort, sorts, index); \
508 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
509 : : d_nm == sort.d_nm, "sort", sorts, index) \
510 : : << "a sort associated with this term manager"; \
511 : : } while (0)
512 : :
513 : : /**
514 : : * Sort checks for member functions of class TermManager.
515 : : * Check if each sort in the given container of sorts is not null and
516 : : * associated with the term manager of this solver.
517 : : */
518 : : #define CVC5_API_TM_CHECK_SORTS(sorts) \
519 : : do \
520 : : { \
521 : : size_t i = 0; \
522 : : for (const auto& s : sorts) \
523 : : { \
524 : : CVC5_API_TM_CHECK_SORT_AT_INDEX(s, sorts, i); \
525 : : i += 1; \
526 : : } \
527 : : } while (0)
528 : :
529 : : /**
530 : : * Domain sort checks for member functions of class TermManager.
531 : : * Check if each domain sort in the given container of sorts is not null,
532 : : * associated with this term manager, and a first-class sort.
533 : : */
534 : : #define CVC5_API_TM_CHECK_DOMAIN_SORTS(sorts) \
535 : : do \
536 : : { \
537 : : size_t i = 0; \
538 : : for (const auto& s : sorts) \
539 : : { \
540 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("domain sort", s, sorts, i); \
541 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
542 : : d_nm == s.d_nm, "domain sort", sorts, i) \
543 : : << "a sort associated with this term manager"; \
544 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
545 : : s.getTypeNode().isFirstClass(), "domain sort", sorts, i) \
546 : : << "first-class sort as domain sort"; \
547 : : i += 1; \
548 : : } \
549 : : } while (0)
550 : :
551 : : /**
552 : : * Domain sort check for member functions of class TermManager.
553 : : * Check if domain sort is not null, associated with this term manager, and a
554 : : * first-class sort.
555 : : */
556 : : #define CVC5_API_TM_CHECK_DOMAIN_SORT(sort) \
557 : : do \
558 : : { \
559 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
560 : : CVC5_API_CHECK(d_nm == sort.d_nm) << "Given sort is not associated with " \
561 : : "this term manager"; \
562 : : CVC5_API_ARG_CHECK_EXPECTED(sort.getTypeNode().isFirstClass(), sort) \
563 : : << "first-class sort as domain sort"; \
564 : : } while (0)
565 : :
566 : : /**
567 : : * Codomain sort check for member functions of class TermManager.
568 : : * Check if codomain sort is not null, associated with this term manager, and a
569 : : * first-class, non-function sort.
570 : : */
571 : : #define CVC5_API_TM_CHECK_CODOMAIN_SORT(sort) \
572 : : do \
573 : : { \
574 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
575 : : CVC5_API_CHECK(d_nm == sort.d_nm) << "Given sort is not associated with " \
576 : : "this term manager"; \
577 : : CVC5_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \
578 : : << "non-function sort as codomain sort"; \
579 : : } while (0)
580 : :
581 : : /**
582 : : * Op checks for member functions of class TermManager.
583 : : * Check if given operator is not null and associated with this term manager.
584 : : */
585 : : #define CVC5_API_TM_CHECK_OP(op) \
586 : : do \
587 : : { \
588 : : CVC5_API_ARG_CHECK_NOT_NULL(op); \
589 : : CVC5_API_CHECK(d_nm == op.d_nm) << "Given operator is not associated " \
590 : : "with this term manager"; \
591 : : } while (0)
592 : :
593 : : /**
594 : : * Term check for member functions of class TermManager.
595 : : * Check if given term is not null and associated with this term manager.
596 : : */
597 : : #define CVC5_API_TM_CHECK_TERM(term) \
598 : : do \
599 : : { \
600 : : CVC5_API_ARG_CHECK_NOT_NULL(term); \
601 : : CVC5_API_ARG_TM_CHECK_TM("term", term); \
602 : : } while (0)
603 : :
604 : : /**
605 : : * Term checks for member functions of class TermManager.
606 : : * Check if given term 't' (which is stored at index 'idx' of 'terms') is not
607 : : * null and associated with this term manager.
608 : : */
609 : : #define CVC5_API_TM_CHECK_TERM_AT_INDEX(t, terms, idx) \
610 : : do \
611 : : { \
612 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, idx); \
613 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_nm == t.d_nm, "term", terms, idx) \
614 : : << "a term associated with this term manager"; \
615 : : } while (0)
616 : :
617 : : /**
618 : : * Term checks for member functions of class TermManager.
619 : : * Check if each term in the given container of terms is not null and
620 : : * associated with this term manager.
621 : : */
622 : : #define CVC5_API_TM_CHECK_TERMS(terms) \
623 : : for (size_t i = 0, size = terms.size(); i < size; ++i) \
624 : : { \
625 : : CVC5_API_TM_CHECK_TERM_AT_INDEX(terms[i], terms, i); \
626 : : }
627 : :
628 : : /**
629 : : * DatatypeDecl checks for member functions of class TermManager.
630 : : * Check if given datatype declaration is not null and associated with this
631 : : * term manager.
632 : : */
633 : : #define CVC5_API_TM_CHECK_DTDECL(decl) \
634 : : do \
635 : : { \
636 : : CVC5_API_ARG_CHECK_NOT_NULL(decl); \
637 : : CVC5_API_ARG_TM_CHECK_TM("datatype declaration", decl); \
638 : : CVC5_API_CHECK(!decl.isResolved()) \
639 : : << "Given datatype declaration is already resolved (has already " \
640 : : << "been used to create a datatype sort)"; \
641 : : CVC5_API_ARG_CHECK_EXPECTED( \
642 : : dtypedecl.getDatatype().getNumConstructors() > 0, dtypedecl) \
643 : : << "a datatype declaration with at least one constructor"; \
644 : : } while (0)
645 : :
646 : : /**
647 : : * DatatypeDecl checks for member functions of class TermManager.
648 : : * Check if each datatype declaration in the given container of declarations is
649 : : * not null and associated with this term manager.
650 : : */
651 : : #define CVC5_API_TM_CHECK_DTDECLS(decls) \
652 : : do \
653 : : { \
654 : : size_t i = 0; \
655 : : for (const auto& d : decls) \
656 : : { \
657 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \
658 : : "datatype declaration", d, decls, i); \
659 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
660 : : d_nm == d.d_nm, "datatype declaration", decls, i) \
661 : : << "a datatype declaration associated with this term manager"; \
662 : : CVC5_API_CHECK(!d.isResolved()) \
663 : : << "Given datatype declaration is already resolved (has " \
664 : : << "already been used to create a datatype sort)"; \
665 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
666 : : d.getDatatype().getNumConstructors() > 0, \
667 : : "datatype declaration", \
668 : : decls, \
669 : : i) \
670 : : << "a datatype declaration with at least one constructor"; \
671 : : i += 1; \
672 : : } \
673 : : } while (0)
674 : :
675 : : /* -------------------------------------------------------------------------- */
676 : : /* Checks for class Solver. */
677 : : /* -------------------------------------------------------------------------- */
678 : :
679 : : /* Sort checks. ------------------------------------------------------------- */
680 : :
681 : : /**
682 : : * Sort checks for member functions of class Solver.
683 : : * Check if given sort is not null and associated with the term manager of this
684 : : * solver.
685 : : */
686 : : #define CVC5_API_SOLVER_CHECK_SORT(sort) \
687 : : do \
688 : : { \
689 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
690 : : CVC5_API_CHECK(d_tm.d_nm == sort.d_nm) \
691 : : << "Given sort is not associated with " \
692 : : "the term manager of this solver"; \
693 : : } while (0)
694 : :
695 : : /**
696 : : * Sort checks for member functions of class Solver.
697 : : * Check if each sort in the given container of sorts is not null and
698 : : * associated with the term manager of this solver.
699 : : */
700 : : #define CVC5_API_SOLVER_CHECK_SORTS(sorts) \
701 : : do \
702 : : { \
703 : : size_t i = 0; \
704 : : for (const auto& s : sorts) \
705 : : { \
706 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("sorts", s, sorts, i); \
707 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
708 : : d_tm.d_nm == s.d_nm, "sort", sorts, i) \
709 : : << "a sort associated with the term manager of this solver"; \
710 : : i += 1; \
711 : : } \
712 : : } while (0)
713 : :
714 : : /**
715 : : * Domain sort checks for member functions of class Solver.
716 : : * Check if each domain sort in the given container of sorts is not null,
717 : : * associated with the term manager of this solver, and a first-class sort.
718 : : */
719 : : #define CVC5_API_SOLVER_CHECK_DOMAIN_SORTS(sorts) \
720 : : do \
721 : : { \
722 : : size_t i = 0; \
723 : : for (const auto& s : sorts) \
724 : : { \
725 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("domain sort", s, sorts, i); \
726 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
727 : : d_tm.d_nm == s.d_nm, "domain sort", sorts, i) \
728 : : << "a sort associated with the term manager of this solver object"; \
729 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
730 : : s.getTypeNode().isFirstClass(), "domain sort", sorts, i) \
731 : : << "first-class sort as domain sort"; \
732 : : i += 1; \
733 : : } \
734 : : } while (0)
735 : :
736 : : /**
737 : : * Codomain sort check for member functions of class Solver.
738 : : * Check if codomain sort is not null, associated with the term manager of this
739 : : * solver, and a first-class, non-function sort.
740 : : */
741 : : #define CVC5_API_SOLVER_CHECK_CODOMAIN_SORT(sort) \
742 : : do \
743 : : { \
744 : : CVC5_API_ARG_CHECK_NOT_NULL(sort); \
745 : : CVC5_API_CHECK(d_tm.d_nm == sort.d_nm) \
746 : : << "Given sort is not associated with " \
747 : : "the term manager of this solver"; \
748 : : CVC5_API_ARG_CHECK_EXPECTED(!sort.isFunction(), sort) \
749 : : << "non-function sort as codomain sort"; \
750 : : } while (0)
751 : :
752 : : /* Term checks. ------------------------------------------------------------- */
753 : :
754 : : /**
755 : : * Term checks for member functions of class Solver.
756 : : * Check if given term is not null and associated with the term manager of this
757 : : * solver.
758 : : */
759 : : #define CVC5_API_SOLVER_CHECK_TERM(term) \
760 : : do \
761 : : { \
762 : : CVC5_API_ARG_CHECK_NOT_NULL(term); \
763 : : CVC5_API_CHECK(d_tm.d_nm == term.d_nm) \
764 : : << "Given term is not associated with " \
765 : : "the term manager of this solver"; \
766 : : } while (0)
767 : :
768 : : /**
769 : : * Term checks for member functions of class Solver.
770 : : * Check if given term 't' (which is stored at index 'idx' of 'terms') is not
771 : : * null and associated with the term manager of this solver.
772 : : */
773 : : #define CVC5_API_SOLVER_CHECK_TERM_AT_INDEX(t, terms, idx) \
774 : : do \
775 : : { \
776 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL("term", t, terms, idx); \
777 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
778 : : d_tm.d_nm == t.d_nm, "term", terms, idx) \
779 : : << "a term associated with the term manager of this solver"; \
780 : : } while (0)
781 : :
782 : : /**
783 : : * Term checks for member functions of class Solver.
784 : : * Check if each term in the given container of terms is not null and
785 : : * associated with the term manager of this solver.
786 : : */
787 : : #define CVC5_API_SOLVER_CHECK_TERMS(terms) \
788 : : do \
789 : : { \
790 : : size_t i = 0; \
791 : : for (const auto& t : terms) \
792 : : { \
793 : : CVC5_API_SOLVER_CHECK_TERM_AT_INDEX(t, terms, i); \
794 : : i += 1; \
795 : : } \
796 : : } while (0)
797 : :
798 : : /**
799 : : * Term checks for member functions of class Solver.
800 : : * Check if given term is not null, associated with the term manager of this
801 : : * solver, and of given sort.
802 : : */
803 : : #define CVC5_API_SOLVER_CHECK_TERM_WITH_SORT(term, sort) \
804 : : do \
805 : : { \
806 : : CVC5_API_SOLVER_CHECK_TERM(term); \
807 : : CVC5_API_CHECK(CVC5_EQUAL(term.getSort(), sort)) \
808 : : << "Expected term with sort " << sort; \
809 : : } while (0)
810 : :
811 : : /**
812 : : * Term checks for member functions of class Solver.
813 : : * Check if each term in the given container is not null, associated with the
814 : : * term manager of this solver, and of the given sort.
815 : : */
816 : : #define CVC5_API_SOLVER_CHECK_TERMS_WITH_SORT(terms, sort) \
817 : : for (size_t i = 0, size = terms.size(); i < size; ++i) \
818 : : { \
819 : : CVC5_API_SOLVER_CHECK_TERM_AT_INDEX(terms[i], terms, i); \
820 : : CVC5_API_CHECK(CVC5_EQUAL(terms[i].getSort(), sort)) \
821 : : << "Expected term with sort " << sort << " at index " << i << " in " \
822 : : << #terms; \
823 : : }
824 : :
825 : : /**
826 : : * Bound variable checks for member functions of class Solver.
827 : : * Check if given term 'bv' (which is stored at index 'idx' of 'bound_vars') is
828 : : * not null, associated with the term manager of this solver, and a bound
829 : : * variable.
830 : : */
831 : : #define CVC5_API_SOLVER_CHECK_BOUND_VAR_AT_INDEX(bv, bound_vars, idx) \
832 : : do \
833 : : { \
834 : : CVC5_API_SOLVER_CHECK_TERM_AT_INDEX(bv, bound_vars, idx); \
835 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
836 : : bv.d_node->getKind() == cvc5::internal::Kind::BOUND_VARIABLE, \
837 : : "bound variable", \
838 : : bound_vars, \
839 : : idx) \
840 : : << "a bound variable"; \
841 : : } while (0)
842 : :
843 : : /**
844 : : * Bound variable checks for member functions of class Solver.
845 : : * Check if each term in the given container is not null, associated with the
846 : : * term manager of this solver, and a bound variable.
847 : : */
848 : : #define CVC5_API_SOLVER_CHECK_BOUND_VARS(bound_vars) \
849 : : for (size_t i = 0, size = bound_vars.size(); i < size; ++i) \
850 : : { \
851 : : CVC5_API_SOLVER_CHECK_BOUND_VAR_AT_INDEX(bound_vars[i], bound_vars, i); \
852 : : }
853 : :
854 : : /**
855 : : * Additional bound variable checks for member functions of class Solver that
856 : : * define functions.
857 : : * Check if each term in the given container matches the corresponding sort in
858 : : * 'domain_sorts', and is a first-class term.
859 : : */
860 : : #define CVC5_API_SOLVER_CHECK_BOUND_VARS_DEF_FUN_SORTS(bound_vars, \
861 : : domain_sorts) \
862 : : do \
863 : : { \
864 : : size_t size = bound_vars.size(); \
865 : : CVC5_API_ARG_SIZE_CHECK_EXPECTED(size == domain_sorts.size(), bound_vars) \
866 : : << "'" << domain_sorts.size() << "'"; \
867 : : for (size_t i = 0; i < size; ++i) \
868 : : { \
869 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
870 : : domain_sorts[i] == bound_vars[i].getSort(), \
871 : : "sort of parameter", \
872 : : bound_vars, \
873 : : i) \
874 : : << "sort '" << domain_sorts[i] << "'"; \
875 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED( \
876 : : domain_sorts[i].getTypeNode().isFirstClass(), \
877 : : "domain sort", \
878 : : domain_sorts, \
879 : : i) \
880 : : << "first-class sort of parameter of defined function"; \
881 : : } \
882 : : } while (0)
883 : :
884 : : /**
885 : : * Grammar checks for member functions of class Solver.
886 : : * Check if given grammar is not null and associated with the term manager of
887 : : * this solver.
888 : : */
889 : : #define CVC5_API_SOLVER_CHECK_GRAMMAR(grammar) \
890 : : do \
891 : : { \
892 : : CVC5_API_ARG_CHECK_NOT_NULL(grammar); \
893 : : CVC5_API_CHECK(d_tm.d_nm == grammar.d_nm) \
894 : : << "Given grammar is not associated with " \
895 : : "the term manager of this solver"; \
896 : : } while (0)
897 : :
898 : : /* Datatype checks. --------------------------------------------------------- */
899 : :
900 : : /**
901 : : * DatatypeConstructorDecl checks for member functions of class Solver.
902 : : * Check if a given datatype constructor declaration at the index in the given
903 : : * container of declarations is not null and associated with the term manager of
904 : : * this solver.
905 : : */
906 : : #define CVC5_API_SOLVER_CHECK_DTCTORDECL_AT_INDEX(decl, decls, idx) \
907 : : do \
908 : : { \
909 : : CVC5_API_ARG_AT_INDEX_CHECK_NOT_NULL( \
910 : : "datatype constructor declaration", decl, decls, idx); \
911 : : CVC5_API_ARG_AT_INDEX_CHECK_EXPECTED(d_tm.d_nm == decl.d_nm, \
912 : : "datatype constructor declaration", \
913 : : decls, \
914 : : idx) \
915 : : << "a datatype constructor declaration associated with the term " \
916 : : "manager of this solver " \
917 : : "object"; \
918 : : } while (0)
919 : :
920 : : /**
921 : : * DatatypeConstructorDecl checks for member functions of class Solver.
922 : : * Check if each datatype constructor declaration in the given container of
923 : : * declarations is not null and associated with the term manager of this solver.
924 : : */
925 : : #define CVC5_API_SOLVER_CHECK_DTCTORDECLS(decls) \
926 : : for (size_t i = 0, size = decls.size(); i < size; ++i) \
927 : : { \
928 : : CVC5_API_SOLVER_CHECK_DTCTORDECL_AT_INDEX(decls[i], decls, i); \
929 : : }
930 : :
931 : : /**
932 : : * Argument number checks for mkOp.
933 : : */
934 : : #define CVC5_API_OP_CHECK_ARITY(nargs, expected, kind) \
935 : : CVC5_API_CHECK(nargs == expected) \
936 : : << "invalid number of indices for operator " << kind << ", expected " \
937 : : << expected << " but got " << nargs << "."
938 : :
939 : : } // namespace cvc5
940 : : #endif
|
