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