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