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 : : * The cvc5 C++ API.
11 : : */
12 : :
13 : : #include <cvc5/cvc5_export.h>
14 : :
15 : : #ifndef CVC5__API__CVC5_H
16 : : #define CVC5__API__CVC5_H
17 : :
18 : : #include <cvc5/cvc5_kind.h>
19 : : #include <cvc5/cvc5_proof_rule.h>
20 : : #include <cvc5/cvc5_skolem_id.h>
21 : : #include <cvc5/cvc5_types.h>
22 : :
23 : : #include <functional>
24 : : #include <map>
25 : : #include <memory>
26 : : #include <optional>
27 : : #include <set>
28 : : #include <sstream>
29 : : #include <string>
30 : : #include <unordered_map>
31 : : #include <unordered_set>
32 : : #include <variant>
33 : : #include <vector>
34 : :
35 : : namespace cvc5 {
36 : :
37 : : namespace main {
38 : : class CommandExecutor;
39 : : } // namespace main
40 : :
41 : : namespace internal {
42 : :
43 : : #ifndef DOXYGEN_SKIP
44 : : template <bool ref_count>
45 : : class NodeTemplate;
46 : : typedef NodeTemplate<true> Node;
47 : : #endif
48 : :
49 : : class DType;
50 : : class DTypeConstructor;
51 : : class DTypeSelector;
52 : : class NodeManager;
53 : : class SolverEngine;
54 : : class TypeNode;
55 : : class ProofNode;
56 : : class Options;
57 : : class Random;
58 : : class Rational;
59 : : class Result;
60 : : class SygusGrammar;
61 : : class SynthResult;
62 : : class StatisticsRegistry;
63 : : } // namespace internal
64 : :
65 : : namespace parser {
66 : : class Cmd;
67 : : }
68 : :
69 : : class TermManager;
70 : : class Solver;
71 : : class Statistics;
72 : : struct APIStatistics;
73 : : class Term;
74 : : class PluginInternal;
75 : :
76 : : /* -------------------------------------------------------------------------- */
77 : : /* Exception */
78 : : /* -------------------------------------------------------------------------- */
79 : :
80 : : /**
81 : : * Base class for all API exceptions.
82 : : * If thrown, all API objects may be in an unsafe state.
83 : : */
84 : : class CVC5_EXPORT CVC5ApiException : public std::exception
85 : : {
86 : : public:
87 : : /**
88 : : * Construct with message from a string.
89 : : * @param str The error message.
90 : : */
91 : 13054 : CVC5ApiException(const std::string& str) : d_msg(str) {}
92 : : /**
93 : : * Construct with message from a string stream.
94 : : * @param stream The error message.
95 : : */
96 : : CVC5ApiException(const std::stringstream& stream) : d_msg(stream.str()) {}
97 : : /**
98 : : * Retrieve the message from this exception.
99 : : * @return The error message.
100 : : */
101 : 1096 : const std::string& getMessage() const { return d_msg; }
102 : : /**
103 : : * Retrieve the message as a C-style array.
104 : : * @return The error message.
105 : : */
106 : 144 : const char* what() const noexcept override { return d_msg.c_str(); }
107 : :
108 : : /**
109 : : * Printing: feel free to redefine toStream(). When overridden in
110 : : * a derived class, it's recommended that this method print the
111 : : * type of exception before the actual message.
112 : : */
113 : 4 : virtual void toStream(std::ostream& os) const { os << d_msg; }
114 : :
115 : : private:
116 : : /** The stored error message. */
117 : : std::string d_msg;
118 : : };
119 : :
120 : 67 : inline std::ostream& operator<<(std::ostream& os, const CVC5ApiException& e)
121 : : {
122 : 67 : e.toStream(os);
123 : 67 : return os;
124 : : }
125 : :
126 : : /**
127 : : * A recoverable API exception.
128 : : * If thrown, API objects can still be used.
129 : : */
130 : : class CVC5_EXPORT CVC5ApiRecoverableException : public CVC5ApiException
131 : : {
132 : : public:
133 : : /**
134 : : * Construct with message from a string.
135 : : * @param str The error message.
136 : : */
137 : 11140 : CVC5ApiRecoverableException(const std::string& str) : CVC5ApiException(str) {}
138 : : /**
139 : : * Construct with message from a string stream.
140 : : * @param stream The error message.
141 : : */
142 : : CVC5ApiRecoverableException(const std::stringstream& stream)
143 : : : CVC5ApiException(stream.str())
144 : : {
145 : : }
146 : : };
147 : :
148 : : /**
149 : : * Exception for unsupported command arguments.
150 : : * If thrown, API objects can still be used.
151 : : */
152 : : class CVC5_EXPORT CVC5ApiUnsupportedException
153 : : : public CVC5ApiRecoverableException
154 : : {
155 : : public:
156 : : /**
157 : : * Construct with message from a string.
158 : : * @param str The error message.
159 : : */
160 : 56 : CVC5ApiUnsupportedException(const std::string& str)
161 : 56 : : CVC5ApiRecoverableException(str)
162 : : {
163 : 56 : }
164 : : /**
165 : : * Construct with message from a string stream.
166 : : * @param stream The error message.
167 : : */
168 : : CVC5ApiUnsupportedException(const std::stringstream& stream)
169 : : : CVC5ApiRecoverableException(stream.str())
170 : : {
171 : : }
172 : : };
173 : :
174 : : /**
175 : : * An option-related API exception.
176 : : * If thrown, API objects can still be used.
177 : : */
178 : : class CVC5_EXPORT CVC5ApiOptionException : public CVC5ApiRecoverableException
179 : : {
180 : : public:
181 : : /**
182 : : * Construct with message from a string.
183 : : * @param str The error message.
184 : : */
185 : 11002 : CVC5ApiOptionException(const std::string& str)
186 : 11002 : : CVC5ApiRecoverableException(str)
187 : : {
188 : 11002 : }
189 : : /**
190 : : * Construct with message from a string stream.
191 : : * @param stream The error message.
192 : : */
193 : : CVC5ApiOptionException(const std::stringstream& stream)
194 : : : CVC5ApiRecoverableException(stream.str())
195 : : {
196 : : }
197 : : };
198 : :
199 : : /* -------------------------------------------------------------------------- */
200 : : /* Result */
201 : : /* -------------------------------------------------------------------------- */
202 : :
203 : : /**
204 : : * Encapsulation of a three-valued solver result, with explanations.
205 : : */
206 : : class CVC5_EXPORT Result
207 : : {
208 : : friend class Solver;
209 : :
210 : : public:
211 : : /** Constructor. */
212 : : Result();
213 : :
214 : : /**
215 : : * Determine if this Result is a nullary Result.
216 : : * @return True if Result is empty (a nullary Result) and not an actual
217 : : * result returned from a checkSat() (and friends) query.
218 : : */
219 : : bool isNull() const;
220 : :
221 : : /**
222 : : * @return True if this result is from a satisfiable checkSat() or
223 : : * checkSatAssuming() query.
224 : : */
225 : : bool isSat() const;
226 : :
227 : : /**
228 : : * @return True if this result is from an unsatisfiable checkSat() or
229 : : * checkSatAssuming() query.
230 : : */
231 : : bool isUnsat() const;
232 : :
233 : : /**
234 : : * @return True if result is from a checkSat() or checkSatAssuming() query
235 : : * and cvc5 was not able to determine (un)satisfiability.
236 : : */
237 : : bool isUnknown() const;
238 : :
239 : : /**
240 : : * Operator overloading for equality of two results.
241 : : * @param r The result to compare to for equality.
242 : : * @return True if the results are equal.
243 : : */
244 : : bool operator==(const Result& r) const;
245 : :
246 : : /**
247 : : * Operator overloading for disequality of two results.
248 : : * @param r The result to compare to for disequality.
249 : : * @return True if the results are disequal.
250 : : */
251 : : bool operator!=(const Result& r) const;
252 : :
253 : : /**
254 : : * @return An explanation for an unknown query result.
255 : : */
256 : : UnknownExplanation getUnknownExplanation() const;
257 : :
258 : : /**
259 : : * @return A string representation of this result.
260 : : */
261 : : std::string toString() const;
262 : :
263 : : private:
264 : : /**
265 : : * Constructor.
266 : : * @param r The internal result that is to be wrapped by this result.
267 : : * @return The Result.
268 : : */
269 : : Result(const internal::Result& r);
270 : :
271 : : /**
272 : : * The internal result wrapped by this result.
273 : : *
274 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
275 : : * since ``internal::Result`` is not ref counted.
276 : : */
277 : : std::shared_ptr<internal::Result> d_result;
278 : : };
279 : :
280 : : /**
281 : : * Serialize a Result to given stream.
282 : : * @param out The output stream.
283 : : * @param r The result to be serialized to the given output stream.
284 : : * @return The output stream.
285 : : */
286 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Result& r);
287 : :
288 : : } // namespace cvc5
289 : :
290 : : namespace std {
291 : : /**
292 : : * Hash function for results.
293 : : */
294 : : template <>
295 : : struct CVC5_EXPORT hash<cvc5::Result>
296 : : {
297 : : size_t operator()(const cvc5::Result& result) const;
298 : : };
299 : : } // namespace std
300 : :
301 : : namespace cvc5 {
302 : :
303 : : /* -------------------------------------------------------------------------- */
304 : : /* SynthResult */
305 : : /* -------------------------------------------------------------------------- */
306 : :
307 : : /**
308 : : * Encapsulation of a solver synth result.
309 : : *
310 : : * This is the return value of the API functions:
311 : : * - Solver::checkSynth()
312 : : * - Solver::checkSynthNext()
313 : : *
314 : : * which we call "synthesis queries". This class indicates whether the
315 : : * synthesis query has a solution, has no solution, or is unknown.
316 : : */
317 : : class CVC5_EXPORT SynthResult
318 : : {
319 : : friend class Solver;
320 : :
321 : : public:
322 : : /** Constructor. */
323 : : SynthResult();
324 : :
325 : : /**
326 : : * Determine if a given synthesis result is empty (a nullary result) and not
327 : : * an actual result returned from a synthesis query.
328 : : * @return True if SynthResult is null, i.e., not a SynthResult returned
329 : : * from a synthesis query.
330 : : */
331 : : bool isNull() const;
332 : :
333 : : /**
334 : : * @return True if the synthesis query has a solution.
335 : : */
336 : : bool hasSolution() const;
337 : :
338 : : /**
339 : : * @return True if the synthesis query has no solution. In this case, it
340 : : * was determined that there was no solution.
341 : : */
342 : : bool hasNoSolution() const;
343 : :
344 : : /**
345 : : * @return True if the result of the synthesis query could not be determined.
346 : : */
347 : : bool isUnknown() const;
348 : :
349 : : /**
350 : : * Operator overloading for equality of two synthesis results.
351 : : * @param r The synthesis result to compare to for equality.
352 : : * @return True if the synthesis results are equal.
353 : : */
354 : : bool operator==(const SynthResult& r) const;
355 : :
356 : : /**
357 : : * Operator overloading for disequality of two synthesis results.
358 : : * @param r The synthesis result to compare to for disequality.
359 : : * @return True if the synthesis results are disequal.
360 : : */
361 : : bool operator!=(const SynthResult& r) const;
362 : :
363 : : /**
364 : : * @return A string representation of this synthesis result.
365 : : */
366 : : std::string toString() const;
367 : :
368 : : private:
369 : : /**
370 : : * Constructor.
371 : : * @param r The internal synth result that is to be wrapped by this synth.
372 : : * result
373 : : * @return The SynthResult.
374 : : */
375 : : SynthResult(const internal::SynthResult& r);
376 : : /**
377 : : * The internal result wrapped by this result.
378 : : *
379 : : * @note This is a `std::shared_ptr` rather than a `std::unique_ptr`
380 : : * since `internal::SynthResult` is not ref counted.
381 : : */
382 : : std::shared_ptr<internal::SynthResult> d_result;
383 : : };
384 : :
385 : : /**
386 : : * Serialize a SynthResult to given stream.
387 : : * @param out The output stream.
388 : : * @param r The result to be serialized to the given output stream.
389 : : * @return The output stream.
390 : : */
391 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const SynthResult& r);
392 : :
393 : : } // namespace cvc5
394 : :
395 : : namespace std {
396 : : /**
397 : : * Hash function for synthesis results.
398 : : */
399 : : template <>
400 : : struct CVC5_EXPORT hash<cvc5::SynthResult>
401 : : {
402 : : size_t operator()(const cvc5::SynthResult& result) const;
403 : : };
404 : : } // namespace std
405 : :
406 : : namespace cvc5 {
407 : :
408 : : /* -------------------------------------------------------------------------- */
409 : : /* Sort */
410 : : /* -------------------------------------------------------------------------- */
411 : :
412 : : class Datatype;
413 : :
414 : : /**
415 : : * The sort of a cvc5 term.
416 : : */
417 : : class CVC5_EXPORT Sort
418 : : {
419 : : friend class parser::Cmd;
420 : : friend class DatatypeConstructor;
421 : : friend class DatatypeConstructorDecl;
422 : : friend class DatatypeSelector;
423 : : friend class DatatypeDecl;
424 : : friend class Datatype;
425 : : friend class Op;
426 : : friend class Term;
427 : : friend class TermManager;
428 : : friend class Solver;
429 : : friend class Grammar;
430 : : friend struct std::hash<Sort>;
431 : :
432 : : public:
433 : : /**
434 : : * Constructor.
435 : : */
436 : : Sort();
437 : :
438 : : /**
439 : : * Destructor.
440 : : */
441 : : ~Sort();
442 : :
443 : : /**
444 : : * Comparison for structural equality.
445 : : * @param s The sort to compare to.
446 : : * @return True if the sorts are equal.
447 : : */
448 : : bool operator==(const Sort& s) const;
449 : :
450 : : /**
451 : : * Comparison for structural disequality.
452 : : * @param s The sort to compare to.
453 : : * @return True if the sorts are not equal.
454 : : */
455 : : bool operator!=(const Sort& s) const;
456 : :
457 : : /**
458 : : * Comparison for ordering on sorts.
459 : : * @param s The sort to compare to.
460 : : * @return True if this sort is less than s.
461 : : */
462 : : bool operator<(const Sort& s) const;
463 : :
464 : : /**
465 : : * Comparison for ordering on sorts.
466 : : * @param s The sort to compare to.
467 : : * @return True if this sort is greater than s.
468 : : */
469 : : bool operator>(const Sort& s) const;
470 : :
471 : : /**
472 : : * Comparison for ordering on sorts.
473 : : * @param s The sort to compare to.
474 : : * @return True if this sort is less than or equal to s.
475 : : */
476 : : bool operator<=(const Sort& s) const;
477 : :
478 : : /**
479 : : * Comparison for ordering on sorts.
480 : : * @param s The sort to compare to.
481 : : * @return True if this sort is greater than or equal to s.
482 : : */
483 : : bool operator>=(const Sort& s) const;
484 : :
485 : : /**
486 : : * Get the kind of this sort.
487 : : * @return The kind of the sort.
488 : : *
489 : : * @warning This function is experimental and may change in future versions.
490 : : */
491 : : SortKind getKind() const;
492 : :
493 : : /**
494 : : * Determine if this sort has a symbol (a name).
495 : : *
496 : : * For example, uninterpreted sorts and uninterpreted sort constructors have
497 : : * symbols.
498 : : *
499 : : * @return True if the sort has a symbol.
500 : : */
501 : : bool hasSymbol() const;
502 : :
503 : : /**
504 : : * Get the symbol of this Sort.
505 : : *
506 : : * @note Asserts hasSymbol().
507 : : *
508 : : * The symbol of this sort is the string that was
509 : : * provided when constructing it via
510 : : * TermManager::mkUninterpretedSort(const std::optional<std::string>&), or
511 : : * TermManager::mkUninterpretedSortConstructorSort(size_t, const
512 : : * std::optional<std::string>&).
513 : : *
514 : : * @return The raw symbol of the sort.
515 : : */
516 : : std::string getSymbol() const;
517 : :
518 : : /**
519 : : * Determine if this is the null sort (Sort::Sort()).
520 : : * @return True if this Sort is the null sort.
521 : : */
522 : : bool isNull() const;
523 : :
524 : : /**
525 : : * Determine if this is the Boolean sort (SMT-LIB: `Bool`).
526 : : * @return True if this sort is the Boolean sort.
527 : : */
528 : : bool isBoolean() const;
529 : :
530 : : /**
531 : : * Determine if this is the integer sort (SMT-LIB: `Int`).
532 : : * @return True if this sort is the integer sort.
533 : : */
534 : : bool isInteger() const;
535 : :
536 : : /**
537 : : * Determine if this is the real sort (SMT-LIB: `Real`).
538 : : * @return True if this sort is the real sort.
539 : : */
540 : : bool isReal() const;
541 : :
542 : : /**
543 : : * Determine if this is the string sort (SMT-LIB: `String`).
544 : : * @return True if this sort is the string sort.
545 : : */
546 : : bool isString() const;
547 : :
548 : : /**
549 : : * Determine if this is the regular expression sort (SMT-LIB: `RegLan`).
550 : : * @return True if this sort is the regular expression sort.
551 : : */
552 : : bool isRegExp() const;
553 : :
554 : : /**
555 : : * Determine if this is the rounding mode sort (SMT-LIB: `RoundingMode`).
556 : : * @return True if this sort is the rounding mode sort.
557 : : */
558 : : bool isRoundingMode() const;
559 : :
560 : : /**
561 : : * Determine if this is a bit-vector sort (SMT-LIB: `(_ BitVec i)`).
562 : : * @return True if this sort is a bit-vector sort.
563 : : */
564 : : bool isBitVector() const;
565 : :
566 : : /**
567 : : * Determine if this is a floatingpoint sort
568 : : * (SMT-LIB: `(_ FloatingPoint eb sb)`).
569 : : * @return True if this sort is a floating-point sort.
570 : : */
571 : : bool isFloatingPoint() const;
572 : :
573 : : /**
574 : : * Determine if this is a datatype sort.
575 : : * @return True if this sort is a datatype sort.
576 : : */
577 : : bool isDatatype() const;
578 : :
579 : : /**
580 : : * Determine if this is a datatype constructor sort.
581 : : * @return True if this sort is a datatype constructor sort.
582 : : */
583 : : bool isDatatypeConstructor() const;
584 : :
585 : : /**
586 : : * Determine if this is a datatype selector sort.
587 : : * @return True if this sort is a datatype selector sort.
588 : : */
589 : : bool isDatatypeSelector() const;
590 : :
591 : : /**
592 : : * Determine if this is a datatype tester sort.
593 : : * @return True if this sort is a datatype tester sort.
594 : : */
595 : : bool isDatatypeTester() const;
596 : : /**
597 : : * Determine if this is a datatype updater sort.
598 : : * @return True if this sort is a datatype updater sort.
599 : : */
600 : : bool isDatatypeUpdater() const;
601 : : /**
602 : : * Determine if this is a function sort.
603 : : * @return True if this sort is a function sort.
604 : : */
605 : : bool isFunction() const;
606 : :
607 : : /**
608 : : * Determine if this is a predicate sort.
609 : : *
610 : : * A predicate sort is a function sort that maps to the Boolean sort. All
611 : : * predicate sorts are also function sorts.
612 : : *
613 : : * @return True if this sort is a predicate sort.
614 : : */
615 : : bool isPredicate() const;
616 : :
617 : : /**
618 : : * Determine if this is a tuple sort.
619 : : * @return True if this sort is a tuple sort.
620 : : */
621 : : bool isTuple() const;
622 : :
623 : : /**
624 : : * Determine if this is a nullable sort.
625 : : * @return True if the sort is a nullable sort.
626 : : */
627 : : bool isNullable() const;
628 : :
629 : : /**
630 : : * Determine if this is a record sort.
631 : : * @warning This function is experimental and may change in future versions.
632 : : * @return True if the sort is a record sort.
633 : : */
634 : : bool isRecord() const;
635 : :
636 : : /**
637 : : * Determine if this is an array sort.
638 : : * @return True if the sort is an array sort.
639 : : */
640 : : bool isArray() const;
641 : :
642 : : /**
643 : : * Determine if this is a finite field sort.
644 : : * @return True if the sort is a finite field sort.
645 : : */
646 : : bool isFiniteField() const;
647 : :
648 : : /**
649 : : * Determine if this is a Set sort.
650 : : * @return True if the sort is a Set sort.
651 : : */
652 : : bool isSet() const;
653 : :
654 : : /**
655 : : * Determine if this is a Bag sort.
656 : : * @return True if the sort is a Bag sort.
657 : : */
658 : : bool isBag() const;
659 : :
660 : : /**
661 : : * Determine if this is a Sequence sort.
662 : : * @return True if the sort is a Sequence sort.
663 : : */
664 : : bool isSequence() const;
665 : :
666 : : /**
667 : : * Determine if this is an abstract sort.
668 : : * @return True if the sort is a abstract sort.
669 : : *
670 : : * @warning This function is experimental and may change in future versions.
671 : : */
672 : : bool isAbstract() const;
673 : :
674 : : /**
675 : : * Determine if this is an uninterpreted sort.
676 : : * @return True if this is an uninterpreted sort.
677 : : */
678 : : bool isUninterpretedSort() const;
679 : :
680 : : /**
681 : : * Determine if this is an uninterpreted sort constructor.
682 : : *
683 : : * An uninterpreted sort constructor has arity > 0 and can be instantiated to
684 : : * construct uninterpreted sorts with given sort parameters.
685 : : *
686 : : * @return True if this is of sort constructor kind.
687 : : */
688 : : bool isUninterpretedSortConstructor() const;
689 : :
690 : : /**
691 : : * Determine if this is an instantiated (parametric datatype or uninterpreted
692 : : * sort constructor) sort.
693 : : *
694 : : * An instantiated sort is a sort that has been constructed from
695 : : * instantiating a sort with sort arguments
696 : : * (see Sort::instantiate(const std::vector<Sort>&) const)).
697 : : *
698 : : * @return True if this is an instantiated sort.
699 : : */
700 : : bool isInstantiated() const;
701 : :
702 : : /**
703 : : * Get the associated uninterpreted sort constructor of an instantiated
704 : : * uninterpreted sort.
705 : : *
706 : : * @return The uninterpreted sort constructor sort.
707 : : */
708 : : Sort getUninterpretedSortConstructor() const;
709 : :
710 : : /**
711 : : * @return The underlying datatype of a datatype sort.
712 : : */
713 : : Datatype getDatatype() const;
714 : :
715 : : /**
716 : : * Instantiate a parameterized datatype sort or uninterpreted sort
717 : : * constructor sort.
718 : : *
719 : : * Create sort parameters with TermManager::mkParamSort().
720 : : *
721 : : * @param params The list of sort parameters to instantiate with.
722 : : * @return The instantiated sort.
723 : : */
724 : : Sort instantiate(const std::vector<Sort>& params) const;
725 : :
726 : : /**
727 : : * Get the sorts used to instantiate the sort parameters of a parametric
728 : : * sort (parametric datatype or uninterpreted sort constructor sort,
729 : : * see Sort::instantiate(const std::vector<Sort>& const)).
730 : : *
731 : : * @return The sorts used to instantiate the sort parameters of a
732 : : * parametric sort
733 : : */
734 : : std::vector<Sort> getInstantiatedParameters() const;
735 : :
736 : : /**
737 : : * Substitution of Sorts.
738 : : *
739 : : * Note that this replacement is applied during a pre-order traversal and
740 : : * only once to the sort. It is not run until fix point.
741 : : *
742 : : * For example,
743 : : * `(Array A B).substitute({A, C}, {(Array C D), (Array A B)})` will
744 : : * return `(Array (Array C D) B)`.
745 : : *
746 : : * @warning This function is experimental and may change in future versions.
747 : : *
748 : : * @param sort The subsort to be substituted within this sort.
749 : : * @param replacement The sort replacing the substituted subsort.
750 : : */
751 : : Sort substitute(const Sort& sort, const Sort& replacement) const;
752 : :
753 : : /**
754 : : * Simultaneous substitution of Sorts.
755 : : *
756 : : * Note that this replacement is applied during a pre-order traversal and
757 : : * only once to the sort. It is not run until fix point. In the case that
758 : : * sorts contains duplicates, the replacement earliest in the vector takes
759 : : * priority.
760 : : *
761 : : * @warning This function is experimental and may change in future versions.
762 : : *
763 : : * @param sorts The subsorts to be substituted within this sort.
764 : : * @param replacements The sort replacing the substituted subsorts.
765 : : */
766 : : Sort substitute(const std::vector<Sort>& sorts,
767 : : const std::vector<Sort>& replacements) const;
768 : :
769 : : /**
770 : : * Output a string representation of this sort to a given stream.
771 : : * @param out The output stream.
772 : : */
773 : : void toStream(std::ostream& out) const;
774 : :
775 : : /**
776 : : * @return A string representation of this sort.
777 : : */
778 : : std::string toString() const;
779 : :
780 : : /* Datatype constructor sort ------------------------------------------- */
781 : :
782 : : /**
783 : : * @return The arity of a datatype constructor sort.
784 : : */
785 : : size_t getDatatypeConstructorArity() const;
786 : :
787 : : /**
788 : : * @return The domain sorts of a datatype constructor sort.
789 : : */
790 : : std::vector<Sort> getDatatypeConstructorDomainSorts() const;
791 : :
792 : : /**
793 : : * @return The codomain sort of a constructor sort.
794 : : */
795 : : Sort getDatatypeConstructorCodomainSort() const;
796 : :
797 : : /* Selector sort ------------------------------------------------------- */
798 : :
799 : : /**
800 : : * @return The domain sort of a datatype selector sort.
801 : : */
802 : : Sort getDatatypeSelectorDomainSort() const;
803 : :
804 : : /**
805 : : * @return The codomain sort of a datatype selector sort.
806 : : */
807 : : Sort getDatatypeSelectorCodomainSort() const;
808 : :
809 : : /* Tester sort ------------------------------------------------------- */
810 : :
811 : : /**
812 : : * @return The domain sort of a datatype tester sort.
813 : : */
814 : : Sort getDatatypeTesterDomainSort() const;
815 : :
816 : : /**
817 : : * @return The codomain sort of a datatype tester sort, which is the Boolean
818 : : * sort.
819 : : *
820 : : * @note We mainly need this for the symbol table, which doesn't have
821 : : * access to the solver object.
822 : : */
823 : : Sort getDatatypeTesterCodomainSort() const;
824 : :
825 : : /* Function sort ------------------------------------------------------- */
826 : :
827 : : /**
828 : : * @return The arity of a function sort.
829 : : */
830 : : size_t getFunctionArity() const;
831 : :
832 : : /**
833 : : * @return The domain sorts of a function sort.
834 : : */
835 : : std::vector<Sort> getFunctionDomainSorts() const;
836 : :
837 : : /**
838 : : * @return The codomain sort of a function sort.
839 : : */
840 : : Sort getFunctionCodomainSort() const;
841 : :
842 : : /* Array sort ---------------------------------------------------------- */
843 : :
844 : : /**
845 : : * @return The array index sort of an array sort.
846 : : */
847 : : Sort getArrayIndexSort() const;
848 : :
849 : : /**
850 : : * @return The array element sort of an array sort.
851 : : */
852 : : Sort getArrayElementSort() const;
853 : :
854 : : /* Set sort ------------------------------------------------------------ */
855 : :
856 : : /**
857 : : * @return The element sort of a set sort.
858 : : */
859 : : Sort getSetElementSort() const;
860 : :
861 : : /* Bag sort ------------------------------------------------------------ */
862 : :
863 : : /**
864 : : * @return The element sort of a bag sort.
865 : : */
866 : : Sort getBagElementSort() const;
867 : :
868 : : /* Sequence sort ------------------------------------------------------- */
869 : :
870 : : /**
871 : : * @return The element sort of a sequence sort.
872 : : */
873 : : Sort getSequenceElementSort() const;
874 : :
875 : : /* Abstract sort ------------------------------------------------------- */
876 : : /**
877 : : * @return The sort kind of an abstract sort, which denotes the kind of
878 : : * sorts that this abstract sort denotes.
879 : : *
880 : : * @warning This function is experimental and may change in future versions.
881 : : */
882 : : SortKind getAbstractedKind() const;
883 : :
884 : : /* Uninterpreted sort constructor sort --------------------------------- */
885 : :
886 : : /**
887 : : * @return The arity of an uninterpreted sort constructor sort.
888 : : */
889 : : size_t getUninterpretedSortConstructorArity() const;
890 : :
891 : : /* Bit-vector sort ----------------------------------------------------- */
892 : :
893 : : /**
894 : : * @return The bit-width of the bit-vector sort.
895 : : */
896 : : uint32_t getBitVectorSize() const;
897 : :
898 : : /* Finite field sort --------------------------------------------------- */
899 : :
900 : : /**
901 : : * @return The size of the finite field sort.
902 : : */
903 : : std::string getFiniteFieldSize() const;
904 : :
905 : : /* Floating-point sort ------------------------------------------------- */
906 : :
907 : : /**
908 : : * @return The bit-width of the exponent of the floating-point sort.
909 : : */
910 : : uint32_t getFloatingPointExponentSize() const;
911 : :
912 : : /**
913 : : * @return The width of the significand of the floating-point sort.
914 : : */
915 : : uint32_t getFloatingPointSignificandSize() const;
916 : :
917 : : /* Datatype sort ------------------------------------------------------- */
918 : :
919 : : /**
920 : : * Get the arity of a datatype sort, which is the number of type parameters
921 : : * if the datatype is parametric, or 0 otherwise.
922 : : * @return The arity of a datatype sort.
923 : : */
924 : : size_t getDatatypeArity() const;
925 : :
926 : : /* Tuple sort ---------------------------------------------------------- */
927 : :
928 : : /**
929 : : * @return The length of a tuple sort.
930 : : */
931 : : size_t getTupleLength() const;
932 : :
933 : : /**
934 : : * @return The element sorts of a tuple sort.
935 : : */
936 : : std::vector<Sort> getTupleSorts() const;
937 : :
938 : : /**
939 : : * @return The element sort of a nullable sort.
940 : : */
941 : : Sort getNullableElementSort() const;
942 : :
943 : : /* --------------------------------------------------------------------- */
944 : :
945 : : private:
946 : : /** @return The internal wrapped TypeNode of this sort. */
947 : : const internal::TypeNode& getTypeNode(void) const;
948 : :
949 : : /** Helper to convert a vector of Sorts to internal TypeNodes. */
950 : : std::vector<internal::TypeNode> static sortVectorToTypeNodes(
951 : : const std::vector<Sort>& sorts);
952 : : /** Helper to convert a vector of internal TypeNodes to Sorts. */
953 : : std::vector<Sort> static typeNodeVectorToSorts(
954 : : TermManager* tm, const std::vector<internal::TypeNode>& types);
955 : :
956 : : /**
957 : : * Constructor.
958 : : * @param tm The associated term manager.
959 : : * @param t The internal type that is to be wrapped by this sort.
960 : : * @return The Sort.
961 : : */
962 : : Sort(TermManager* tm, const internal::TypeNode& t);
963 : :
964 : : /**
965 : : * Helper for isNull checks. This prevents calling an API function with
966 : : * CVC5_API_CHECK_NOT_NULL
967 : : */
968 : : bool isNullHelper() const;
969 : :
970 : : /**
971 : : * The associated term manager.
972 : : */
973 : : TermManager* d_tm = nullptr;
974 : :
975 : : /**
976 : : * The internal type wrapped by this sort.
977 : : *
978 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
979 : : * avoid overhead due to memory allocation (``internal::Type`` is
980 : : * already ref counted, so this could be a ``std::unique_ptr`` instead).
981 : : */
982 : : std::shared_ptr<internal::TypeNode> d_type;
983 : : };
984 : :
985 : : /**
986 : : * Serialize a sort to given stream.
987 : : * @param out The output stream.
988 : : * @param s The sort to be serialized to the given output stream.
989 : : * @return The output stream.
990 : : */
991 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Sort& s);
992 : :
993 : : } // namespace cvc5
994 : :
995 : : namespace std {
996 : :
997 : : /**
998 : : * Hash function for Sorts.
999 : : */
1000 : : template <>
1001 : : struct CVC5_EXPORT hash<cvc5::Sort>
1002 : : {
1003 : : size_t operator()(const cvc5::Sort& s) const;
1004 : : };
1005 : :
1006 : : } // namespace std
1007 : :
1008 : : namespace cvc5 {
1009 : :
1010 : : /* -------------------------------------------------------------------------- */
1011 : : /* Op */
1012 : : /* -------------------------------------------------------------------------- */
1013 : :
1014 : : /**
1015 : : * A cvc5 operator.
1016 : : *
1017 : : * An operator is a term that represents certain operators, instantiated
1018 : : * with its required parameters, e.g., a Term of kind #BITVECTOR_EXTRACT.
1019 : : */
1020 : : class CVC5_EXPORT Op
1021 : : {
1022 : : friend class TermManager;
1023 : : friend class Term;
1024 : : friend struct std::hash<Op>;
1025 : :
1026 : : public:
1027 : : /**
1028 : : * Constructor.
1029 : : */
1030 : : Op();
1031 : :
1032 : : /**
1033 : : * Destructor.
1034 : : */
1035 : : ~Op();
1036 : :
1037 : : /**
1038 : : * Syntactic equality operator.
1039 : : *
1040 : : * @param t The operator to compare to for equality.
1041 : : * @return True if both operators are syntactically identical.
1042 : : */
1043 : : bool operator==(const Op& t) const;
1044 : :
1045 : : /**
1046 : : * Syntactic disequality operator.
1047 : : *
1048 : : * @param t The operator to compare to for disequality.
1049 : : * @return True if operators differ syntactically.
1050 : : */
1051 : : bool operator!=(const Op& t) const;
1052 : :
1053 : : /**
1054 : : * Get the kind of this operator.
1055 : : * @return The kind of this operator.
1056 : : */
1057 : : Kind getKind() const;
1058 : :
1059 : : /**
1060 : : * Determine if this operator is nullary.
1061 : : * @return True if this operator is a nullary operator.
1062 : : */
1063 : : bool isNull() const;
1064 : :
1065 : : /**
1066 : : * Determine if this operator is indexed.
1067 : : * @return True iff this operator is indexed.
1068 : : */
1069 : : bool isIndexed() const;
1070 : :
1071 : : /**
1072 : : * Get the number of indices of this operator.
1073 : : * @return The number of indices of this operator.
1074 : : */
1075 : : size_t getNumIndices() const;
1076 : :
1077 : : /**
1078 : : * Get the index at position `i` of an indexed operator.
1079 : : * @param i The position of the index to return.
1080 : : * @return The index at position i.
1081 : : */
1082 : : Term operator[](size_t i);
1083 : :
1084 : : /**
1085 : : * Get the string representation of this operator.
1086 : : * @return A string representation of this operator.
1087 : : */
1088 : : std::string toString() const;
1089 : :
1090 : : private:
1091 : : /**
1092 : : * Constructor for a single kind (non-indexed operator).
1093 : : * @param tm The associated term manager.
1094 : : * @param k The kind of this Op.
1095 : : */
1096 : : Op(TermManager* tm, const Kind k);
1097 : :
1098 : : /**
1099 : : * Constructor.
1100 : : * @param tm The associated term managaer.
1101 : : * @param k The kind of this Op.
1102 : : * @param n The internal node that is to be wrapped by this term.
1103 : : * @return The Term.
1104 : : */
1105 : : Op(TermManager* tm, const Kind k, const internal::Node& n);
1106 : :
1107 : : /**
1108 : : * Helper for isNull checks. This prevents calling an API function with
1109 : : * CVC5_API_CHECK_NOT_NULL
1110 : : */
1111 : : bool isNullHelper() const;
1112 : :
1113 : : /**
1114 : : * @note An indexed operator has a non-null internal node (``d_node``).
1115 : : *
1116 : : * @note We use a helper function to avoid having API functions call other API
1117 : : * functions (we need to call this internally).
1118 : : *
1119 : : * @return True iff this Op is indexed.
1120 : : */
1121 : : bool isIndexedHelper() const;
1122 : :
1123 : : /**
1124 : : * Helper for getNumIndices
1125 : : * @return The number of indices of this op.
1126 : : */
1127 : : size_t getNumIndicesHelper() const;
1128 : :
1129 : : /**
1130 : : * Helper for operator[](size_t index).
1131 : : * @param index Position of the index. Should be less than
1132 : : * getNumIndicesHelper().
1133 : : * @return The index at position index.
1134 : : */
1135 : : Term getIndexHelper(size_t index);
1136 : :
1137 : : /**
1138 : : * The associated term manager.
1139 : : */
1140 : : TermManager* d_tm = nullptr;
1141 : :
1142 : : /** The kind of this operator. */
1143 : : Kind d_kind;
1144 : :
1145 : : /**
1146 : : * The internal node wrapped by this operator.
1147 : : *
1148 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
1149 : : * avoid overhead due to memory allocation (``internal::Node`` is
1150 : : * already ref counted, so this could be a ``std::unique_ptr`` instead).
1151 : : */
1152 : : std::shared_ptr<internal::Node> d_node;
1153 : : };
1154 : :
1155 : : /**
1156 : : * Serialize an operator to given stream.
1157 : : * @param out The output stream.
1158 : : * @param op The operator to be serialized to the given output stream.
1159 : : * @return The output stream.
1160 : : */
1161 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Op& op);
1162 : :
1163 : : } // namespace cvc5
1164 : :
1165 : : namespace std {
1166 : : /**
1167 : : * Hash function for Ops.
1168 : : */
1169 : : template <>
1170 : : struct CVC5_EXPORT hash<cvc5::Op>
1171 : : {
1172 : : size_t operator()(const cvc5::Op& op) const;
1173 : : };
1174 : : } // namespace std
1175 : :
1176 : : namespace cvc5 {
1177 : :
1178 : : /* -------------------------------------------------------------------------- */
1179 : : /* Term */
1180 : : /* -------------------------------------------------------------------------- */
1181 : :
1182 : : /**
1183 : : * A cvc5 Term.
1184 : : */
1185 : : class CVC5_EXPORT Term
1186 : : {
1187 : : friend class parser::Cmd;
1188 : : friend class Datatype;
1189 : : friend class DatatypeConstructor;
1190 : : friend class DatatypeSelector;
1191 : : friend class Proof;
1192 : : friend class TermManager;
1193 : : friend class Solver;
1194 : : friend class Grammar;
1195 : : friend class PluginInternal;
1196 : : friend class SynthResult;
1197 : : friend struct std::hash<Term>;
1198 : :
1199 : : public:
1200 : : /**
1201 : : * Constructor for a null term.
1202 : : */
1203 : : Term();
1204 : :
1205 : : /**
1206 : : * Destructor.
1207 : : */
1208 : : ~Term();
1209 : :
1210 : : /**
1211 : : * Syntactic equality operator.
1212 : : * @param t The term to compare to for equality.
1213 : : * @return True if the terms are equal.
1214 : : */
1215 : : bool operator==(const Term& t) const;
1216 : :
1217 : : /**
1218 : : * Syntactic disequality operator.
1219 : : * @param t The term to compare to for disequality.
1220 : : * @return True if terms are disequal.
1221 : : */
1222 : : bool operator!=(const Term& t) const;
1223 : :
1224 : : /**
1225 : : * Comparison for ordering on terms by their id.
1226 : : * @param t The term to compare to.
1227 : : * @return True if this term is less than t.
1228 : : */
1229 : : bool operator<(const Term& t) const;
1230 : :
1231 : : /**
1232 : : * Comparison for ordering on terms by their id.
1233 : : * @param t The term to compare to.
1234 : : * @return True if this term is greater than t.
1235 : : */
1236 : : bool operator>(const Term& t) const;
1237 : :
1238 : : /**
1239 : : * Comparison for ordering on terms by their id.
1240 : : * @param t The term to compare to.
1241 : : * @return True if this term is less than or equal to t.
1242 : : */
1243 : : bool operator<=(const Term& t) const;
1244 : :
1245 : : /**
1246 : : * Comparison for ordering on terms by their id.
1247 : : * @param t The term to compare to.
1248 : : * @return True if this term is greater than or equal to t.
1249 : : */
1250 : : bool operator>=(const Term& t) const;
1251 : :
1252 : : /**
1253 : : * Get the number of children of this term.
1254 : : * @return The number of children of this term.
1255 : : */
1256 : : size_t getNumChildren() const;
1257 : :
1258 : : /**
1259 : : * Get the child term of this term at a given index.
1260 : : * @param index The index of the child.
1261 : : * @return The child term at the given index.
1262 : : */
1263 : : Term operator[](size_t index) const;
1264 : :
1265 : : /**
1266 : : * Get the id of this term.
1267 : : * @return The id of this term.
1268 : : */
1269 : : uint64_t getId() const;
1270 : :
1271 : : /**
1272 : : * Get the kind of this term.
1273 : : * @return The kind of this term.
1274 : : */
1275 : : Kind getKind() const;
1276 : :
1277 : : /**
1278 : : * Get the sort of this term.
1279 : : * @return The sort of this term.
1280 : : */
1281 : : Sort getSort() const;
1282 : :
1283 : : /**
1284 : : * Replace `term` with `replacement` in this term.
1285 : : *
1286 : : * @param term The term to replace.
1287 : : * @param replacement The term to replace it with.
1288 : : * @return The result of replacing `term` with `replacement` in this term.
1289 : : *
1290 : : * @note This replacement is applied during a pre-order traversal and
1291 : : * only once (it is not run until fixed point).
1292 : : */
1293 : : Term substitute(const Term& term, const Term& replacement) const;
1294 : :
1295 : : /**
1296 : : * Simultaneously replace `terms` with `replacements` in this term.
1297 : : *
1298 : : * In the case that `terms` contains duplicates, the replacement earliest in
1299 : : * the vector takes priority. For example, calling substitute on `f(x,y)`
1300 : : * with `terms = { x, z }`, `replacements = { g(z), w }` results in the term
1301 : : * `f(g(z),y)`.
1302 : : *
1303 : : * @note Requires that `terms` and `replacements` are of equal size (they are
1304 : : * interpreted as 1 : 1 mapping).
1305 : : *
1306 : : * @note This replacement is applied during a pre-order traversal and
1307 : : * only once (it is not run until fixed point).
1308 : : *
1309 : : * @param terms The terms to replace.
1310 : : * @param replacements The replacement terms.
1311 : : * @return The result of simultaneously replacing `terms` with `replacements`
1312 : : * in this term.
1313 : : */
1314 : : Term substitute(const std::vector<Term>& terms,
1315 : : const std::vector<Term>& replacements) const;
1316 : :
1317 : : /**
1318 : : * Determine if this term has an operator.
1319 : : * @return True iff this term has an operator.
1320 : : */
1321 : : bool hasOp() const;
1322 : :
1323 : : /**
1324 : : * Get the operator of a term with an operator.
1325 : : *
1326 : : * @note Requires that this term has an operator (see hasOp()).
1327 : : *
1328 : : * @return The Op used to create this term.
1329 : : */
1330 : : Op getOp() const;
1331 : :
1332 : : /**
1333 : : * Determine if this term has a symbol (a name).
1334 : : *
1335 : : * For example, free constants and variables have symbols.
1336 : : *
1337 : : * @return True if the term has a symbol.
1338 : : */
1339 : : bool hasSymbol() const;
1340 : :
1341 : : /**
1342 : : * Get the symbol of this Term.
1343 : : *
1344 : : * @note Requires that this term has a symbol (see hasSymbol()).
1345 : : *
1346 : : * The symbol of the term is the string that was provided when constructing
1347 : : * it via TermManager::mkConst() or TermManager::mkVar().
1348 : : *
1349 : : * @return The raw symbol of the term.
1350 : : */
1351 : : std::string getSymbol() const;
1352 : :
1353 : : /**
1354 : : * Determine if this term is nullary.
1355 : : * @return True if this Term is a null term.
1356 : : */
1357 : : bool isNull() const;
1358 : :
1359 : : /**
1360 : : * Boolean negation.
1361 : : * @return The Boolean negation of this term.
1362 : : */
1363 : : Term notTerm() const;
1364 : :
1365 : : /**
1366 : : * Boolean and.
1367 : : * @param t A Boolean term.
1368 : : * @return The conjunction of this term and the given term.
1369 : : */
1370 : : Term andTerm(const Term& t) const;
1371 : :
1372 : : /**
1373 : : * Boolean or.
1374 : : * @param t A Boolean term.
1375 : : * @return The disjunction of this term and the given term.
1376 : : */
1377 : : Term orTerm(const Term& t) const;
1378 : :
1379 : : /**
1380 : : * Boolean exclusive or.
1381 : : * @param t A Boolean term.
1382 : : * @return The exclusive disjunction of this term and the given term.
1383 : : */
1384 : : Term xorTerm(const Term& t) const;
1385 : :
1386 : : /**
1387 : : * Equality.
1388 : : * @param t A Boolean term.
1389 : : * @return A Boolean term representing equivalence of this term and the given
1390 : : * term.
1391 : : */
1392 : : Term eqTerm(const Term& t) const;
1393 : :
1394 : : /**
1395 : : * Boolean implication.
1396 : : * @param t A Boolean term.
1397 : : * @return The implication of this term and the given term.
1398 : : */
1399 : : Term impTerm(const Term& t) const;
1400 : :
1401 : : /**
1402 : : * If-then-else with this term as the Boolean condition.
1403 : : * @param t The 'then' term.
1404 : : * @param e The 'else' term.
1405 : : * @return The if-then-else term with this term as the Boolean condition.
1406 : : */
1407 : : Term iteTerm(const Term& t, const Term& e) const;
1408 : :
1409 : : /**
1410 : : * @return A string representation of this term.
1411 : : */
1412 : : std::string toString() const;
1413 : :
1414 : : /**
1415 : : * Iterator for the children of a Term.
1416 : : * @note This treats uninterpreted functions as Term just like any other term
1417 : : * for example, the term ``f(x, y)`` will have Kind ``APPLY_UF`` and
1418 : : * three children: ``f``, ``x``, and ``y``
1419 : : */
1420 : : class CVC5_EXPORT const_iterator
1421 : : {
1422 : : friend class Term;
1423 : :
1424 : : public:
1425 : : /* The following types are required by trait std::iterator_traits */
1426 : :
1427 : : /** Iterator tag */
1428 : : using iterator_category = std::forward_iterator_tag;
1429 : :
1430 : : /** The type of the item */
1431 : : using value_type = Term;
1432 : :
1433 : : /** The pointer type of the item */
1434 : : using pointer = const Term*;
1435 : :
1436 : : /** The reference type of the item */
1437 : : using reference = const Term&;
1438 : :
1439 : : /** The type returned when two iterators are subtracted */
1440 : : using difference_type = std::ptrdiff_t;
1441 : :
1442 : : /* End of std::iterator_traits required types */
1443 : :
1444 : : /**
1445 : : * Null Constructor.
1446 : : */
1447 : : const_iterator();
1448 : :
1449 : : /**
1450 : : * Constructor
1451 : : * @param tm The associated term manager.
1452 : : * @param e A `std::shared pointer` to the node that we're iterating over.
1453 : : * @param p The position of the iterator (e.g. which child it's on).
1454 : : */
1455 : : const_iterator(TermManager* tm,
1456 : : const std::shared_ptr<internal::Node>& e,
1457 : : uint32_t p);
1458 : :
1459 : : /**
1460 : : * Equality operator.
1461 : : * @param it The iterator to compare to for equality.
1462 : : * @return True if the iterators are equal.
1463 : : */
1464 : : bool operator==(const const_iterator& it) const;
1465 : :
1466 : : /**
1467 : : * Disequality operator.
1468 : : * @param it The iterator to compare to for disequality.
1469 : : * @return True if the iterators are disequal.
1470 : : */
1471 : : bool operator!=(const const_iterator& it) const;
1472 : :
1473 : : /**
1474 : : * Increment operator (prefix).
1475 : : * @return A reference to the iterator after incrementing by one.
1476 : : */
1477 : : const_iterator& operator++();
1478 : :
1479 : : /**
1480 : : * Increment operator (postfix).
1481 : : * @return A reference to the iterator after incrementing by one.
1482 : : */
1483 : : const_iterator operator++(int);
1484 : :
1485 : : /**
1486 : : * Dereference operator.
1487 : : * @return The term this iterator points to.
1488 : : */
1489 : : Term operator*() const;
1490 : :
1491 : : private:
1492 : : /**
1493 : : * The associated term manager.
1494 : : */
1495 : : TermManager* d_tm = nullptr;
1496 : : /** The original node to be iterated over. */
1497 : : std::shared_ptr<internal::Node> d_origNode;
1498 : : /** Keeps track of the iteration position. */
1499 : : uint32_t d_pos;
1500 : : };
1501 : :
1502 : : /**
1503 : : * @return An iterator to the first child of this Term.
1504 : : */
1505 : : const_iterator begin() const;
1506 : :
1507 : : /**
1508 : : * @return An iterator to one-off-the-last child of this Term.
1509 : : */
1510 : : const_iterator end() const;
1511 : :
1512 : : /**
1513 : : * Get the sign of an integer or real value.
1514 : : * @note Requires that this term is an integer or real value.
1515 : : * @return 0 if this term is zero, -1 if this term is a negative real or
1516 : : * integer value, 1 if this term is a positive real or integer value.
1517 : : */
1518 : : int32_t getRealOrIntegerValueSign() const;
1519 : : /**
1520 : : * Determine if this term is an int32 value.
1521 : : * @note This will return true for integer constants and real constants that
1522 : : * have integer value.
1523 : : * @return True if the term is an integral value that fits within int32_t.
1524 : : */
1525 : : bool isInt32Value() const;
1526 : : /**
1527 : : * Get the `int32_t` representation of this integral value.
1528 : : * @note Requires that this term is an int32 value (see isInt32Value()).
1529 : : * @return This integral value as `int32_t` value.
1530 : : */
1531 : : int32_t getInt32Value() const;
1532 : : /**
1533 : : * Determine if this term is a uint32 value.
1534 : : * @note This will return true for integer constants and real constants that
1535 : : * have integral value.
1536 : : * @return True if the term is an integral value and fits within uint32_t.
1537 : : */
1538 : : bool isUInt32Value() const;
1539 : : /**
1540 : : * Get the `uint32_t` representation of this integral value.
1541 : : * @note Requires that this term is a uint32 value (see isUInt32Value()).
1542 : : * @return This integral value as a `uint32_t`.
1543 : : */
1544 : : uint32_t getUInt32Value() const;
1545 : : /**
1546 : : * Determine if this term is an int64 value.
1547 : : * @note This will return true for integer constants and real constants that
1548 : : * have integral value.
1549 : : * @return True if the term is an integral value and fits within int64_t.
1550 : : */
1551 : : bool isInt64Value() const;
1552 : : /**
1553 : : * Get the `int64_t` representation of this integral value.
1554 : : * @note Requires that this term is an int64 value (see isInt64Value()).
1555 : : * @return This integral value as a `int64_t`.
1556 : : */
1557 : : int64_t getInt64Value() const;
1558 : : /**
1559 : : * Determine if this term is a uint64 value.
1560 : : * @note This will return true for integer constants and real constants that
1561 : : * have integral value.
1562 : : * @return True if the term is an integral value that fits within uint64_t.
1563 : : */
1564 : : bool isUInt64Value() const;
1565 : : /**
1566 : : * Get the `uint64_t` representation of this integral value.
1567 : : * @note Requires that this term is an uint64 value (see isUInt64Value()).
1568 : : * @return This integral value as a `uint64_t`.
1569 : : */
1570 : : uint64_t getUInt64Value() const;
1571 : : /**
1572 : : * Determine if this term is an integral value.
1573 : : * @return True if the term is an integer constant or a real constant that
1574 : : * has an integral value.
1575 : : */
1576 : : bool isIntegerValue() const;
1577 : : /**
1578 : : * Get a string representation of this integral value.
1579 : : * @note Requires that this term is an integral value (see isIntegerValue()).
1580 : : * @return The integral term in (decimal) string representation.
1581 : : */
1582 : : std::string getIntegerValue() const;
1583 : :
1584 : : /**
1585 : : * Determine if this term is a string value.
1586 : : * @return True if the term is a string value.
1587 : : */
1588 : : bool isStringValue() const;
1589 : : /**
1590 : : * Get the native string representation of a string value.
1591 : : * @note Requires that this term is a string value (see isStringValue()).
1592 : : * @note This is not to be confused with toString(), which returns
1593 : : * some string representation of the term, whatever data it may hold.
1594 : : * @return The string term as a native string value.
1595 : : * @warning This function is deprecated and replaced by
1596 : : * Term::getU32StringValue(). It will be removed in a future
1597 : : * release.
1598 : : */
1599 : : [[deprecated("Use Term::getU32StringValue() instead")]] std::wstring
1600 : : getStringValue() const;
1601 : : /**
1602 : : * Get the native UTF-32 string representation of a string value.
1603 : : * @note Requires that this term is a string value (see isStringValue()).
1604 : : * @note This is not to be confused with toString(), which returns
1605 : : * some string representation of the term, whatever data it may hold.
1606 : : * @return The string term as a native UTF-32 string value.
1607 : : */
1608 : : std::u32string getU32StringValue() const;
1609 : :
1610 : : /**
1611 : : * Determine if this term is a rational value whose numerator fits into an
1612 : : * int32 value and its denominator fits into a uint32 value.
1613 : : * @return True if the term is a rational and its numerator and denominator
1614 : : * fit into 32 bit integer values.
1615 : : */
1616 : : bool isReal32Value() const;
1617 : : /**
1618 : : * Get the 32 bit integer representations of the numerator and denominator of
1619 : : * a rational value.
1620 : : * @note Requires that this term is a rational value and its numerator and
1621 : : * denominator fit into 32 bit integer values (see isReal32Value()).
1622 : : * @return The representation of a rational value as a pair of its numerator
1623 : : * and denominator as integer values.
1624 : : */
1625 : : std::pair<int32_t, uint32_t> getReal32Value() const;
1626 : : /**
1627 : : * Determine if this term is a rational value whose numerator fits into an
1628 : : * int64 value and its denominator fits into a uint64 value.
1629 : : * @return True if the term is a rational value whose numerator and
1630 : : * denominator fit within int64_t and uint64_t, respectively.
1631 : : */
1632 : : bool isReal64Value() const;
1633 : : /**
1634 : : * Get the 64 bit integer representations of the numerator and denominator of
1635 : : * a rational value.
1636 : : * @note Requires that this term is a rational value and its numerator and
1637 : : * denominator fit into 64 bit integer values (see isReal64Value()).
1638 : : * @return The representation of a rational value as a pair of its numerator
1639 : : * and denominator.
1640 : : */
1641 : : std::pair<int64_t, uint64_t> getReal64Value() const;
1642 : : /**
1643 : : * Determine if this term is a rational value.
1644 : : * @note A term of kind PI is not considered to be a real value.
1645 : : * @return True if the term is a rational value.
1646 : : */
1647 : : bool isRealValue() const;
1648 : : /**
1649 : : * Get a string representation of this rational value.
1650 : : * @note Requires that this term is a rational value (see isRealValue()).
1651 : : * @return The representation of a rational value as a (rational) string.
1652 : : */
1653 : : std::string getRealValue() const;
1654 : :
1655 : : /**
1656 : : * Determine if this term is a constant array.
1657 : : * @return True if the term is a constant array.
1658 : : */
1659 : : bool isConstArray() const;
1660 : : /**
1661 : : * Determine the base (element stored at all indices) of a constant array.
1662 : : * @note Requires that this term is a constant array (see isConstArray()).
1663 : : * @return The base term.
1664 : : */
1665 : : Term getConstArrayBase() const;
1666 : :
1667 : : /**
1668 : : * Determine if this term is a Boolean value.
1669 : : * @return True if the term is a Boolean value.
1670 : : */
1671 : : bool isBooleanValue() const;
1672 : : /**
1673 : : * Get the value of a Boolean term as a native Boolean value.
1674 : : * @note Asserts isBooleanValue().
1675 : : * @return The representation of a Boolean value as a native Boolean value.
1676 : : */
1677 : : bool getBooleanValue() const;
1678 : :
1679 : : /**
1680 : : * Determine if this term is a bit-vector value.
1681 : : * @return True if the term is a bit-vector value.
1682 : : */
1683 : : bool isBitVectorValue() const;
1684 : : /**
1685 : : * Get the string representation of a bit-vector value.
1686 : : *
1687 : : * @note Asserts isBitVectorValue().
1688 : : * @param base `2` for binary, `10` for decimal, and `16` for hexadecimal.
1689 : : * @return The string representation of a bit-vector value.
1690 : : */
1691 : : std::string getBitVectorValue(uint32_t base = 2) const;
1692 : :
1693 : : /**
1694 : : * Determine if this term is a finite field value.
1695 : : * @return True if the term is a finite field value.
1696 : : */
1697 : : bool isFiniteFieldValue() const;
1698 : : /**
1699 : : * Get the string representation of a finite field value (base 10).
1700 : : *
1701 : : * @note Asserts isFiniteFieldValue().
1702 : : *
1703 : : * @note Uses the integer representative of smallest absolute value.
1704 : : *
1705 : : * @return The string representation of the integer representation of this
1706 : : * finite field value.
1707 : : */
1708 : : std::string getFiniteFieldValue() const;
1709 : :
1710 : : /**
1711 : : * Determine if this term is an uninterpreted sort value.
1712 : : * @return True if the term is an abstract value.
1713 : : */
1714 : : bool isUninterpretedSortValue() const;
1715 : : /**
1716 : : * Get a string representation of an uninterpreted sort value.
1717 : : * @note Asserts isUninterpretedSortValue().
1718 : : * @return The representation of an uninterpreted sort value as a string.
1719 : : */
1720 : : std::string getUninterpretedSortValue() const;
1721 : :
1722 : : /**
1723 : : * Determine if this term is a tuple value.
1724 : : * @return True if the term is a tuple value.
1725 : : */
1726 : : bool isTupleValue() const;
1727 : : /**
1728 : : * Get a tuple value as a vector of terms.
1729 : : * @note Asserts isTupleValue().
1730 : : * @return The representation of a tuple value as a vector of terms.
1731 : : */
1732 : : std::vector<Term> getTupleValue() const;
1733 : :
1734 : : /**
1735 : : * Determine if this term is a floating-point rounding mode value.
1736 : : * @return True if the term is a rounding mode value.
1737 : : */
1738 : : bool isRoundingModeValue() const;
1739 : : /**
1740 : : * Get the RoundingMode value of a given rounding-mode value term.
1741 : : * @note Asserts isRoundingModeValue().
1742 : : * @return The floating-point rounding mode value of the term.
1743 : : */
1744 : : RoundingMode getRoundingModeValue() const;
1745 : :
1746 : : /**
1747 : : * Determine if this term is a floating-point positive zero value (+zero).
1748 : : * @return True if the term is the floating-point value for positive zero.
1749 : : */
1750 : : bool isFloatingPointPosZero() const;
1751 : : /**
1752 : : * Determine if this term is a floating-point negative zero value (-zero).
1753 : : * @return True if the term is the floating-point value for negative zero.
1754 : : */
1755 : : bool isFloatingPointNegZero() const;
1756 : : /**
1757 : : * Determine if this term is a floating-point positive infinity value (+oo).
1758 : : * @return True if the term is the floating-point value for positive.
1759 : : * infinity.
1760 : : */
1761 : : bool isFloatingPointPosInf() const;
1762 : : /**
1763 : : * Determine if this term is a floating-point negative infinity value (-oo).
1764 : : * @return True if the term is the floating-point value for negative.
1765 : : * infinity.
1766 : : */
1767 : : bool isFloatingPointNegInf() const;
1768 : : /**
1769 : : * Determine if a given term is a floating-point NaN value.
1770 : : * @return True if the term is the floating-point value for not a number.
1771 : : */
1772 : : bool isFloatingPointNaN() const;
1773 : : /**
1774 : : * Determine if a given term is a floating-point value.
1775 : : * @return True if the term is a floating-point value.
1776 : : */
1777 : : bool isFloatingPointValue() const;
1778 : : /**
1779 : : * Get the representation of a floating-point value as a tuple of its
1780 : : * exponent width, significand width and a bit-vector value term.
1781 : : * @note Asserts isFloatingPointValue().
1782 : : * @return The floating-point value representation.
1783 : : */
1784 : : std::tuple<uint32_t, uint32_t, Term> getFloatingPointValue() const;
1785 : :
1786 : : /**
1787 : : * Determine if this term is a set value.
1788 : : *
1789 : : * A term is a set value if it is considered to be a (canonical) constant set
1790 : : * value. A canonical set value is one whose AST is:
1791 : : *
1792 : : * \verbatim embed:rst:leading-asterisk
1793 : : * .. code:: smtlib
1794 : : *
1795 : : * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
1796 : : * \endverbatim
1797 : : *
1798 : : * where @f$c_1 ... c_n@f$ are values ordered by id such that
1799 : : * @f$c_1 > ... > c_n@f$ (see @ref Term::operator>(const Term&) const).
1800 : : *
1801 : : * @note A universe set term (kind `SET_UNIVERSE`) is not considered to be
1802 : : * a set value.
1803 : : *
1804 : : * @return True if the term is a set value.
1805 : : */
1806 : : bool isSetValue() const;
1807 : : /**
1808 : : * Get a set value as a set of terms.
1809 : : * @note Asserts isSetValue().
1810 : : * @return The representation of a set value as a set of terms.
1811 : : */
1812 : : std::set<Term> getSetValue() const;
1813 : :
1814 : : /**
1815 : : * Determine if this term is a sequence value.
1816 : : *
1817 : : * A term is a sequence value if it has kind #CONST_SEQUENCE. In contrast to
1818 : : * values for the set sort (as described in isSetValue()), a sequence value
1819 : : * is represented as a Term with no children.
1820 : : *
1821 : : * Semantically, a sequence value is a concatenation of unit sequences
1822 : : * whose elements are themselves values. For example:
1823 : : *
1824 : : * \verbatim embed:rst:leading-asterisk
1825 : : * .. code:: smtlib
1826 : : *
1827 : : * (seq.++ (seq.unit 0) (seq.unit 1))
1828 : : * \endverbatim
1829 : : *
1830 : : * The above term has two representations in Term. One is as the sequence
1831 : : * concatenation term:
1832 : : *
1833 : : * \rst
1834 : : * .. code:: lisp
1835 : : *
1836 : : * (SEQ_CONCAT (SEQ_UNIT 0) (SEQ_UNIT 1))
1837 : : * \endrst
1838 : : *
1839 : : * where 0 and 1 are the terms corresponding to the integer constants 0 and 1.
1840 : : *
1841 : : * Alternatively, the above term is represented as the constant sequence
1842 : : * value:
1843 : : *
1844 : : * \rst
1845 : : * .. code:: lisp
1846 : : *
1847 : : * CONST_SEQUENCE_{0,1}
1848 : : * \endrst
1849 : : *
1850 : : * where calling getSequenceValue() on the latter returns the vector `{0, 1}`.
1851 : : *
1852 : : * The former term is not a sequence value, but the latter term is.
1853 : : *
1854 : : * Constant sequences cannot be constructed directly via the API. They are
1855 : : * returned in response to API calls such Solver::getValue() and
1856 : : * Solver::simplify().
1857 : : *
1858 : : * @return True if the term is a sequence value.
1859 : : */
1860 : : bool isSequenceValue() const;
1861 : : /**
1862 : : * Get a sequence value as a vector of terms.
1863 : : * @note Asserts isSequenceValue().
1864 : : * @return The representation of a sequence value as a vector of terms.
1865 : : */
1866 : : std::vector<Term> getSequenceValue() const;
1867 : :
1868 : : /**
1869 : : * Determine if this term is a cardinality constraint.
1870 : : * @return True if the term is a cardinality constraint.
1871 : : */
1872 : : bool isCardinalityConstraint() const;
1873 : : /**
1874 : : * Get a cardinality constraint as a pair of its sort and upper bound.
1875 : : * @note Asserts isCardinalityConstraint().
1876 : : * @return The sort the cardinality constraint is for and its upper bound.
1877 : : */
1878 : : std::pair<Sort, uint32_t> getCardinalityConstraint() const;
1879 : :
1880 : : /**
1881 : : * Determine if this term is a real algebraic number.
1882 : : * @return True if the term is a real algebraic number.
1883 : : */
1884 : : bool isRealAlgebraicNumber() const;
1885 : : /**
1886 : : * Get the defining polynomial for a real algebraic number term, expressed in
1887 : : * terms of the given variable.
1888 : : * @note Asserts isRealAlgebraicNumber().
1889 : : * @param v The variable over which to express the polynomial.
1890 : : * @return The defining polynomial.
1891 : : */
1892 : : Term getRealAlgebraicNumberDefiningPolynomial(const Term& v) const;
1893 : : /**
1894 : : * Get the lower bound for a real algebraic number value.
1895 : : * @note Asserts isRealAlgebraicNumber().
1896 : : * @return The lower bound.
1897 : : */
1898 : : Term getRealAlgebraicNumberLowerBound() const;
1899 : : /**
1900 : : * Get the upper bound for a real algebraic number value.
1901 : : * @note Asserts isRealAlgebraicNumber().
1902 : : * @return The upper bound.
1903 : : */
1904 : : Term getRealAlgebraicNumberUpperBound() const;
1905 : :
1906 : : /**
1907 : : * Is this term a skolem?
1908 : : * @warning This function is experimental and may change in future versions.
1909 : : * @return True if this term is a skolem function.
1910 : : */
1911 : : bool isSkolem() const;
1912 : : /**
1913 : : * Get skolem identifier of this term.
1914 : : * @note Asserts isSkolem().
1915 : : * @warning This function is experimental and may change in future versions.
1916 : : * @return The skolem identifier of this term.
1917 : : */
1918 : : SkolemId getSkolemId() const;
1919 : : /**
1920 : : * Get the skolem indices of this term.
1921 : : * @note Asserts isSkolem().
1922 : : * @warning This function is experimental and may change in future versions.
1923 : : * @return The skolem indices of this term. This is list of terms that the
1924 : : * skolem function is indexed by. For example, the array diff skolem
1925 : : * `SkolemId::ARRAY_DEQ_DIFF` is indexed by two arrays.
1926 : : */
1927 : : std::vector<Term> getSkolemIndices() const;
1928 : :
1929 : : protected:
1930 : : /**
1931 : : * The associated term manager.
1932 : : */
1933 : : TermManager* d_tm = nullptr;
1934 : :
1935 : : private:
1936 : : /** Helper function to collect all elements of a set. */
1937 : : static void collectSet(std::set<Term>& set,
1938 : : const internal::Node& node,
1939 : : TermManager* tm);
1940 : : /** Helper function to collect all elements of a sequence. */
1941 : : static void collectSequence(std::vector<Term>& seq,
1942 : : const internal::Node& node,
1943 : : TermManager* tm);
1944 : :
1945 : : /**
1946 : : * Constructor.
1947 : : * @param tm The associated term manager.
1948 : : * @param n The internal node that is to be wrapped by this term.
1949 : : * @return The Term.
1950 : : */
1951 : : Term(TermManager* tm, const internal::Node& n);
1952 : :
1953 : : /** @return The internal wrapped Node of this term. */
1954 : : const internal::Node& getNode(void) const;
1955 : :
1956 : : /** Helper to convert a vector of Terms to internal Nodes. */
1957 : : std::vector<internal::Node> static termVectorToNodes(
1958 : : const std::vector<Term>& terms);
1959 : : /** Helper to convert a vector of internal Nodes to Terms. */
1960 : : std::vector<Term> static nodeVectorToTerms(
1961 : : TermManager* tm, const std::vector<internal::Node>& nodes);
1962 : :
1963 : : /**
1964 : : * Helper for isNull checks. This prevents calling an API function with
1965 : : * CVC5_API_CHECK_NOT_NULL
1966 : : */
1967 : : bool isNullHelper() const;
1968 : :
1969 : : /**
1970 : : * Helper function that returns the kind of the term, which takes into
1971 : : * account special cases of the conversion for internal to external kinds.
1972 : : * @return The kind of this term.
1973 : : */
1974 : : Kind getKindHelper() const;
1975 : :
1976 : : /**
1977 : : * The internal node wrapped by this term.
1978 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr`` to
1979 : : * avoid overhead due to memory allocation (``internal::Node`` is
1980 : : * already ref counted, so this could be a ``std::unique_ptr`` instead).
1981 : : */
1982 : : std::shared_ptr<internal::Node> d_node;
1983 : : };
1984 : :
1985 : : /**
1986 : : * Serialize a term to given stream.
1987 : : * @param out The output stream.
1988 : : * @param t The term to be serialized to the given output stream.
1989 : : * @return The output stream.
1990 : : */
1991 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Term& t);
1992 : :
1993 : : /**
1994 : : * Serialize a vector of terms to given stream.
1995 : : * @param out The output stream.
1996 : : * @param vector The vector of terms to be serialized to the given stream.
1997 : : * @return The output stream.
1998 : : */
1999 : : CVC5_EXPORT
2000 : : std::ostream& operator<<(std::ostream& out, const std::vector<Term>& vector);
2001 : :
2002 : : /**
2003 : : * Serialize a set of terms to the given stream.
2004 : : * @param out The output stream.
2005 : : * @param set The set of terms to be serialized to the given stream.
2006 : : * @return The output stream.
2007 : : */
2008 : : CVC5_EXPORT
2009 : : std::ostream& operator<<(std::ostream& out, const std::set<Term>& set);
2010 : :
2011 : : /**
2012 : : * Serialize an unordered_set of terms to the given stream.
2013 : : *
2014 : : * @param out The output stream.
2015 : : * @param unordered_set The set of terms to be serialized to the given stream.
2016 : : * @return The output stream.
2017 : : */
2018 : : CVC5_EXPORT
2019 : : std::ostream& operator<<(std::ostream& out,
2020 : : const std::unordered_set<Term>& unordered_set);
2021 : :
2022 : : /**
2023 : : * Serialize a map of terms to the given stream.
2024 : : *
2025 : : * @param out The output stream.
2026 : : * @param map The map of terms to be serialized to the given stream.
2027 : : * @return The output stream.
2028 : : */
2029 : : template <typename V>
2030 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out,
2031 : : const std::map<Term, V>& map);
2032 : :
2033 : : /**
2034 : : * Serialize an unordered_map of terms to the given stream.
2035 : : *
2036 : : * @param out The output stream.
2037 : : * @param unordered_map The map of terms to be serialized to the given stream.
2038 : : * @return The output stream.
2039 : : */
2040 : : template <typename V>
2041 : : CVC5_EXPORT std::ostream& operator<<(
2042 : : std::ostream& out, const std::unordered_map<Term, V>& unordered_map);
2043 : :
2044 : : } // namespace cvc5
2045 : :
2046 : : namespace std {
2047 : : /**
2048 : : * Hash function for Terms.
2049 : : */
2050 : : template <>
2051 : : struct CVC5_EXPORT hash<cvc5::Term>
2052 : : {
2053 : : size_t operator()(const cvc5::Term& t) const;
2054 : : };
2055 : : } // namespace std
2056 : :
2057 : : namespace cvc5 {
2058 : :
2059 : : /* -------------------------------------------------------------------------- */
2060 : : /* Datatypes */
2061 : : /* -------------------------------------------------------------------------- */
2062 : :
2063 : : class DatatypeConstructorIterator;
2064 : : class DatatypeIterator;
2065 : :
2066 : : /**
2067 : : * A cvc5 datatype constructor declaration. A datatype constructor declaration
2068 : : * is a specification used for creating a datatype constructor.
2069 : : */
2070 : : class CVC5_EXPORT DatatypeConstructorDecl
2071 : : {
2072 : : friend class DatatypeDecl;
2073 : : friend class TermManager;
2074 : : friend class Solver;
2075 : : friend struct std::hash<DatatypeConstructorDecl>;
2076 : :
2077 : : public:
2078 : : /** Constructor. */
2079 : : DatatypeConstructorDecl();
2080 : :
2081 : : /**
2082 : : * Destructor.
2083 : : */
2084 : : ~DatatypeConstructorDecl();
2085 : :
2086 : : /**
2087 : : * Equality operator.
2088 : : * @param decl The datatype constructor declaration to compare to for
2089 : : * equality.
2090 : : * @return True if the datatype constructor declarations are equal.
2091 : : */
2092 : : bool operator==(const DatatypeConstructorDecl& decl) const;
2093 : :
2094 : : /**
2095 : : * Add datatype selector declaration.
2096 : : * @param name The name of the datatype selector declaration to add.
2097 : : * @param sort The codomain sort of the datatype selector declaration to add.
2098 : : */
2099 : : void addSelector(const std::string& name, const Sort& sort);
2100 : : /**
2101 : : * Add datatype selector declaration whose codomain type is the datatype
2102 : : * itself.
2103 : : * @param name The name of the datatype selector declaration to add.
2104 : : */
2105 : : void addSelectorSelf(const std::string& name);
2106 : :
2107 : : /**
2108 : : * Add datatype selector declaration whose codomain sort is an unresolved
2109 : : * datatype with the given name.
2110 : : * @param name The name of the datatype selector declaration to add.
2111 : : * @param unresDataypeName The name of the unresolved datatype. The codomain
2112 : : * of the selector will be the resolved datatype with
2113 : : * the given name.
2114 : : */
2115 : : void addSelectorUnresolved(const std::string& name,
2116 : : const std::string& unresDataypeName);
2117 : :
2118 : : /**
2119 : : * @return True if this DatatypeConstructorDecl is a null declaration.
2120 : : */
2121 : : bool isNull() const;
2122 : :
2123 : : /**
2124 : : * @return A string representation of this datatype constructor declaration.
2125 : : */
2126 : : std::string toString() const;
2127 : :
2128 : : private:
2129 : : /**
2130 : : * Constructor.
2131 : : * @param tm The associated term manager.
2132 : : * @param name The name of the datatype constructor.
2133 : : * @return The DatatypeConstructorDecl.
2134 : : */
2135 : : DatatypeConstructorDecl(TermManager* tm, const std::string& name);
2136 : :
2137 : : /**
2138 : : * Helper for isNull checks. This prevents calling an API function with
2139 : : * CVC5_API_CHECK_NOT_NULL
2140 : : */
2141 : : bool isNullHelper() const;
2142 : :
2143 : : /**
2144 : : * Is the underlying constructor resolved (i.e,. has it been used to declare
2145 : : * a datatype already)?
2146 : : */
2147 : : bool isResolved() const;
2148 : :
2149 : : /**
2150 : : * The associated term manager.
2151 : : */
2152 : : TermManager* d_tm = nullptr;
2153 : :
2154 : : /**
2155 : : * The internal (intermediate) datatype constructor wrapped by this
2156 : : * datatype constructor declaration.
2157 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
2158 : : * since ``internal::DTypeConstructor`` is not ref counted.
2159 : : */
2160 : : std::shared_ptr<internal::DTypeConstructor> d_ctor;
2161 : : };
2162 : :
2163 : : } // namespace cvc5
2164 : :
2165 : : namespace std {
2166 : : /**
2167 : : * Hash function for datatype constructor declarations.
2168 : : */
2169 : : template <>
2170 : : struct CVC5_EXPORT hash<cvc5::DatatypeConstructorDecl>
2171 : : {
2172 : : size_t operator()(const cvc5::DatatypeConstructorDecl& decl) const;
2173 : : };
2174 : : } // namespace std
2175 : :
2176 : : namespace cvc5 {
2177 : :
2178 : : class Solver;
2179 : :
2180 : : /**
2181 : : * A cvc5 datatype declaration. A datatype declaration is not itself a datatype
2182 : : * (see Datatype), but a specification for creating a datatype sort.
2183 : : *
2184 : : * The interface for a datatype declaration coincides with the syntax for the
2185 : : * SMT-LIB 2.6 command `declare-datatype`, or a single datatype within the
2186 : : * `declare-datatypes` command.
2187 : : *
2188 : : * Datatype sorts can be constructed from a DatatypeDecl using:
2189 : : * - Solver::mkDatatypeSort()
2190 : : * - Solver::mkDatatypeSorts()
2191 : : */
2192 : : class CVC5_EXPORT DatatypeDecl
2193 : : {
2194 : : friend class DatatypeConstructorArg;
2195 : : friend class TermManager;
2196 : : friend class Solver;
2197 : : friend struct std::hash<DatatypeDecl>;
2198 : :
2199 : : public:
2200 : : /** Constructor. */
2201 : : DatatypeDecl();
2202 : :
2203 : : /**
2204 : : * Destructor.
2205 : : */
2206 : : ~DatatypeDecl();
2207 : :
2208 : : /**
2209 : : * Equality operator.
2210 : : * @param decl The datatype declaration to compare to for equality.
2211 : : * @return True if the datatype declarations are equal.
2212 : : */
2213 : : bool operator==(const DatatypeDecl& decl) const;
2214 : :
2215 : : /**
2216 : : * Add datatype constructor declaration.
2217 : : * @param ctor The datatype constructor declaration to add.
2218 : : */
2219 : : void addConstructor(const DatatypeConstructorDecl& ctor);
2220 : :
2221 : : /**
2222 : : * Get the number of constructors (so far) for this Datatype declaration.
2223 : : * @return The number of constructors.
2224 : : */
2225 : : size_t getNumConstructors() const;
2226 : :
2227 : : /**
2228 : : * Determine if this Datatype declaration is parametric.
2229 : : * @warning This function is experimental and may change in future versions.
2230 : : * @return True if this datatype declaration is parametric.
2231 : : */
2232 : : bool isParametric() const;
2233 : :
2234 : : /**
2235 : : * Determine if this datatype declaration is resolved (has already been used
2236 : : * to declare a datatype).
2237 : : * @return True if this datatype declaration is resolved.
2238 : : */
2239 : : bool isResolved() const;
2240 : :
2241 : : /**
2242 : : * Determine if this datatype declaration is nullary.
2243 : : * @return True if this DatatypeDecl is a null object.
2244 : : */
2245 : : bool isNull() const;
2246 : :
2247 : : /**
2248 : : * Get a string representation of this datatype declaration.
2249 : : * @return A string representation.
2250 : : */
2251 : : std::string toString() const;
2252 : :
2253 : : /**
2254 : : * Get the name of this datatype declaration.
2255 : : * @return The name.
2256 : : */
2257 : : std::string getName() const;
2258 : :
2259 : : private:
2260 : : /**
2261 : : * Constructor.
2262 : : * @param tm The associated term manager.
2263 : : * @param name The name of the datatype.
2264 : : * @param isCoDatatype True if a codatatype is to be constructed.
2265 : : * @return The DatatypeDecl.
2266 : : */
2267 : : DatatypeDecl(TermManager* tm,
2268 : : const std::string& name,
2269 : : bool isCoDatatype = false);
2270 : :
2271 : : /**
2272 : : * Constructor for parameterized datatype declaration.
2273 : : * Create sorts parameter with TermManager::mkParamSort().
2274 : : * @param tm The associated term manager.
2275 : : * @param name The name of the datatype.
2276 : : * @param params A list of sort parameters.
2277 : : * @param isCoDatatype True if a codatatype is to be constructed.
2278 : : */
2279 : : DatatypeDecl(TermManager* tm,
2280 : : const std::string& name,
2281 : : const std::vector<Sort>& params,
2282 : : bool isCoDatatype = false);
2283 : :
2284 : : /** @return The internal wrapped Dtype of this datatype declaration. */
2285 : : internal::DType& getDatatype(void) const;
2286 : :
2287 : : /**
2288 : : * Helper for isNull checks. This prevents calling an API function with
2289 : : * CVC5_API_CHECK_NOT_NULL
2290 : : */
2291 : : bool isNullHelper() const;
2292 : :
2293 : : /**
2294 : : * The associated term manager.
2295 : : */
2296 : : TermManager* d_tm = nullptr;
2297 : :
2298 : : /**
2299 : : * The internal (intermediate) datatype wrapped by this datatype
2300 : : * declaration.
2301 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
2302 : : * since ``internal::DType`` is not ref counted.
2303 : : */
2304 : : std::shared_ptr<internal::DType> d_dtype;
2305 : : };
2306 : :
2307 : : } // namespace cvc5
2308 : :
2309 : : namespace std {
2310 : : /**
2311 : : * Hash function for datatype declarations.
2312 : : */
2313 : : template <>
2314 : : struct CVC5_EXPORT hash<cvc5::DatatypeDecl>
2315 : : {
2316 : : size_t operator()(const cvc5::DatatypeDecl& decl) const;
2317 : : };
2318 : : } // namespace std
2319 : :
2320 : : namespace cvc5 {
2321 : :
2322 : : /**
2323 : : * A cvc5 datatype selector.
2324 : : */
2325 : : class CVC5_EXPORT DatatypeSelector
2326 : : {
2327 : : friend class Datatype;
2328 : : friend class DatatypeConstructor;
2329 : : friend class TermManager;
2330 : : friend struct std::hash<DatatypeSelector>;
2331 : :
2332 : : public:
2333 : : /**
2334 : : * Constructor.
2335 : : */
2336 : : DatatypeSelector();
2337 : :
2338 : : /**
2339 : : * Destructor.
2340 : : */
2341 : : ~DatatypeSelector();
2342 : :
2343 : : /**
2344 : : * Equality operator.
2345 : : * @param sel The datatype selector to compare to for equality.
2346 : : * @return True if the datatype selectors are equal.
2347 : : */
2348 : : bool operator==(const DatatypeSelector& sel) const;
2349 : :
2350 : : /**
2351 : : * Get the name of this datatype selector.
2352 : : * @return The name of this Datatype selector.
2353 : : */
2354 : : std::string getName() const;
2355 : :
2356 : : /**
2357 : : * Get the selector term of this datatype selector.
2358 : : *
2359 : : * Selector terms are a class of function-like terms of selector
2360 : : * sort (Sort::isDatatypeSelector()), and should be used as the first
2361 : : * argument of Terms of kind #APPLY_SELECTOR.
2362 : : *
2363 : : * @return The selector term.
2364 : : */
2365 : : Term getTerm() const;
2366 : :
2367 : : /**
2368 : : * Get the updater term of this datatype selector.
2369 : : *
2370 : : * Similar to selectors, updater terms are a class of function-like terms of
2371 : : * updater Sort (Sort::isDatatypeUpdater()), and should be used as the first
2372 : : * argument of Terms of kind #APPLY_UPDATER.
2373 : : *
2374 : : * @return The updater term.
2375 : : */
2376 : : Term getUpdaterTerm() const;
2377 : :
2378 : : /**
2379 : : * Get the codomain sort of this selector.
2380 : : * @return The codomain sort of this selector.
2381 : : */
2382 : : Sort getCodomainSort() const;
2383 : :
2384 : : /**
2385 : : * @return True if this DatatypeSelector is a null object.
2386 : : */
2387 : : bool isNull() const;
2388 : :
2389 : : /**
2390 : : * Get the string representation of this datatype selector.
2391 : : * @return The string representation.
2392 : : */
2393 : : std::string toString() const;
2394 : :
2395 : : private:
2396 : : /**
2397 : : * Constructor.
2398 : : * @param tm The associated term manager.
2399 : : * @param stor The internal datatype selector to be wrapped.
2400 : : * @return The DatatypeSelector.
2401 : : */
2402 : : DatatypeSelector(TermManager* tm, const internal::DTypeSelector& stor);
2403 : :
2404 : : /**
2405 : : * Helper for isNull checks. This prevents calling an API function with
2406 : : * CVC5_API_CHECK_NOT_NULL
2407 : : */
2408 : : bool isNullHelper() const;
2409 : :
2410 : : /**
2411 : : * The associated term manager.
2412 : : */
2413 : : TermManager* d_tm = nullptr;
2414 : :
2415 : : /**
2416 : : * The internal datatype selector wrapped by this datatype selector.
2417 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
2418 : : * since ``internal::DType`` is not ref counted.
2419 : : */
2420 : : std::shared_ptr<internal::DTypeSelector> d_stor;
2421 : : };
2422 : :
2423 : : } // namespace cvc5
2424 : :
2425 : : namespace std {
2426 : : /**
2427 : : * Hash function for datatype Selectors.
2428 : : */
2429 : : template <>
2430 : : struct CVC5_EXPORT hash<cvc5::DatatypeSelector>
2431 : : {
2432 : : size_t operator()(const cvc5::DatatypeSelector& sel) const;
2433 : : };
2434 : : } // namespace std
2435 : :
2436 : : namespace cvc5 {
2437 : :
2438 : : /**
2439 : : * A cvc5 datatype constructor.
2440 : : */
2441 : : class CVC5_EXPORT DatatypeConstructor
2442 : : {
2443 : : friend class Datatype;
2444 : : friend class TermManager;
2445 : : friend struct std::hash<DatatypeConstructor>;
2446 : :
2447 : : public:
2448 : : /**
2449 : : * Constructor.
2450 : : */
2451 : : DatatypeConstructor();
2452 : :
2453 : : /**
2454 : : * Destructor.
2455 : : */
2456 : : ~DatatypeConstructor();
2457 : :
2458 : : /**
2459 : : * Equality operator.
2460 : : * @param cons The datatype constructor to compare to for equality.
2461 : : * @return True if the datatype constructors are equal.
2462 : : */
2463 : : bool operator==(const DatatypeConstructor& cons) const;
2464 : :
2465 : : /**
2466 : : * Get the name of this datatype constructor.
2467 : : * @return The name.
2468 : : */
2469 : : std::string getName() const;
2470 : :
2471 : : /**
2472 : : * Get the constructor term of this datatype constructor.
2473 : : *
2474 : : * Datatype constructors are a special class of function-like terms whose sort
2475 : : * is datatype constructor (Sort::isDatatypeConstructor()). All datatype
2476 : : * constructors, including nullary ones, should be used as the
2477 : : * first argument to Terms whose kind is #APPLY_CONSTRUCTOR. For example,
2478 : : * the nil list can be constructed by
2479 : : * `TermManager::mkTerm(Kind::APPLY_CONSTRUCTOR, {t})`, where `t` is the term
2480 : : * returned by this function.
2481 : : *
2482 : : * @note This function should not be used for parametric datatypes. Instead,
2483 : : * use the function DatatypeConstructor::getInstantiatedTerm() below.
2484 : : *
2485 : : * @return The constructor term.
2486 : : */
2487 : : Term getTerm() const;
2488 : :
2489 : : /**
2490 : : * Get the constructor term of this datatype constructor whose return
2491 : : * type is `retSort`.
2492 : : *
2493 : : * This function is intended to be used on constructors of parametric
2494 : : * datatypes and can be seen as returning the constructor term that has been
2495 : : * explicitly cast to the given sort.
2496 : : *
2497 : : * This function is required for constructors of parametric datatypes whose
2498 : : * return type cannot be determined by type inference. For example, given:
2499 : : *
2500 : : * \verbatim embed:rst:leading-asterisk
2501 : : * .. code:: smtlib
2502 : : *
2503 : : * (declare-datatype List
2504 : : * (par (T) ((nil) (cons (head T) (tail (List T))))))
2505 : : * \endverbatim
2506 : : *
2507 : : * The type of nil terms must be provided by the user. In SMT version 2.6,
2508 : : * this is done via the syntax for qualified identifiers:
2509 : : *
2510 : : * \verbatim embed:rst:leading-asterisk
2511 : : * .. code:: smtlib
2512 : : *
2513 : : * (as nil (List Int))
2514 : : * \endverbatim
2515 : : *
2516 : : * This function is equivalent of applying the above, where this
2517 : : * DatatypeConstructor is the one corresponding to `nil`, and `retSort` is
2518 : : * `(List Int)`.
2519 : : *
2520 : : * @note The returned constructor term `t` is used to construct the above
2521 : : * (nullary) application of `nil` with
2522 : : * `TermManager::mkTerm(Kind::APPLY_CONSTRUCTOR, {t})`.
2523 : : *
2524 : : * @warning This function is experimental and may change in future versions.
2525 : : *
2526 : : * @param retSort The desired return sort of the constructor.
2527 : : * @return The constructor term.
2528 : : */
2529 : : Term getInstantiatedTerm(const Sort& retSort) const;
2530 : :
2531 : : /**
2532 : : * Get the tester term of this datatype constructor.
2533 : : *
2534 : : * Similar to constructors, testers are a class of function-like terms of
2535 : : * tester sort (Sort::isDatatypeConstructor()) which should be used as the
2536 : : * first argument of Terms of kind #APPLY_TESTER.
2537 : : *
2538 : : * @return The tester term.
2539 : : */
2540 : : Term getTesterTerm() const;
2541 : :
2542 : : /**
2543 : : * @return The number of selectors (so far) of this Datatype constructor.
2544 : : */
2545 : : size_t getNumSelectors() const;
2546 : :
2547 : : /** @return The i^th DatatypeSelector. */
2548 : : DatatypeSelector operator[](size_t index) const;
2549 : : /**
2550 : : * Get the datatype selector with the given name.
2551 : : * @note This is a linear search through the selectors, so in case of
2552 : : * multiple, similarly-named selectors, the first is returned.
2553 : : * @param name The name of the datatype selector.
2554 : : * @return The first datatype selector with the given name.
2555 : : */
2556 : : DatatypeSelector operator[](const std::string& name) const;
2557 : : /**
2558 : : * Get the datatype selector with the given name.
2559 : : * @note This is a linear search through the selectors, so in case of
2560 : : * multiple, similarly-named selectors, the first is returned.
2561 : : * @param name The name of the datatype selector.
2562 : : * @return The first datatype selector with the given name.
2563 : : */
2564 : : DatatypeSelector getSelector(const std::string& name) const;
2565 : :
2566 : : /**
2567 : : * @return True if this DatatypeConstructor is a null object.
2568 : : */
2569 : : bool isNull() const;
2570 : :
2571 : : /**
2572 : : * Get a string representation of this datatype constructor.
2573 : : * @return The string representation.
2574 : : */
2575 : : std::string toString() const;
2576 : :
2577 : : /**
2578 : : * Iterator for the selectors of a datatype constructor.
2579 : : */
2580 : : class CVC5_EXPORT const_iterator
2581 : : {
2582 : : friend class DatatypeConstructor; // to access constructor
2583 : :
2584 : : public:
2585 : : /* The following types are required by trait std::iterator_traits */
2586 : :
2587 : : /** Iterator tag */
2588 : : using iterator_category = std::forward_iterator_tag;
2589 : :
2590 : : /** The type of the item */
2591 : : using value_type = DatatypeConstructor;
2592 : :
2593 : : /** The pointer type of the item */
2594 : : using pointer = const DatatypeConstructor*;
2595 : :
2596 : : /** The reference type of the item */
2597 : : using reference = const DatatypeConstructor&;
2598 : :
2599 : : /** The type returned when two iterators are subtracted */
2600 : : using difference_type = std::ptrdiff_t;
2601 : :
2602 : : /* End of std::iterator_traits required types */
2603 : :
2604 : : /** Nullary constructor (required for Cython). */
2605 : : const_iterator();
2606 : :
2607 : : /**
2608 : : * Equality operator.
2609 : : * @param it The iterator to compare to for equality.
2610 : : * @return True if the iterators are equal.
2611 : : */
2612 : : bool operator==(const const_iterator& it) const;
2613 : :
2614 : : /**
2615 : : * Disequality operator.
2616 : : * @param it The iterator to compare to for disequality.
2617 : : * @return True if the iterators are disequal.
2618 : : */
2619 : : bool operator!=(const const_iterator& it) const;
2620 : :
2621 : : /**
2622 : : * Increment operator (prefix).
2623 : : * @return A reference to the iterator after incrementing by one.
2624 : : */
2625 : : const_iterator& operator++();
2626 : :
2627 : : /**
2628 : : * Increment operator (postfix).
2629 : : * @return A reference to the iterator after incrementing by one.
2630 : : */
2631 : : const_iterator operator++(int);
2632 : :
2633 : : /**
2634 : : * Dereference operator.
2635 : : * @return A reference to the selector this iterator points to.
2636 : : */
2637 : : const DatatypeSelector& operator*() const;
2638 : :
2639 : : /**
2640 : : * Dereference operator.
2641 : : * @return A pointer to the selector this iterator points to.
2642 : : */
2643 : : const DatatypeSelector* operator->() const;
2644 : :
2645 : : private:
2646 : : /**
2647 : : * Constructor.
2648 : : * @param tm The associated term manager.
2649 : : * @param ctor The internal datatype constructor to iterate over.
2650 : : * @param begin True if this is a `begin()` iterator.
2651 : : */
2652 : : const_iterator(TermManager* tm,
2653 : : const internal::DTypeConstructor& ctor,
2654 : : bool begin);
2655 : :
2656 : : /**
2657 : : * The associated term manager.
2658 : : */
2659 : : TermManager* d_tm = nullptr;
2660 : :
2661 : : /**
2662 : : * A pointer to the list of selectors of the internal datatype
2663 : : * constructor to iterate over.
2664 : : * This pointer is maintained for operators == and != only.
2665 : : */
2666 : : const void* d_int_stors;
2667 : :
2668 : : /** The list of datatype selector (wrappers) to iterate over. */
2669 : : std::vector<DatatypeSelector> d_stors;
2670 : :
2671 : : /** The current index of the iterator. */
2672 : : size_t d_idx;
2673 : : };
2674 : :
2675 : : /**
2676 : : * @return An iterator to the first selector of this constructor.
2677 : : */
2678 : : const_iterator begin() const;
2679 : :
2680 : : /**
2681 : : * @return An iterator to one-off-the-last selector of this constructor.
2682 : : */
2683 : : const_iterator end() const;
2684 : :
2685 : : private:
2686 : : /**
2687 : : * Constructor.
2688 : : * @param tm The associated term manager.
2689 : : * @param ctor The internal datatype constructor to be wrapped.
2690 : : * @return The DatatypeConstructor.
2691 : : */
2692 : : DatatypeConstructor(TermManager* tm, const internal::DTypeConstructor& ctor);
2693 : :
2694 : : /**
2695 : : * Return selector for name.
2696 : : * @param name The name of selector to find.
2697 : : * @return The selector object for the name.
2698 : : */
2699 : : DatatypeSelector getSelectorForName(const std::string& name) const;
2700 : :
2701 : : /**
2702 : : * Helper for isNull checks. This prevents calling an API function with
2703 : : * CVC5_API_CHECK_NOT_NULL
2704 : : */
2705 : : bool isNullHelper() const;
2706 : :
2707 : : /**
2708 : : * The associated term manager.
2709 : : */
2710 : : TermManager* d_tm = nullptr;
2711 : :
2712 : : /**
2713 : : * The internal datatype constructor wrapped by this datatype constructor.
2714 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
2715 : : * since ``internal::DType`` is not ref counted.
2716 : : */
2717 : : std::shared_ptr<internal::DTypeConstructor> d_ctor;
2718 : : };
2719 : :
2720 : : } // namespace cvc5
2721 : :
2722 : : namespace std {
2723 : : /**
2724 : : * Hash function for datatype constructors.
2725 : : */
2726 : : template <>
2727 : : struct CVC5_EXPORT hash<cvc5::DatatypeConstructor>
2728 : : {
2729 : : size_t operator()(const cvc5::DatatypeConstructor& cons) const;
2730 : : };
2731 : : } // namespace std
2732 : :
2733 : : namespace cvc5 {
2734 : :
2735 : : /**
2736 : : * A cvc5 datatype.
2737 : : */
2738 : : class CVC5_EXPORT Datatype
2739 : : {
2740 : : friend class TermManager;
2741 : : friend class Sort;
2742 : : friend struct std::hash<Datatype>;
2743 : :
2744 : : public:
2745 : : /** Constructor. */
2746 : : Datatype();
2747 : :
2748 : : /**
2749 : : * Destructor.
2750 : : */
2751 : : ~Datatype();
2752 : :
2753 : : /**
2754 : : * Equality operator.
2755 : : * @param dt The datatype to compare to for equality.
2756 : : * @return True if the datatypes are equal.
2757 : : */
2758 : : bool operator==(const Datatype& dt) const;
2759 : :
2760 : : /**
2761 : : * Get the datatype constructor at a given index.
2762 : : * @param idx The index of the datatype constructor to return.
2763 : : * @return The datatype constructor with the given index.
2764 : : */
2765 : : DatatypeConstructor operator[](size_t idx) const;
2766 : :
2767 : : /**
2768 : : * Get the datatype constructor with the given name.
2769 : : * @note This is a linear search through the constructors, so in case of
2770 : : * multiple, similarly-named constructors, the first is returned.
2771 : : * @param name The name of the datatype constructor.
2772 : : * @return The datatype constructor with the given name.
2773 : : */
2774 : : DatatypeConstructor operator[](const std::string& name) const;
2775 : : DatatypeConstructor getConstructor(const std::string& name) const;
2776 : :
2777 : : /**
2778 : : * Get the datatype selector with the given name.
2779 : : * @note This is a linear search through the constructors and their
2780 : : * selectors, so in case of multiple, similarly-named selectors, the
2781 : : * first is returned.
2782 : : * @param name The name of the datatype selector.
2783 : : * @return The datatype selector with the given name.
2784 : : */
2785 : : DatatypeSelector getSelector(const std::string& name) const;
2786 : :
2787 : : /**
2788 : : * Get the name of this datatype.
2789 : : * @return The name.
2790 : : */
2791 : : std::string getName() const;
2792 : :
2793 : : /**
2794 : : * Get the number of constructors of this datatype.
2795 : : * @return The number of constructors.
2796 : : */
2797 : : size_t getNumConstructors() const;
2798 : :
2799 : : /**
2800 : : * Get the parameters of this datatype, if it is parametric.
2801 : : *
2802 : : * @note Asserts that this datatype is parametric.
2803 : : *
2804 : : * @warning This function is experimental and may change in future versions.
2805 : : *
2806 : : * @return The parameters of this datatype.
2807 : : */
2808 : : std::vector<Sort> getParameters() const;
2809 : :
2810 : : /**
2811 : : * Determine if this datatype is parametric.
2812 : : * @warning This function is experimental and may change in future versions.
2813 : : * @return True if this datatype is parametric.
2814 : : */
2815 : : bool isParametric() const;
2816 : :
2817 : : /**
2818 : : * Determine if this datatype corresponds to a co-datatype.
2819 : : * @return True if this datatype corresponds to a co-datatype.
2820 : : */
2821 : : bool isCodatatype() const;
2822 : :
2823 : : /**
2824 : : * Determine if this datatype corresponds to a tuple.
2825 : : * @return True if this datatype corresponds to a tuple.
2826 : : */
2827 : : bool isTuple() const;
2828 : :
2829 : : /**
2830 : : * Determine if this datatype corresponds to a record.
2831 : : * @warning This function is experimental and may change in future versions.
2832 : : * @return True if this datatype corresponds to a record.
2833 : : */
2834 : : bool isRecord() const;
2835 : :
2836 : : /**
2837 : : * Determine if a given datatype is finite.
2838 : : * @return True if this datatype is finite.
2839 : : */
2840 : : bool isFinite() const;
2841 : :
2842 : : /**
2843 : : * Determine if this datatype is well-founded.
2844 : : *
2845 : : * If this datatype is not a codatatype, this returns false if there are no
2846 : : * values of this datatype that are of finite size.
2847 : : *
2848 : : * @return True if this datatype is well-founded.
2849 : : */
2850 : : bool isWellFounded() const;
2851 : :
2852 : : /**
2853 : : * @return True if this Datatype is a null object.
2854 : : */
2855 : : bool isNull() const;
2856 : :
2857 : : /**
2858 : : * @return A string representation of this datatype.
2859 : : */
2860 : : std::string toString() const;
2861 : :
2862 : : /**
2863 : : * Iterator for the constructors of a datatype.
2864 : : */
2865 : : class CVC5_EXPORT const_iterator
2866 : : {
2867 : : friend class Datatype; // to access constructor
2868 : :
2869 : : public:
2870 : : /* The following types are required by trait std::iterator_traits */
2871 : :
2872 : : /** Iterator tag */
2873 : : using iterator_category = std::forward_iterator_tag;
2874 : :
2875 : : /** The type of the item */
2876 : : using value_type = Datatype;
2877 : :
2878 : : /** The pointer type of the item */
2879 : : using pointer = const Datatype*;
2880 : :
2881 : : /** The reference type of the item */
2882 : : using reference = const Datatype&;
2883 : :
2884 : : /** The type returned when two iterators are subtracted */
2885 : : using difference_type = std::ptrdiff_t;
2886 : :
2887 : : /* End of std::iterator_traits required types */
2888 : :
2889 : : /** Nullary constructor (required for Cython). */
2890 : : const_iterator();
2891 : :
2892 : : /**
2893 : : * Equality operator.
2894 : : * @param it The iterator to compare to for equality.
2895 : : * @return True if the iterators are equal.
2896 : : */
2897 : : bool operator==(const const_iterator& it) const;
2898 : :
2899 : : /**
2900 : : * Disequality operator.
2901 : : * @param it The iterator to compare to for disequality.
2902 : : * @return True if the iterators are disequal.
2903 : : */
2904 : : bool operator!=(const const_iterator& it) const;
2905 : :
2906 : : /**
2907 : : * Increment operator (prefix).
2908 : : * @return A reference to the iterator after incrementing by one.
2909 : : */
2910 : : const_iterator& operator++();
2911 : :
2912 : : /**
2913 : : * Increment operator (postfix).
2914 : : * @return A reference to the iterator after incrementing by one.
2915 : : */
2916 : : const_iterator operator++(int);
2917 : :
2918 : : /**
2919 : : * Dereference operator.
2920 : : * @return A reference to the constructor this iterator points to.
2921 : : */
2922 : : const DatatypeConstructor& operator*() const;
2923 : :
2924 : : /**
2925 : : * Dereference operator.
2926 : : * @return A pointer to the constructor this iterator points to.
2927 : : */
2928 : : const DatatypeConstructor* operator->() const;
2929 : :
2930 : : private:
2931 : : /**
2932 : : * Constructor.
2933 : : * @param tm The associated term manager.
2934 : : * @param dtype The internal datatype to iterate over.
2935 : : * @param begin True if this is a begin() iterator.
2936 : : */
2937 : : const_iterator(TermManager* tm, const internal::DType& dtype, bool begin);
2938 : :
2939 : : /**
2940 : : * The associated term manager.
2941 : : */
2942 : : TermManager* d_tm = nullptr;
2943 : :
2944 : : /**
2945 : : * A pointer to the list of constructors of the internal datatype
2946 : : * to iterate over.
2947 : : * This pointer is maintained for operators == and != only.
2948 : : */
2949 : : const void* d_int_ctors;
2950 : :
2951 : : /** The list of datatype constructor (wrappers) to iterate over. */
2952 : : std::vector<DatatypeConstructor> d_ctors;
2953 : :
2954 : : /** The current index of the iterator. */
2955 : : size_t d_idx;
2956 : : };
2957 : :
2958 : : /**
2959 : : * @return An iterator to the first constructor of this datatype.
2960 : : */
2961 : : const_iterator begin() const;
2962 : :
2963 : : /**
2964 : : * @return An iterator to one-off-the-last constructor of this datatype.
2965 : : */
2966 : : const_iterator end() const;
2967 : :
2968 : : private:
2969 : : /**
2970 : : * Constructor.
2971 : : * @param tm The associated term manager.
2972 : : * @param dtype The internal datatype to be wrapped.
2973 : : * @return The Datatype.
2974 : : */
2975 : : Datatype(TermManager* tm, const internal::DType& dtype);
2976 : :
2977 : : /**
2978 : : * Return constructor for name.
2979 : : * @param name The name of constructor to find.
2980 : : * @return The constructor object for the name.
2981 : : */
2982 : : DatatypeConstructor getConstructorForName(const std::string& name) const;
2983 : :
2984 : : /**
2985 : : * Return selector for name.
2986 : : * @param name The name of selector to find.
2987 : : * @return The selector object for the name.
2988 : : */
2989 : : DatatypeSelector getSelectorForName(const std::string& name) const;
2990 : :
2991 : : /**
2992 : : * Helper for isNull checks. This prevents calling an API function with
2993 : : * CVC5_API_CHECK_NOT_NULL
2994 : : */
2995 : : bool isNullHelper() const;
2996 : :
2997 : : /**
2998 : : * The associated term manager.
2999 : : */
3000 : : TermManager* d_tm = nullptr;
3001 : :
3002 : : /**
3003 : : * The internal datatype wrapped by this datatype.
3004 : : * @note This is a ``std::shared_ptr`` rather than a ``std::unique_ptr``
3005 : : * since ``internal::DType`` is not ref counted.
3006 : : */
3007 : : std::shared_ptr<internal::DType> d_dtype;
3008 : : };
3009 : :
3010 : : /**
3011 : : * Serialize a datatype declaration to given stream.
3012 : : * @param out The output stream.
3013 : : * @param dtdecl The datatype declaration to be serialized to the given stream.
3014 : : * @return The output stream.
3015 : : */
3016 : : CVC5_EXPORT
3017 : : std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl);
3018 : :
3019 : : /**
3020 : : * Serialize a datatype constructor declaration to given stream.
3021 : : * @param out The output stream.
3022 : : * @param ctordecl The datatype constructor declaration to be serialized.
3023 : : * @return The output stream.
3024 : : */
3025 : : CVC5_EXPORT
3026 : : std::ostream& operator<<(std::ostream& out,
3027 : : const DatatypeConstructorDecl& ctordecl);
3028 : :
3029 : : /**
3030 : : * Serialize a vector of datatype constructor declarations to given stream.
3031 : : * @param out The output stream.
3032 : : * @param vector The vector of datatype constructor declarations to be.
3033 : : * serialized to the given stream
3034 : : * @return The output stream.
3035 : : */
3036 : : CVC5_EXPORT
3037 : : std::ostream& operator<<(std::ostream& out,
3038 : : const std::vector<DatatypeConstructorDecl>& vector);
3039 : :
3040 : : /**
3041 : : * Serialize a datatype to given stream.
3042 : : * @param out The output stream.
3043 : : * @param dtype The datatype to be serialized to given stream.
3044 : : * @return The output stream.
3045 : : */
3046 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Datatype& dtype);
3047 : :
3048 : : /**
3049 : : * Serialize a datatype constructor to given stream.
3050 : : * @param out The output stream.
3051 : : * @param ctor The datatype constructor to be serialized to given stream.
3052 : : * @return The output stream.
3053 : : */
3054 : : CVC5_EXPORT
3055 : : std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor);
3056 : :
3057 : : /**
3058 : : * Serialize a datatype selector to given stream.
3059 : : * @param out The output stream.
3060 : : * @param stor The datatype selector to be serialized to given stream.
3061 : : * @return The output stream.
3062 : : */
3063 : : CVC5_EXPORT
3064 : : std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor);
3065 : :
3066 : : } // namespace cvc5
3067 : :
3068 : : namespace std {
3069 : : /**
3070 : : * Hash function for datatypes.
3071 : : */
3072 : : template <>
3073 : : struct CVC5_EXPORT hash<cvc5::Datatype>
3074 : : {
3075 : : size_t operator()(const cvc5::Datatype& dt) const;
3076 : : };
3077 : : } // namespace std
3078 : :
3079 : : namespace cvc5 {
3080 : :
3081 : : /* -------------------------------------------------------------------------- */
3082 : : /* Grammar */
3083 : : /* -------------------------------------------------------------------------- */
3084 : :
3085 : : /**
3086 : : * A Sygus Grammar. This class can be used to define a context-free grammar
3087 : : * of terms. Its interface coincides with the definition of grammars
3088 : : * (``GrammarDef``) in the SyGuS IF 2.1 standard.
3089 : : */
3090 : : class CVC5_EXPORT Grammar
3091 : : {
3092 : : friend class parser::Cmd;
3093 : : friend class Solver;
3094 : : friend struct std::hash<Grammar>;
3095 : :
3096 : : public:
3097 : : /**
3098 : : * Nullary constructor. Needed for the Cython API.
3099 : : */
3100 : : Grammar();
3101 : :
3102 : : /**
3103 : : * Destructor for bookeeping.
3104 : : */
3105 : : ~Grammar();
3106 : :
3107 : : /**
3108 : : * Determine if this is the null grammar (Grammar::Grammar()).
3109 : : * @return True if this grammar is the null grammar.
3110 : : */
3111 : : bool isNull() const;
3112 : :
3113 : : /**
3114 : : * Operator overloading for referential equality of two grammars.
3115 : : * @param grammar The grammarto compare to for equality.
3116 : : * @return True if both grammars point to the same internal grammar object.
3117 : : */
3118 : : bool operator==(const Grammar& grammar) const;
3119 : :
3120 : : /**
3121 : : * Referential disequality operator.
3122 : : * @param grammar The grammar to compare to for disequality.
3123 : : * @return True if both grammars point to different internal grammar objects.
3124 : : */
3125 : : bool operator!=(const Grammar& grammar) const;
3126 : :
3127 : : /**
3128 : : * Add `rule` to the set of rules corresponding to `ntSymbol`.
3129 : : * @param ntSymbol The non-terminal to which the rule is added.
3130 : : * @param rule The rule to add.
3131 : : */
3132 : : void addRule(const Term& ntSymbol, const Term& rule);
3133 : :
3134 : : /**
3135 : : * Add `rules` to the set of rules corresponding to `ntSymbol`.
3136 : : * @param ntSymbol The non-terminal to which the rules are added.
3137 : : * @param rules The rules to add.
3138 : : */
3139 : : void addRules(const Term& ntSymbol, const std::vector<Term>& rules);
3140 : :
3141 : : /**
3142 : : * Allow `ntSymbol` to be an arbitrary constant.
3143 : : * @param ntSymbol The non-terminal allowed to be any constant.
3144 : : */
3145 : : void addAnyConstant(const Term& ntSymbol);
3146 : :
3147 : : /**
3148 : : * Allow `ntSymbol` to be any input variable to corresponding
3149 : : * synth-fun/synth-inv with the same sort as `ntSymbol`.
3150 : : * @param ntSymbol The non-terminal allowed to be any input variable.
3151 : : */
3152 : : void addAnyVariable(const Term& ntSymbol);
3153 : :
3154 : : /**
3155 : : * @return A string representation of this grammar.
3156 : : */
3157 : : std::string toString() const;
3158 : :
3159 : : private:
3160 : : /**
3161 : : * Constructor.
3162 : : * @param tm The associated term manager.
3163 : : * @param sygusVars The input variables to synth-fun/synth-var.
3164 : : * @param ntSymbols The non-terminals of this grammar.
3165 : : */
3166 : : Grammar(TermManager* tm,
3167 : : const std::vector<Term>& sygusVars,
3168 : : const std::vector<Term>& ntSymbols);
3169 : :
3170 : : /**
3171 : : * @return The resolved datatype of the Start symbol of the grammar.
3172 : : */
3173 : : Sort resolve();
3174 : :
3175 : : /**
3176 : : * The associated term manager.
3177 : : * @note This is only needed temporarily until deprecated term/sort handling
3178 : : * functions are removed.
3179 : : */
3180 : : TermManager* d_tm;
3181 : : /** The internal representation of this grammar. */
3182 : : std::shared_ptr<internal::SygusGrammar> d_grammar;
3183 : : };
3184 : :
3185 : : /**
3186 : : * Serialize a grammar to given stream.
3187 : : * @param out The output stream.
3188 : : * @param grammar The grammar to be serialized to the given output stream.
3189 : : * @return The output stream.
3190 : : */
3191 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out, const Grammar& grammar);
3192 : :
3193 : : } // namespace cvc5
3194 : :
3195 : : namespace std {
3196 : : /**
3197 : : * Hash function for grammar.
3198 : : */
3199 : : template <>
3200 : : struct CVC5_EXPORT hash<cvc5::Grammar>
3201 : : {
3202 : : size_t operator()(const cvc5::Grammar& grammar) const;
3203 : : };
3204 : : } // namespace std
3205 : :
3206 : : namespace cvc5 {
3207 : :
3208 : : /* -------------------------------------------------------------------------- */
3209 : : /* Options */
3210 : : /* -------------------------------------------------------------------------- */
3211 : :
3212 : : /**
3213 : : * \verbatim embed:rst:leading-asterisk
3214 : : * This class provides type-safe access to a few options that frontends are
3215 : : * likely to use, but can not be not be communicated appropriately via the
3216 : : * regular :cpp:func:`Solver::getOption() <cvc5::Solver::getOption()>` or
3217 : : * :cpp:func:`Solver::getOptionInfo() <cvc5::Solver::getOptionInfo()>`
3218 : : * functions. This includes, e.g., the input and output streams that can be
3219 : : * configured via :ref:`err <lbl-option-err>`, :ref:`in <lbl-option-in>` and
3220 : : * :ref:`out <lbl-option-out>`. This class does not store the options itself,
3221 : : * but only acts as a wrapper to the solver object. It can thus no longer be
3222 : : * used after the solver object has been destroyed. \endverbatim
3223 : : */
3224 : : class CVC5_EXPORT DriverOptions
3225 : : {
3226 : : friend class Solver;
3227 : :
3228 : : public:
3229 : : /** Access the solver's input stream */
3230 : : std::istream& in() const;
3231 : : /** Access the solver's error output stream */
3232 : : std::ostream& err() const;
3233 : : /** Access the solver's output stream */
3234 : : std::ostream& out() const;
3235 : :
3236 : : private:
3237 : : DriverOptions(const Solver& solver);
3238 : : const Solver& d_solver;
3239 : : };
3240 : :
3241 : : /**
3242 : : * \verbatim embed:rst:leading-asterisk
3243 : : * Holds information about a specific option, including its name, its
3244 : : * aliases, whether the option was explicitly set by the user, and information
3245 : : * concerning its value. It can be obtained via
3246 : : * :cpp:func:`Solver::getOptionInfo() <cvc5::Solver::getOptionInfo()>` and
3247 : : * allows for a more detailed inspection of options than
3248 : : * :cpp:func:`Solver::getOption() <cvc5::Solver::getOption()>`. The
3249 : : * :cpp:member:`valueInfo <cvc5::OptionInfo::valueInfo>` member holds any of the
3250 : : * following alternatives:
3251 : : *
3252 : : * - :cpp:class:`VoidInfo <cvc5::OptionInfo::VoidInfo>` if the option holds no
3253 : : * value (or the value has no native type)
3254 : : * - :cpp:class:`ValueInfo <cvc5::OptionInfo::ValueInfo>` if the option is of
3255 : : * type ``bool`` or ``std::string``, holds the current value and the default
3256 : : * value.
3257 : : * - :cpp:class:`NumberInfo <cvc5::OptionInfo::NumberInfo>` if the option is of
3258 : : * type ``int64_t``, ``uint64_t`` or ``double``, holds the current and default
3259 : : * value, as well as the minimum and maximum.
3260 : : * - :cpp:class:`ModeInfo <cvc5::OptionInfo::ModeInfo>` if the option is a mode
3261 : : * option, holds the current and default values, as well as a list of valid
3262 : : * modes.
3263 : : *
3264 : : * Additionally, this class provides convenience functions to obtain the
3265 : : * current value of an option in a type-safe manner using :cpp:func:`boolValue()
3266 : : * <cvc5::OptionInfo::boolValue()>`, :cpp:func:`stringValue()
3267 : : * <cvc5::OptionInfo::stringValue()>`, :cpp:func:`intValue()
3268 : : * <cvc5::OptionInfo::intValue()>`, :cpp:func:`uintValue()
3269 : : * <cvc5::OptionInfo::uintValue()>` and :cpp:func:`doubleValue()
3270 : : * <cvc5::OptionInfo::doubleValue()>`. They assert that the option has the
3271 : : * respective type and return the current value.
3272 : : *
3273 : : * If the option has a special type that is not covered by the above
3274 : : * alternatives, the :cpp:member:`valueInfo <cvc5::OptionInfo::valueInfo>` holds
3275 : : * a :cpp:class:`VoidInfo <cvc5::OptionInfo::VoidInfo>`. Some options, that are
3276 : : * expected to be used by frontends (e.g., input and output streams) can also
3277 : : * be accessed using :cpp:func:`Solver::getDriverOptions()
3278 : : * <cvc5::Solver::getDriverOptions()>`. \endverbatim
3279 : : */
3280 : : struct CVC5_EXPORT OptionInfo
3281 : : {
3282 : : /** Has no value information. */
3283 : : struct VoidInfo
3284 : : {
3285 : : };
3286 : : /** Basic information for option values. ``T`` can be ``bool`` or
3287 : : * ``std::string``. */
3288 : : template <typename T>
3289 : : struct ValueInfo
3290 : : {
3291 : : /** The default value. */
3292 : : T defaultValue;
3293 : : /** The current value. */
3294 : : T currentValue;
3295 : : };
3296 : : /** Information for numeric values. ``T`` can be ``int64_t``, ``uint64_t`` or
3297 : : * ``double``. */
3298 : : template <typename T>
3299 : : struct NumberInfo
3300 : : {
3301 : : /** The default value. */
3302 : : T defaultValue;
3303 : : /** The current value. */
3304 : : T currentValue;
3305 : : /** The optional minimum value. */
3306 : : std::optional<T> minimum;
3307 : : /** The optional maximum value. */
3308 : : std::optional<T> maximum;
3309 : : };
3310 : : /** Information for mode option values. */
3311 : : struct ModeInfo
3312 : : {
3313 : : /** The default value. */
3314 : : std::string defaultValue;
3315 : : /** The current value. */
3316 : : std::string currentValue;
3317 : : /** The possible modes. */
3318 : : std::vector<std::string> modes;
3319 : : };
3320 : :
3321 : : /** Move assignment operator. */
3322 : : // Note: this is only required to surpress deprecation warnings for deprecated
3323 : : // members of this struct. Can be removed after the deprecated members
3324 : : // have been removed.
3325 : : OptionInfo& operator=(OptionInfo&& info);
3326 : : /** The option name */
3327 : : std::string name;
3328 : : /** The option name aliases */
3329 : : std::vector<std::string> aliases;
3330 : : /** The features not supported with this */
3331 : : std::vector<std::string> noSupports;
3332 : : /** Whether the option was explicitly set by the user */
3333 : : bool setByUser;
3334 : : /**
3335 : : * True if the option is an expert option
3336 : : * @warning This field is deprecated and replaced by `category`. It will be
3337 : : * removed in a future release.
3338 : : */
3339 : : [[deprecated(
3340 : : "Query cvc5::modes::OptionCategory category for EXPERT instead")]] bool
3341 : : isExpert;
3342 : : /**
3343 : : * True if the option is a regular option
3344 : : * @warning This field is deprecated and replaced by `category`. It will be
3345 : : * removed in a future release.
3346 : : */
3347 : : [[deprecated(
3348 : : "Query cvc5::modes::OptionCategory category for REGULAR instead")]] bool
3349 : : isRegular;
3350 : : /** The category of this option. */
3351 : : modes::OptionCategory category;
3352 : : /** Possible types for ``valueInfo``. */
3353 : : using OptionInfoVariant = std::variant<VoidInfo,
3354 : : ValueInfo<bool>,
3355 : : ValueInfo<std::string>,
3356 : : NumberInfo<int64_t>,
3357 : : NumberInfo<uint64_t>,
3358 : : NumberInfo<double>,
3359 : : ModeInfo>;
3360 : : /** The option value information */
3361 : : OptionInfoVariant valueInfo;
3362 : : /**
3363 : : * Get the current value as a `bool`.
3364 : : * @note Asserts that `valueInfo` holds a `bool`.
3365 : : * @return The current value as a `bool`.
3366 : : */
3367 : : bool boolValue() const;
3368 : : /**
3369 : : * Get the current value as a `std::string`.
3370 : : * @note Asserts that `valueInfo` holds a `std::string`.
3371 : : * @return The current value as a `std::string`.
3372 : : */
3373 : : std::string stringValue() const;
3374 : : /**
3375 : : * Get the current value as an `int64_t`.
3376 : : * @note Asserts that `valueInfo` holds an `int64_t`.
3377 : : * @return The current value as a `int64_t`.
3378 : : */
3379 : : int64_t intValue() const;
3380 : : /**
3381 : : * Get the current value as a `uint64_t`.
3382 : : * @note Asserts that `valueInfo` holds a `uint64_t`.
3383 : : * @return The current value as a `uint64_t`.
3384 : : */
3385 : : uint64_t uintValue() const;
3386 : : /**
3387 : : * Obtain the current value as a `double`.
3388 : : * @note Asserts that `valueInfo` holds a `double`.
3389 : : * @return The current value as a `double`.
3390 : : */
3391 : : double doubleValue() const;
3392 : : /**
3393 : : * Get a string representation of an option info.
3394 : : * @return The string representation.
3395 : : */
3396 : : std::string toString() const;
3397 : : };
3398 : :
3399 : : /**
3400 : : * Print an `OptionInfo` object to an output stream.
3401 : : * @param os The output stream.
3402 : : * @param oi The option info.
3403 : : * @return The output stream.
3404 : : */
3405 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& os, const OptionInfo& oi);
3406 : :
3407 : : /* -------------------------------------------------------------------------- */
3408 : : /* Statistics */
3409 : : /* -------------------------------------------------------------------------- */
3410 : :
3411 : : /**
3412 : : * \verbatim embed:rst:leading-asterisk
3413 : : * Represents a snapshot of a single statistic value. See :doc:`/statistics` for
3414 : : * how statistics can be used.
3415 : : *
3416 : : * A value can be of type ``int64_t``, ``double``, ``std::string`` or a
3417 : : * histogram (``std::map<std::string, uint64_t>``).
3418 : : * The value type can be queried (using ``isInt()``, ``isDouble()``, etc.) and
3419 : : * the stored value can be accessed (using ``getInt()``, ``getDouble()``, etc.).
3420 : : *
3421 : : * It is possible to query whether this statistic is an internal statistic by
3422 : : * :cpp:func:`isInternal() <cvc5::Stat::isInternal()>` and whether its value is
3423 : : * the default value by :cpp:func:`isDefault() <cvc5::Stat::isDefault()>`.
3424 : : * \endverbatim
3425 : : */
3426 : : class CVC5_EXPORT Stat
3427 : : {
3428 : : struct StatData;
3429 : :
3430 : : public:
3431 : : friend class Statistics;
3432 : : CVC5_EXPORT friend std::ostream& operator<<(std::ostream& os, const Stat& sv);
3433 : : /** Representation of a histogram: maps names to frequencies. */
3434 : : using HistogramData = std::map<std::string, uint64_t>;
3435 : : /**
3436 : : * Create an empty statistics object.
3437 : : *
3438 : : * On such an object all `isX()` return false and all `getX()` throw an API
3439 : : * exception. It solely exists because it makes implementing bindings for
3440 : : * other languages much easier.
3441 : : */
3442 : : Stat();
3443 : : /** Copy constructor */
3444 : : Stat(const Stat& s);
3445 : : /** Destructor */
3446 : : ~Stat();
3447 : : /** Copy assignment */
3448 : : Stat& operator=(const Stat& s);
3449 : :
3450 : : /**
3451 : : * Determine if this statistic is intended for internal use only.
3452 : : * @return True if this is an internal statistic.
3453 : : */
3454 : : bool isInternal() const;
3455 : : /**
3456 : : * Determine if this statistic holds the default value.
3457 : : * @return True if this is a defaulted statistic.
3458 : : */
3459 : : bool isDefault() const;
3460 : :
3461 : : /**
3462 : : * Determine if this statistic holds an integer value.
3463 : : * @return True if this value is an integer.
3464 : : */
3465 : : bool isInt() const;
3466 : : /**
3467 : : * Get the value of an integer statistic.
3468 : : * @return The integer value.
3469 : : */
3470 : : int64_t getInt() const;
3471 : : /**
3472 : : * Determine if this statistic holds a double value.
3473 : : * @return True if this value is a double.
3474 : : */
3475 : : bool isDouble() const;
3476 : : /**
3477 : : * Get the value of a double statistic.
3478 : : * @return The double value.
3479 : : */
3480 : : double getDouble() const;
3481 : : /**
3482 : : * Determine if this statistic holds a string value.
3483 : : * @return True if this value is a string.
3484 : : */
3485 : : bool isString() const;
3486 : : /**
3487 : : * Get the value of a string statistic.
3488 : : * @return The string value.
3489 : : */
3490 : : const std::string& getString() const;
3491 : : /**
3492 : : * Determine if this statistics holds a histogram.
3493 : : * @return True if this value is a histogram.
3494 : : */
3495 : : bool isHistogram() const;
3496 : : /**
3497 : : * Get the value of a histogram statistic.
3498 : : * @return The histogram value.
3499 : : */
3500 : : const HistogramData& getHistogram() const;
3501 : :
3502 : : /**
3503 : : * Get a string represenation of this statistic.
3504 : : * @return The string represenation.
3505 : : */
3506 : : std::string toString() const;
3507 : :
3508 : : private:
3509 : : Stat(bool internal, bool def, StatData&& sd);
3510 : : /** Whether this statistic is only meant for internal use */
3511 : : bool d_internal;
3512 : : /** Whether this statistic has the default value */
3513 : : bool d_default;
3514 : : std::unique_ptr<StatData> d_data;
3515 : : };
3516 : :
3517 : : /**
3518 : : * Print a `Stat` object to an `std::ostream`.
3519 : : */
3520 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& os, const Stat& stat);
3521 : :
3522 : : /**
3523 : : * \verbatim embed:rst:leading-asterisk
3524 : : * Represents a snapshot of the solver statistics. See :doc:`/statistics` for
3525 : : * how statistics can be used.
3526 : : *
3527 : : * Statistics can be queried from the Solver via
3528 : : * :cpp:func:`Solver::getStatistics()`, and from the TermManager via
3529 : : * :cpp:func:`TermManager::getStatistics()`. A statistics instance obtained
3530 : : * from either call is independent of the :cpp:class:`Solver` (and its
3531 : : * associated :cpp:class:`TermManager` object: it will not change when new
3532 : : * terms are created or the solver's internal statistics do. It will also not
3533 : : * be invalidated if the solver/term manageris destroyed.
3534 : : *
3535 : : * Iterating over this class (via :cpp:func:`Statistics::begin()` and
3536 : : * :cpp:func:`Statistics::end()`) shows only public statistics that have been
3537 : : * changed. By passing appropriate flags to :cpp:func:`Statistics::begin()`,
3538 : : * statistics that are internal, defaulted, or both, can be included as well.
3539 : : * A single statistic value is represented as :cpp:class:`Stat`.
3540 : : * \endverbatim
3541 : : */
3542 : : class CVC5_EXPORT Statistics
3543 : : {
3544 : : public:
3545 : : friend class Solver;
3546 : : friend class TermManager;
3547 : : /** How the statistics are stored internally. */
3548 : : using BaseType = std::map<std::string, Stat>;
3549 : :
3550 : : /** Custom iterator to hide certain statistics from regular iteration */
3551 : : class CVC5_EXPORT iterator
3552 : : {
3553 : : public:
3554 : : friend class Statistics;
3555 : : iterator() = default;
3556 : : BaseType::const_reference operator*() const;
3557 : : BaseType::const_pointer operator->() const;
3558 : : iterator& operator++();
3559 : : iterator operator++(int);
3560 : : iterator& operator--();
3561 : : iterator operator--(int);
3562 : : bool operator==(const iterator& rhs) const;
3563 : : bool operator!=(const iterator& rhs) const;
3564 : :
3565 : : private:
3566 : : iterator(BaseType::const_iterator it,
3567 : : const BaseType& base,
3568 : : bool internal,
3569 : : bool defaulted);
3570 : : bool isVisible() const;
3571 : : BaseType::const_iterator d_it;
3572 : : const BaseType* d_base;
3573 : : bool d_showInternal = false;
3574 : : bool d_showDefault = false;
3575 : : };
3576 : :
3577 : : /** Creates an empty statistics object. */
3578 : : Statistics() = default;
3579 : :
3580 : : /**
3581 : : * Retrieve the statistic with the given name.
3582 : : * @note Asserts that a statistic with the given name actually exists and
3583 : : * throws a CVC5ApiRecoverableException if it does not.
3584 : : * @param name The name of the statistic.
3585 : : * @return The statistic with the given name.
3586 : : */
3587 : : const Stat& get(const std::string& name);
3588 : : /**
3589 : : * Begin iteration over the statistics values.
3590 : : * By default, only entries that are public and have been set
3591 : : * are visible while the others are skipped.
3592 : : * @param internal If set to true, internal statistics are shown as well.
3593 : : * @param defaulted If set to true, defaulted statistics are shown as well.
3594 : : */
3595 : : iterator begin(bool internal = true, bool defaulted = true) const;
3596 : : /** End iteration */
3597 : : iterator end() const;
3598 : :
3599 : : /**
3600 : : * Get a string represenation of this statistics object.
3601 : : * @return The string represenation.
3602 : : */
3603 : : std::string toString() const;
3604 : :
3605 : : private:
3606 : : Statistics(const internal::StatisticsRegistry& reg);
3607 : : /** Internal data */
3608 : : BaseType d_stats;
3609 : : };
3610 : : CVC5_EXPORT std::ostream& operator<<(std::ostream& out,
3611 : : const Statistics& stats);
3612 : :
3613 : : /* -------------------------------------------------------------------------- */
3614 : : /* Plugin */
3615 : : /* -------------------------------------------------------------------------- */
3616 : :
3617 : : /**
3618 : : * A cvc5 plugin.
3619 : : */
3620 : : class CVC5_EXPORT Plugin
3621 : : {
3622 : : friend class Solver;
3623 : :
3624 : : public:
3625 : : Plugin(TermManager& tm);
3626 : 28 : virtual ~Plugin() = default;
3627 : : /**
3628 : : * Call to check, return vector of lemmas to add to the SAT solver.
3629 : : * This method is called periodically, roughly at every SAT decision.
3630 : : *
3631 : : * @return The vector of lemmas to add to the SAT solver.
3632 : : */
3633 : : virtual std::vector<Term> check();
3634 : : /**
3635 : : * Notify SAT clause, called when `clause` is learned by the SAT solver.
3636 : : * @param clause The learned clause.
3637 : : */
3638 : : virtual void notifySatClause(const Term& clause);
3639 : : /**
3640 : : * Notify theory lemma, called when `lemma` is sent by a theory solver.
3641 : : * @param lemma The theory lemma.
3642 : : */
3643 : : virtual void notifyTheoryLemma(const Term& lemma);
3644 : : /**
3645 : : * Get the name of the plugin (for debugging).
3646 : : * @return The name of the plugin.
3647 : : */
3648 : : virtual std::string getName() = 0;
3649 : :
3650 : : private:
3651 : : /** Converter to external */
3652 : : std::shared_ptr<cvc5::PluginInternal> d_pExtToInt;
3653 : : };
3654 : :
3655 : : /* -------------------------------------------------------------------------- */
3656 : : /* Proof */
3657 : : /* -------------------------------------------------------------------------- */
3658 : :
3659 : : /**
3660 : : * A cvc5 proof. Proofs are trees and every proof object corresponds to the
3661 : : * root step of a proof. The branches of the root step are the premises of
3662 : : * the step.
3663 : : */
3664 : : class CVC5_EXPORT Proof
3665 : : {
3666 : : friend class Solver;
3667 : : friend struct std::hash<Proof>;
3668 : :
3669 : : public:
3670 : : /**
3671 : : * Nullary constructor. Needed for the Cython API.
3672 : : */
3673 : : Proof();
3674 : : /*
3675 : : * Destructor.
3676 : : */
3677 : : ~Proof();
3678 : :
3679 : : /**
3680 : : * Determine if this is the null proof (Proof::Proof()).
3681 : : * @return True if this grammar is the null proof.
3682 : : */
3683 : : bool isNull() const;
3684 : :
3685 : : /**
3686 : : * Get the proof rule used by the root step of the proof.
3687 : : * @return The proof rule.
3688 : : */
3689 : : ProofRule getRule() const;
3690 : :
3691 : : /**
3692 : : * Get the proof rewrite rule used by the root step of the proof.
3693 : : *
3694 : : * Requires that `getRule()` does not return #DSL_REWRITE or
3695 : : * #THEORY_REWRITE.
3696 : : *
3697 : : * @return The proof rewrite rule.
3698 : : *
3699 : : */
3700 : : ProofRewriteRule getRewriteRule() const;
3701 : :
3702 : : /** @return The conclusion of the root step of the proof. */
3703 : : Term getResult() const;
3704 : :
3705 : : /** @return The premises of the root step of the proof. */
3706 : : const std::vector<Proof> getChildren() const;
3707 : :
3708 : : /**
3709 : : * @return The arguments of the root step of the proof as a vector of terms.
3710 : : * Some of those terms might be strings.
3711 : : */
3712 : : const std::vector<Term> getArguments() const;
3713 : :
3714 : : /**
3715 : : * Operator overloading for referential equality of two proofs.
3716 : : * @param p The proof to compare to for equality.
3717 : : * @return True if both proofs point to the same internal proof object.
3718 : : */
3719 : : bool operator==(const Proof& p) const;
3720 : :
3721 : : /**
3722 : : * Referential disequality operator.
3723 : : * @param p The proof to compare to for disequality.
3724 : : * @return True if both proofs point to different internal proof objects.
3725 : : */
3726 : : bool operator!=(const Proof& p) const;
3727 : :
3728 : : private:
3729 : : /** Construct a proof by wrapping a ProofNode. */
3730 : : Proof(TermManager* tm, const std::shared_ptr<internal::ProofNode> p);
3731 : :
3732 : : /** The internal proof node wrapped by this proof object. */
3733 : : std::shared_ptr<internal::ProofNode> d_proofNode;
3734 : : /**
3735 : : * The associated term manager.
3736 : : * @note This is only needed temporarily until deprecated term/sort handling
3737 : : * functions are removed.
3738 : : */
3739 : : TermManager* d_tm;
3740 : : };
3741 : :
3742 : : } // namespace cvc5
3743 : :
3744 : : namespace std {
3745 : : /**
3746 : : * Hash function for proofs.
3747 : : */
3748 : : template <>
3749 : : struct CVC5_EXPORT hash<cvc5::Proof>
3750 : : {
3751 : : size_t operator()(const cvc5::Proof& p) const;
3752 : : };
3753 : : } // namespace std
3754 : :
3755 : : namespace cvc5 {
3756 : :
3757 : : /* -------------------------------------------------------------------------- */
3758 : : /* TermManager */
3759 : : /* -------------------------------------------------------------------------- */
3760 : :
3761 : : /**
3762 : : * A cvc5 term manager.
3763 : : */
3764 : : class CVC5_EXPORT TermManager
3765 : : {
3766 : : friend class Sort;
3767 : : friend class Op;
3768 : : friend class Term;
3769 : : friend class DatatypeConstructorDecl;
3770 : : friend class DatatypeDecl;
3771 : : friend class Grammar;
3772 : : friend class Plugin;
3773 : : friend class Solver;
3774 : :
3775 : : public:
3776 : : /** Constructor. */
3777 : : TermManager();
3778 : : /** Destructor. */
3779 : : ~TermManager();
3780 : :
3781 : : /**
3782 : : * Get a snapshot of the current state of the statistic values of this
3783 : : * term manager.
3784 : : *
3785 : : * Term manager statistics are independent from any solver instance. The
3786 : : * returned object is completely decoupled from the term manager and will
3787 : : * not change when the solver is used again.
3788 : : *
3789 : : * @return A snapshot of the current state of the statistic values.
3790 : : */
3791 : : Statistics getStatistics() const;
3792 : :
3793 : : /**
3794 : : * Print the statistics to the given file descriptor, suitable for usage in
3795 : : * signal handlers.
3796 : : * @param fd The file descriptor.
3797 : : */
3798 : : void printStatisticsSafe(int fd) const;
3799 : :
3800 : : /* Sorts -------------------------------------------------------------- */
3801 : :
3802 : : /**
3803 : : * Get the Boolean sort.
3804 : : * @return Sort `Bool`.
3805 : : */
3806 : : Sort getBooleanSort();
3807 : : /**
3808 : : * Get the Integer sort.
3809 : : * @return Sort `Int`.
3810 : : */
3811 : : Sort getIntegerSort();
3812 : : /**
3813 : : * Get the Real sort.
3814 : : * @return Sort `Real`.
3815 : : */
3816 : : Sort getRealSort();
3817 : : /**
3818 : : * Get the regular expression sort.
3819 : : * @return Sort `RegExp`.
3820 : : */
3821 : : Sort getRegExpSort();
3822 : : /**
3823 : : * Get the rounding mode sort.
3824 : : * @return Sort `RoundingMode`.
3825 : : */
3826 : : Sort getRoundingModeSort();
3827 : : /**
3828 : : * Get the string sort.
3829 : : * @return Sort `String`.
3830 : : */
3831 : : Sort getStringSort();
3832 : : /**
3833 : : * Create an array sort.
3834 : : * @param indexSort The array index sort.
3835 : : * @param elemSort The array element sort.
3836 : : * @return The array sort.
3837 : : */
3838 : : Sort mkArraySort(const Sort& indexSort, const Sort& elemSort);
3839 : : /**
3840 : : * Create a bit-vector sort.
3841 : : * @param size The bit-width of the bit-vector sort.
3842 : : * @return The bit-vector sort.
3843 : : */
3844 : : Sort mkBitVectorSort(uint32_t size);
3845 : : /**
3846 : : * Create a floating-point sort.
3847 : : * @param exp The bit-width of the exponent of the floating-point sort.
3848 : : * @param sig The bit-width of the significand of the floating-point sort.
3849 : : * @return The floating-point sort.
3850 : : */
3851 : : Sort mkFloatingPointSort(uint32_t exp, uint32_t sig);
3852 : : /**
3853 : : * Create a finite-field sort from a given string of base n.
3854 : : * @param size The modulus of the field. Must be prime.
3855 : : * @param base The base of the string representation of `size`.
3856 : : * @return The finite-field sort.
3857 : : */
3858 : : Sort mkFiniteFieldSort(const std::string& size, uint32_t base = 10);
3859 : : /**
3860 : : * Create a datatype sort.
3861 : : * @param dtypedecl The datatype declaration from which the sort is created.
3862 : : * @return The datatype sort.
3863 : : */
3864 : : Sort mkDatatypeSort(const DatatypeDecl& dtypedecl);
3865 : : /**
3866 : : * Create a vector of datatype sorts.
3867 : : *
3868 : : * @note The names of the datatype declarations must be distinct.
3869 : : *
3870 : : * @param dtypedecls The datatype declarations from which the sort is created.
3871 : : * @return The datatype sorts.
3872 : : */
3873 : : std::vector<Sort> mkDatatypeSorts(
3874 : : const std::vector<DatatypeDecl>& dtypedecls);
3875 : : /**
3876 : : * Create function sort.
3877 : : * @param sorts The sort of the function arguments.
3878 : : * @param codomain The sort of the function return value.
3879 : : * @return The function sort.
3880 : : */
3881 : : Sort mkFunctionSort(const std::vector<Sort>& sorts, const Sort& codomain);
3882 : : /**
3883 : : * Create a skolem.
3884 : : * @param id The skolem identifier.
3885 : : * @param indices The indices of the skolem.
3886 : : * @return The skolem.
3887 : : */
3888 : : Term mkSkolem(SkolemId id, const std::vector<Term>& indices);
3889 : : /**
3890 : : * Get the number of indices for a skolem id.
3891 : : * @param id The skolem id.
3892 : : * @return The number of indices for the skolem id.
3893 : : */
3894 : : size_t getNumIndicesForSkolemId(SkolemId id);
3895 : : /**
3896 : : * Create a sort parameter.
3897 : : *
3898 : : * @warning This function is experimental and may change in future versions.
3899 : : *
3900 : : * @param symbol The name of the sort.
3901 : : * @return The sort parameter.
3902 : : */
3903 : : Sort mkParamSort(const std::optional<std::string>& symbol = std::nullopt);
3904 : : /**
3905 : : * Create a predicate sort.
3906 : : *
3907 : : * This is equivalent to calling mkFunctionSort() with the Boolean sort as the
3908 : : * codomain.
3909 : : *
3910 : : * @param sorts The list of sorts of the predicate.
3911 : : * @return The predicate sort.
3912 : : */
3913 : : Sort mkPredicateSort(const std::vector<Sort>& sorts);
3914 : : /**
3915 : : * Create a record sort
3916 : : *
3917 : : * @warning This function is experimental and may change in future versions.
3918 : : *
3919 : : * @param fields The list of fields of the record.
3920 : : * @return The record sort.
3921 : : */
3922 : : Sort mkRecordSort(const std::vector<std::pair<std::string, Sort>>& fields);
3923 : : /**
3924 : : * Create a set sort.
3925 : : * @param elemSort The sort of the set elements.
3926 : : * @return The set sort.
3927 : : */
3928 : : Sort mkSetSort(const Sort& elemSort);
3929 : : /**
3930 : : * Create a bag sort.
3931 : : * @param elemSort The sort of the bag elements.
3932 : : * @return The bag sort.
3933 : : */
3934 : : Sort mkBagSort(const Sort& elemSort);
3935 : : /**
3936 : : * Create a sequence sort.
3937 : : * @param elemSort The sort of the sequence elements.
3938 : : * @return The sequence sort.
3939 : : */
3940 : : Sort mkSequenceSort(const Sort& elemSort);
3941 : : /**
3942 : : * Create an abstract sort. An abstract sort represents a sort for a given
3943 : : * kind whose parameters and arguments are unspecified.
3944 : : *
3945 : : * The kind `k` must be the kind of a sort that can be abstracted, i.e., a
3946 : : * sort that has indices or argument sorts. For example, #ARRAY_SORT and
3947 : : * #BITVECTOR_SORT can be passed as the kind `k` to this function, while
3948 : : * #INTEGER_SORT and #STRING_SORT cannot.
3949 : : *
3950 : : * @note Providing the kind #ABSTRACT_SORT as an argument to this function
3951 : : * returns the (fully) unspecified sort, denoted `?`.
3952 : : *
3953 : : * @note Providing a kind `k` that has no indices and a fixed arity
3954 : : * of argument sorts will return the sort of kind `k` whose arguments are the
3955 : : * unspecified sort. For example, `mkAbstractSort(SortKind::ARRAY_SORT)` will
3956 : : * return the sort `(ARRAY_SORT ? ?)` instead of the abstract sort whose
3957 : : * abstract kind is #ARRAY_SORT.
3958 : : *
3959 : : * @param k The kind of the abstract sort
3960 : : * @return The abstract sort.
3961 : : *
3962 : : * @warning This function is experimental and may change in future versions.
3963 : : */
3964 : : Sort mkAbstractSort(SortKind k);
3965 : : /**
3966 : : * Create an uninterpreted sort.
3967 : : * @param symbol The name of the sort.
3968 : : * @return The uninterpreted sort.
3969 : : */
3970 : : Sort mkUninterpretedSort(
3971 : : const std::optional<std::string>& symbol = std::nullopt);
3972 : : /**
3973 : : * Create an unresolved datatype sort.
3974 : : *
3975 : : * This is for creating yet unresolved sort placeholders for mutually
3976 : : * recursive parametric datatypes.
3977 : : *
3978 : : * @param symbol The symbol of the sort.
3979 : : * @param arity The number of sort parameters of the sort.
3980 : : * @return The unresolved sort.
3981 : : *
3982 : : * @warning This function is experimental and may change in future versions.
3983 : : */
3984 : : Sort mkUnresolvedDatatypeSort(const std::string& symbol, size_t arity = 0);
3985 : : /**
3986 : : * Create an uninterpreted sort constructor sort.
3987 : : *
3988 : : * An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
3989 : : *
3990 : : * @param symbol The symbol of the sort.
3991 : : * @param arity The arity of the sort (must be > 0)
3992 : : * @return The uninterpreted sort constructor sort.
3993 : : */
3994 : : Sort mkUninterpretedSortConstructorSort(
3995 : : size_t arity, const std::optional<std::string>& symbol = std::nullopt);
3996 : : /**
3997 : : * Create a tuple sort.
3998 : : * @param sorts The sorts of the elements of the tuple.
3999 : : * @return The tuple sort.
4000 : : */
4001 : : Sort mkTupleSort(const std::vector<Sort>& sorts);
4002 : : /**
4003 : : * Create a nullable sort.
4004 : : * @param sort The sort of the element of the nullable.
4005 : : * @return The nullable sort.
4006 : : */
4007 : : Sort mkNullableSort(const Sort& sort);
4008 : :
4009 : : /* Operators ---------------------------------------------------------- */
4010 : :
4011 : : /**
4012 : : * Create operator of Kind:
4013 : : * - #BITVECTOR_EXTRACT
4014 : : * - #BITVECTOR_REPEAT
4015 : : * - #BITVECTOR_ROTATE_LEFT
4016 : : * - #BITVECTOR_ROTATE_RIGHT
4017 : : * - #BITVECTOR_SIGN_EXTEND
4018 : : * - #BITVECTOR_ZERO_EXTEND
4019 : : * - #DIVISIBLE
4020 : : * - #FLOATINGPOINT_TO_FP_FROM_FP
4021 : : * - #FLOATINGPOINT_TO_FP_FROM_IEEE_BV
4022 : : * - #FLOATINGPOINT_TO_FP_FROM_REAL
4023 : : * - #FLOATINGPOINT_TO_FP_FROM_SBV
4024 : : * - #FLOATINGPOINT_TO_FP_FROM_UBV
4025 : : * - #FLOATINGPOINT_TO_SBV
4026 : : * - #FLOATINGPOINT_TO_UBV
4027 : : * - #INT_TO_BITVECTOR
4028 : : * - #TUPLE_PROJECT
4029 : : *
4030 : : * See cvc5::Kind for a description of the parameters.
4031 : : * @param kind The kind of the operator.
4032 : : * @param args The arguments (indices) of the operator.
4033 : : *
4034 : : * @note If ``args`` is empty, the Op simply wraps the cvc5::Kind. The
4035 : : * Kind can be used in TermManager::mkTerm directly without creating an Op
4036 : : * first.
4037 : : */
4038 : : Op mkOp(Kind kind, const std::vector<uint32_t>& args = {});
4039 : : #ifndef DOXYGEN_SKIP
4040 : : // Overload is only used to disambiguate the std::vector and std::string
4041 : : // overloads.
4042 : : Op mkOp(Kind kind, const std::initializer_list<uint32_t>& args);
4043 : : #endif
4044 : : /**
4045 : : * Create operator of kind:
4046 : : * - #DIVISIBLE (to support arbitrary precision integers)
4047 : : * See cvc5::Kind for a description of the parameters.
4048 : : * @param kind The kind of the operator.
4049 : : * @param arg The string argument to this operator.
4050 : : */
4051 : : Op mkOp(Kind kind, const std::string& arg);
4052 : :
4053 : : /* Terms -------------------------------------------------------------- */
4054 : :
4055 : : /**
4056 : : * Create n-ary term of given kind.
4057 : : * @param kind The kind of the term.
4058 : : * @param children The children of the term.
4059 : : * @return The term.
4060 : : */
4061 : : Term mkTerm(Kind kind, const std::vector<Term>& children = {});
4062 : : /**
4063 : : * Create n-ary term of given kind from a given operator.
4064 : : *
4065 : : * Create operators with mkOp().
4066 : : *
4067 : : * @param op The operator.
4068 : : * @param children The children of the term.
4069 : : * @return The Term.
4070 : : */
4071 : : Term mkTerm(const Op& op, const std::vector<Term>& children = {});
4072 : :
4073 : : /* Constants, Values and Special Terms -------------------------------- */
4074 : :
4075 : : /**
4076 : : * Create a Boolean true constant.
4077 : : * @return The `true` constant.
4078 : : */
4079 : : Term mkTrue();
4080 : : /**
4081 : : * Create a Boolean false constant.
4082 : : * @return The `false` constant.
4083 : : */
4084 : : Term mkFalse();
4085 : : /**
4086 : : * Create a Boolean constant.
4087 : : * @return The Boolean constant.
4088 : : * @param val The value of the constant.
4089 : : */
4090 : : Term mkBoolean(bool val);
4091 : : /**
4092 : : * Create a constant representing the number Pi.
4093 : : * @return A constant representing Pi.
4094 : : */
4095 : : Term mkPi();
4096 : : /**
4097 : : * Create an integer constant from a string.
4098 : : * @param s The string representation of the constant, may represent an
4099 : : * integer (e.g., "123").
4100 : : * @return A constant of sort Integer assuming `s` represents an integer)
4101 : : */
4102 : : Term mkInteger(const std::string& s);
4103 : : /**
4104 : : * Create an integer constant from a c++ int.
4105 : : * @param val The value of the constant.
4106 : : * @return A constant of sort Integer.
4107 : : */
4108 : : Term mkInteger(int64_t val);
4109 : : /**
4110 : : * Create a real constant from a string.
4111 : : * @param s The string representation of the constant, may represent an
4112 : : * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
4113 : : * @return A constant of sort Real.
4114 : : */
4115 : : Term mkReal(const std::string& s);
4116 : : /**
4117 : : * Create a real constant from an integer.
4118 : : * @param val The value of the constant.
4119 : : * @return A constant of sort Integer.
4120 : : */
4121 : : Term mkReal(int64_t val);
4122 : : /**
4123 : : * Create a real constant from a rational.
4124 : : * @param num The value of the numerator.
4125 : : * @param den The value of the denominator.
4126 : : * @return A constant of sort Real.
4127 : : */
4128 : : Term mkReal(int64_t num, int64_t den);
4129 : : /**
4130 : : * Create a regular expression all (re.all) term.
4131 : : * @return The all term.
4132 : : */
4133 : : Term mkRegexpAll();
4134 : : /**
4135 : : * Create a regular expression allchar (re.allchar) term.
4136 : : * @return The allchar term.
4137 : : */
4138 : : Term mkRegexpAllchar();
4139 : : /**
4140 : : * Create a regular expression none (re.none) term.
4141 : : * @return The none term.
4142 : : */
4143 : : Term mkRegexpNone();
4144 : : /**
4145 : : * Create a constant representing an empty set of the given sort.
4146 : : * @param sort The sort of the set elements.
4147 : : * @return The empty set constant.
4148 : : */
4149 : : Term mkEmptySet(const Sort& sort);
4150 : : /**
4151 : : * Create a constant representing an empty bag of the given sort.
4152 : : * @param sort The sort of the bag elements.
4153 : : * @return The empty bag constant.
4154 : : */
4155 : : Term mkEmptyBag(const Sort& sort);
4156 : : /**
4157 : : * Create a separation logic empty term.
4158 : : * @return The separation logic empty term.
4159 : : * @warning This function is experimental and may change in future versions.
4160 : : */
4161 : : Term mkSepEmp();
4162 : : /**
4163 : : * Create a separation logic nil term.
4164 : : * @param sort The sort of the nil term.
4165 : : * @return The separation logic nil term.
4166 : : * @warning This function is experimental and may change in future versions.
4167 : : */
4168 : : Term mkSepNil(const Sort& sort);
4169 : : /**
4170 : : * Create a String constant from a `std::string` which may contain SMT-LIB
4171 : : * compatible escape sequences like `\u1234` to encode unicode characters.
4172 : : * @param s The string this constant represents.
4173 : : * @param useEscSequences Determines whether escape sequences in `s` should
4174 : : * be converted to the corresponding unicode character.
4175 : : * @return The String constant.
4176 : : */
4177 : : Term mkString(const std::string& s, bool useEscSequences = false);
4178 : : /**
4179 : : * Create a String constant from a `std::wstring`.
4180 : : *
4181 : : * This function does not support escape sequences as `std::wstring` already
4182 : : * supports unicode characters.
4183 : : *
4184 : : * @param s The string this constant represents.
4185 : : * @return The String constant.
4186 : : * @warning This function is deprecated and replaced by
4187 : : * \ref TermManager::mkString(const std::u32string& s)
4188 : : * "TermManager::mkString(const std::u32string& s)". It will be removed in a
4189 : : * future release.
4190 : : */
4191 : : [[deprecated(
4192 : : "Use TermManager::mkString(const std::u32string& s) instead")]] Term
4193 : : mkString(const std::wstring& s);
4194 : : /**
4195 : : * Create a String constant from a `std::u32string`.
4196 : : *
4197 : : * This function does not support escape sequences as `std::u32string` already
4198 : : * supports unicode characters.
4199 : : *
4200 : : * @param s The string this constant represents.
4201 : : * @return The String constant.
4202 : : */
4203 : : Term mkString(const std::u32string& s);
4204 : : /**
4205 : : * Create an empty sequence of the given element sort.
4206 : : * @param sort The element sort of the sequence.
4207 : : * @return The empty sequence with given element sort.
4208 : : */
4209 : : Term mkEmptySequence(const Sort& sort);
4210 : : /**
4211 : : * Create a universe set of the given sort.
4212 : : * @param sort The sort of the set elements.
4213 : : * @return The universe set constant.
4214 : : */
4215 : : Term mkUniverseSet(const Sort& sort);
4216 : : /**
4217 : : * Create a bit-vector constant of given size and value.
4218 : : *
4219 : : * @note The given value must fit into a bit-vector of the given size.
4220 : : *
4221 : : * @param size The bit-width of the bit-vector sort.
4222 : : * @param val The value of the constant.
4223 : : * @return The bit-vector constant.
4224 : : */
4225 : : Term mkBitVector(uint32_t size, uint64_t val = 0);
4226 : : /**
4227 : : * Create a bit-vector constant of a given bit-width from a given string of
4228 : : * base 2, 10 or 16.
4229 : : *
4230 : : * @note The given value must fit into a bit-vector of the given size.
4231 : : *
4232 : : * @param size The bit-width of the constant.
4233 : : * @param s The string representation of the constant.
4234 : : * @param base The base of the string representation (`2` for binary, `10`
4235 : : * for decimal, and `16` for hexadecimal).
4236 : : * @return The bit-vector constant.
4237 : : */
4238 : : Term mkBitVector(uint32_t size, const std::string& s, uint32_t base);
4239 : : /**
4240 : : * Create a finite field constant in a given field from a given string
4241 : : * of base n.
4242 : : *
4243 : : * If `size` is the field size, the constant needs not be in the range
4244 : : * [0,size). If it is outside this range, it will be reduced modulo size
4245 : : * before being constructed.
4246 : : *
4247 : : * @param value The string representation of the constant.
4248 : : * @param sort The field sort.
4249 : : * @param base The base of the string representation of `value`.
4250 : : *
4251 : : */
4252 : : Term mkFiniteFieldElem(const std::string& value,
4253 : : const Sort& sort,
4254 : : uint32_t base = 10);
4255 : : /**
4256 : : * Create a constant array with the provided constant value stored at every
4257 : : * index.
4258 : : * @param sort The sort of the constant array (must be an array sort).
4259 : : * @param val The constant value to store (must match the sort's element
4260 : : * sort).
4261 : : * @return The constant array term.
4262 : : */
4263 : : Term mkConstArray(const Sort& sort, const Term& val);
4264 : : /**
4265 : : * Create a positive infinity floating-point constant (SMT-LIB: `+oo`).
4266 : : * @param exp Number of bits in the exponent.
4267 : : * @param sig Number of bits in the significand.
4268 : : * @return The floating-point constant.
4269 : : */
4270 : : Term mkFloatingPointPosInf(uint32_t exp, uint32_t sig);
4271 : : /**
4272 : : * Create a negative infinity floating-point constant (SMT-LIB: `-oo`).
4273 : : * @param exp Number of bits in the exponent.
4274 : : * @param sig Number of bits in the significand.
4275 : : * @return The floating-point constant.
4276 : : */
4277 : : Term mkFloatingPointNegInf(uint32_t exp, uint32_t sig);
4278 : : /**
4279 : : * Create a not-a-number floating-point constant (SMT-LIB: `NaN`).
4280 : : * @param exp Number of bits in the exponent.
4281 : : * @param sig Number of bits in the significand.
4282 : : * @return The floating-point constant.
4283 : : */
4284 : : Term mkFloatingPointNaN(uint32_t exp, uint32_t sig);
4285 : : /**
4286 : : * Create a positive zero floating-point constant (SMT-LIB: +zero).
4287 : : * @param exp Number of bits in the exponent.
4288 : : * @param sig Number of bits in the significand.
4289 : : * @return The floating-point constant.
4290 : : */
4291 : : Term mkFloatingPointPosZero(uint32_t exp, uint32_t sig);
4292 : : /**
4293 : : * Create a negative zero floating-point constant (SMT-LIB: -zero).
4294 : : * @param exp Number of bits in the exponent.
4295 : : * @param sig Number of bits in the significand.
4296 : : * @return The floating-point constant.
4297 : : */
4298 : : Term mkFloatingPointNegZero(uint32_t exp, uint32_t sig);
4299 : : /**
4300 : : * Create a rounding mode value.
4301 : : * @param rm The floating point rounding mode this constant represents.
4302 : : * @return The rounding mode value.
4303 : : */
4304 : : Term mkRoundingMode(RoundingMode rm);
4305 : : /**
4306 : : * Create a floating-point value from a bit-vector given in IEEE-754
4307 : : * format.
4308 : : * @param exp Size of the exponent.
4309 : : * @param sig Size of the significand.
4310 : : * @param val Value of the floating-point constant as a bit-vector term.
4311 : : * @return The floating-point value.
4312 : : */
4313 : : Term mkFloatingPoint(uint32_t exp, uint32_t sig, const Term& val);
4314 : : /**
4315 : : * Create a floating-point value from its three IEEE-754 bit-vector
4316 : : * value components (sign bit, exponent, significand).
4317 : : * @param sign The sign bit.
4318 : : * @param exp The bit-vector representing the exponent.
4319 : : * @param sig The bit-vector representing the significand.
4320 : : * @return The floating-point value.
4321 : : */
4322 : : Term mkFloatingPoint(const Term& sign, const Term& exp, const Term& sig);
4323 : : /**
4324 : : * Create a cardinality constraint for an uninterpreted sort.
4325 : : *
4326 : : * @warning This function is experimental and may change in future versions.
4327 : : *
4328 : : * @param sort The sort the cardinality constraint is for.
4329 : : * @param upperBound The upper bound on the cardinality of the sort.
4330 : : * @return The cardinality constraint.
4331 : : */
4332 : : Term mkCardinalityConstraint(const Sort& sort, uint32_t upperBound);
4333 : : /**
4334 : : * Create a tuple term.
4335 : : * @param terms The elements in the tuple.
4336 : : * @return The tuple Term.
4337 : : */
4338 : : Term mkTuple(const std::vector<Term>& terms);
4339 : : /**
4340 : : * Create a nullable some term.
4341 : : * @param term The element value.
4342 : : * @return the Element value wrapped in some constructor.
4343 : : */
4344 : : Term mkNullableSome(const Term& term);
4345 : : /**
4346 : : * Create a selector for nullable term.
4347 : : * @param term A nullable term.
4348 : : * @return The element value of the nullable term.
4349 : : */
4350 : : Term mkNullableVal(const Term& term);
4351 : : /**
4352 : : * Create a null tester for a nullable term.
4353 : : * @param term A nullable term.
4354 : : * @return A tester whether term is null.
4355 : : */
4356 : : Term mkNullableIsNull(const Term& term);
4357 : : /**
4358 : : * Create a some tester for a nullable term.
4359 : : * @param term A nullable term.
4360 : : * @return A tester whether term is some.
4361 : : */
4362 : : Term mkNullableIsSome(const Term& term);
4363 : : /**
4364 : : * Create a constant representing an null of the given sort.
4365 : : * @param sort The sort of the Nullable element.
4366 : : * @return The null constant.
4367 : : */
4368 : : Term mkNullableNull(const Sort& sort);
4369 : : /**
4370 : : * Create a term that lifts kind to nullable terms.
4371 : : *
4372 : : * Example:
4373 : : * If we have the term ((_ nullable.lift +) x y),
4374 : : * where x, y of type (Nullable Int), then
4375 : : * kind would be ADD, and args would be [x, y].
4376 : : * This function would return
4377 : : * (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)
4378 : : *
4379 : : * @param kind The lifted operator.
4380 : : * @param args The arguments of the lifted operator.
4381 : : * @return A term of Kind NULLABLE_LIFT where the first child is a lambda
4382 : : * expression, and the remaining children are the original arguments.
4383 : : */
4384 : : Term mkNullableLift(Kind kind, const std::vector<Term>& args);
4385 : :
4386 : : /* Constants and Variables -------------------------------------------- */
4387 : :
4388 : : /**
4389 : : * Create a free constant.
4390 : : *
4391 : : * Note that the returned term is always fresh, even if the same arguments
4392 : : * were provided on a previous call to mkConst().
4393 : : *
4394 : : * SMT-LIB:
4395 : : *
4396 : : * \verbatim embed:rst:leading-asterisk
4397 : : * .. code:: smtlib
4398 : : *
4399 : : * (declare-const <symbol> <sort>)
4400 : : * (declare-fun <symbol> () <sort>)
4401 : : * \endverbatim
4402 : : *
4403 : : * @param sort The sort of the constant.
4404 : : * @param symbol The name of the constant (optional).
4405 : : * @return The constant.
4406 : : */
4407 : : Term mkConst(const Sort& sort,
4408 : : const std::optional<std::string>& symbol = std::nullopt);
4409 : :
4410 : : /**
4411 : : * Create a bound variable to be used in a binder (i.e., a quantifier, a
4412 : : * lambda, or a witness binder).
4413 : : *
4414 : : * @note The returned term is always fresh, even if the same arguments
4415 : : * were provided on a previous call to mkConst().
4416 : : *
4417 : : * @param sort The sort of the variable.
4418 : : * @param symbol The name of the variable (optional).
4419 : : * @return The variable.
4420 : : */
4421 : : Term mkVar(const Sort& sort,
4422 : : const std::optional<std::string>& symbol = std::nullopt);
4423 : :
4424 : : /* Datatype Constructor Declaration ----------------------------------- */
4425 : :
4426 : : /**
4427 : : * Create a datatype constructor declaration.
4428 : : * @param name The name of the datatype constructor.
4429 : : * @return The DatatypeConstructorDecl.
4430 : : */
4431 : : DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name);
4432 : :
4433 : : /* Datatype Declaration ----------------------------------------------- */
4434 : :
4435 : : /**
4436 : : * Create a datatype declaration.
4437 : : * @param name The name of the datatype.
4438 : : * @param isCoDatatype True if a codatatype is to be constructed.
4439 : : * @return The DatatypeDecl.
4440 : : */
4441 : : DatatypeDecl mkDatatypeDecl(const std::string& name,
4442 : : bool isCoDatatype = false);
4443 : :
4444 : : /**
4445 : : * Create a datatype declaration.
4446 : : *
4447 : : * Create sorts parameter with TermManager::mkParamSort().
4448 : : *
4449 : : * @param name The name of the datatype.
4450 : : * @param params A list of sort parameters.
4451 : : * @param isCoDatatype True if a codatatype is to be constructed.
4452 : : * @return The DatatypeDecl.
4453 : : * @warning This function is experimental and may change in future versions.
4454 : : */
4455 : : DatatypeDecl mkDatatypeDecl(const std::string& name,
4456 : : const std::vector<Sort>& params,
4457 : : bool isCoDatatype = false);
4458 : :
4459 : : private:
4460 : : /**
4461 : : * Get the current, thread_local term manager.
4462 : : * @warning This is a workaround to provide deprecated functionality,
4463 : : * specifically, constructor Solver::Solver(). When this constructor
4464 : : * is removed, a solver instance MUST be constructed from a given
4465 : : * TermManager instance, and this workaround will be removed.
4466 : : */
4467 : : static TermManager* currentTM();
4468 : :
4469 : : /** Reset the API statistics. */
4470 : : void resetStatistics();
4471 : : /** Increment the term stats counter. */
4472 : : void increment_term_stats(Kind kind) const;
4473 : : /** Increment the vars stats or consts stats counter. */
4474 : : void increment_vars_consts_stats(const internal::TypeNode& type,
4475 : : bool is_var) const;
4476 : :
4477 : : /** Helper to check for API misuse in mkOp functions. */
4478 : : void checkMkTerm(Kind kind, uint32_t nchildren) const;
4479 : : /**
4480 : : * Check whether string s is a valid decimal integer.
4481 : : * @param s The string representation to check.
4482 : : * @return True if `s` is a valid decimal integer.
4483 : : */
4484 : : bool isValidInteger(const std::string& s) const;
4485 : :
4486 : : /**
4487 : : * Helper for calls to mkVar from the TermManager and Solver. Ensures that
4488 : : * API statistics are collected.
4489 : : * @param type The internal type of the variable.
4490 : : * @param symbol The symbol of the variable.
4491 : : */
4492 : : internal::Node mkVarHelper(
4493 : : const internal::TypeNode& type,
4494 : : const std::optional<std::string>& symbol = std::nullopt);
4495 : : /**
4496 : : * Helper for calls to mkConst from the TermManager and Solver. Ensures that
4497 : : * API statistics are collected.
4498 : : * @param type The internal type of the const.
4499 : : * @param symbol The symbol of the const.
4500 : : * @param fresh True to return a fresh variable. If false, it returns the
4501 : : * same variable for the given type and name.
4502 : : */
4503 : : internal::Node mkConstHelper(const internal::TypeNode& type,
4504 : : const std::optional<std::string>& symbol,
4505 : : bool fresh = true);
4506 : : /**
4507 : : * Helper for mk-functions that call NodeManager::mkConst().
4508 : : * @param t The value.
4509 : : * @return The value term.
4510 : : */
4511 : : template <typename T>
4512 : : Term mkValHelper(const T& t);
4513 : : /** Helper for creating operators. */
4514 : : template <typename T>
4515 : : Op mkOpHelper(Kind kind, const T& t);
4516 : : /**
4517 : : * Helper for creating rational values.
4518 : : * @param r The value (either int or real).
4519 : : * @param isInt True to create an integer value.
4520 : : * @return The rational value term.
4521 : : */
4522 : : Term mkRationalValHelper(const internal::Rational& r, bool isInt);
4523 : : /**
4524 : : * Helper for mkReal functions that take a string as argument.
4525 : : * @param s The string representation of the real/int value.
4526 : : * @param isInt True if `s` represents an integer.
4527 : : * @return The value term.
4528 : : */
4529 : : Term mkRealOrIntegerFromStrHelper(const std::string& s, bool isInt = true);
4530 : : /**
4531 : : * Helper for mkBitVector functions that take a string as argument.
4532 : : * @param s The string representation of the bit-vector value.
4533 : : * @param base The numerical base of the string representation.
4534 : : * @return The bit-vector value term.
4535 : : */
4536 : : Term mkBVFromStrHelper(const std::string& s, uint32_t base);
4537 : : /**
4538 : : * Helper for mkBitVector functions that take a string and a size as
4539 : : * arguments.
4540 : : * @param size The bit-vector size.
4541 : : * @param s The string representation of the bit-vector value.
4542 : : * @param base The numerical base of the string representation.
4543 : : * @return The bit-vector value term.
4544 : : */
4545 : : Term mkBVFromStrHelper(uint32_t size, const std::string& s, uint32_t base);
4546 : : /**
4547 : : * Helper for mkBitVector functions that take an unsigned integer as argument.
4548 : : * @param size The bit-vector size.
4549 : : * @param val The bit-vector value as uint64_t.
4550 : : * @return The bit-vector value term.
4551 : : */
4552 : : Term mkBVFromIntHelper(uint32_t size, uint64_t val);
4553 : : /**
4554 : : * Helper for functions that create tuple sorts.
4555 : : * @param sorts The sorts.
4556 : : * @return The tuple sort.
4557 : : */
4558 : : Sort mkTupleSortHelper(const std::vector<Sort>& sorts);
4559 : : /**
4560 : : * Helper for mkTerm functions that create Term from a Kind.
4561 : : * @param kind The kind.
4562 : : * @return The term.
4563 : : */
4564 : : Term mkTermFromKind(Kind kind);
4565 : : /**
4566 : : * Helper for mkChar functions that take a string as argument.
4567 : : * @param s The string.
4568 : : * @return The character term.
4569 : : */
4570 : : Term mkCharFromStrHelper(const std::string& s);
4571 : : /**
4572 : : * Create n-ary term of given kind. This handles the cases of left/right
4573 : : * associative operators, chainable operators, and cases when the number of
4574 : : * children exceeds the maximum arity for the kind.
4575 : : * @param kind The kind of the term.
4576 : : * @param children The children of the term.
4577 : : * @return The Term.
4578 : : */
4579 : : Term mkTermHelper(Kind kind, const std::vector<Term>& children);
4580 : : /**
4581 : : * Create n-ary term of given kind from a given operator.
4582 : : * @param op The operator.
4583 : : * @param children The children of the term.
4584 : : * @return The Term.
4585 : : */
4586 : : Term mkTermHelper(const Op& op, const std::vector<Term>& children);
4587 : :
4588 : : /** The associated node manager. */
4589 : : std::unique_ptr<internal::NodeManager> d_nm;
4590 : : /** The statistics collected on the Api level. */
4591 : : std::unique_ptr<APIStatistics> d_stats;
4592 : : /** The statistics registry (independent from any Solver's registry). */
4593 : : std::unique_ptr<internal::StatisticsRegistry> d_statsReg;
4594 : : };
4595 : :
4596 : : /* -------------------------------------------------------------------------- */
4597 : : /* Solver */
4598 : : /* -------------------------------------------------------------------------- */
4599 : :
4600 : : /**
4601 : : * A cvc5 solver.
4602 : : */
4603 : : class CVC5_EXPORT Solver
4604 : : {
4605 : : friend class Datatype;
4606 : : friend class DatatypeDecl;
4607 : : friend class DatatypeConstructor;
4608 : : friend class DatatypeConstructorDecl;
4609 : : friend class DatatypeSelector;
4610 : : friend class DriverOptions;
4611 : : friend class Grammar;
4612 : : friend class Plugin;
4613 : : friend class Op;
4614 : : friend class parser::Cmd;
4615 : : friend class Proof;
4616 : : friend class main::CommandExecutor;
4617 : : friend class Sort;
4618 : : friend class Term;
4619 : :
4620 : : public:
4621 : : /* .................................................................... */
4622 : : /* Constructors/Destructors */
4623 : : /* .................................................................... */
4624 : :
4625 : : /**
4626 : : * Constructor.
4627 : : * @warning This constructor is deprecated and replaced by
4628 : : * `Solver::Solver(TermManager&)`. It will be removed in a future
4629 : : * release.
4630 : : */
4631 : : [[deprecated("Use Solver::Solver(TermManager&) instead")]] Solver();
4632 : : /**
4633 : : * Constructor.
4634 : : *
4635 : : * Constructs solver instance from a given term manager instance.
4636 : : * @param tm The associated term manager.
4637 : : */
4638 : : Solver(TermManager& tm);
4639 : :
4640 : : /**
4641 : : * Destructor.
4642 : : */
4643 : : ~Solver();
4644 : :
4645 : : /**
4646 : : * Disallow copy/assignment.
4647 : : */
4648 : : Solver(const Solver&) = delete;
4649 : : Solver& operator=(const Solver&) = delete;
4650 : :
4651 : : /* .................................................................... */
4652 : : /* Sorts Handling */
4653 : : /* .................................................................... */
4654 : :
4655 : : /**
4656 : : * Get the Boolean sort.
4657 : : * @return Sort Boolean.
4658 : : * @warning This function is deprecated and replaced by
4659 : : * `TermManager::getBooleanSort()`. It will be removed in a future
4660 : : * release.
4661 : : */
4662 : : [[deprecated("Use TermManager::getBooleanSort() instead")]] Sort
4663 : : getBooleanSort() const;
4664 : :
4665 : : /**
4666 : : * Get the Integer sort.
4667 : : * @return Sort Integer.
4668 : : * @warning This function is deprecated and replaced by
4669 : : * `TermManager::getIntegerSort()`. It will be removed in a future
4670 : : * release.
4671 : : */
4672 : : [[deprecated("Use TermManager::getInteger() instead")]] Sort getIntegerSort()
4673 : : const;
4674 : :
4675 : : /**
4676 : : * Get the Real sort.
4677 : : * @return Sort Real.
4678 : : * @warning This function is deprecated and replaced by
4679 : : * `TermManager::getRealSort()`. It will be removed in a future
4680 : : * release.
4681 : : */
4682 : : [[deprecated("Use TermManager::getRealSort() instead")]] Sort getRealSort()
4683 : : const;
4684 : :
4685 : : /**
4686 : : * Get the regular expression sort.
4687 : : * @return Sort RegExp.
4688 : : * @warning This function is deprecated and replaced by
4689 : : * `TermManager::getRegExpSort()`. It will be removed in a future
4690 : : * release.
4691 : : */
4692 : : [[deprecated("Use TermManager::getRegExpSort() instead")]] Sort
4693 : : getRegExpSort() const;
4694 : :
4695 : : /**
4696 : : * Get the rounding mode sort.
4697 : : * @return Sort RoundingMode.
4698 : : * @warning This function is deprecated and replaced by
4699 : : * `TermManager::getRoundingModeSort()`. It will be removed in a
4700 : : * future release.
4701 : : */
4702 : : [[deprecated("Use TermManager::getRoundingModeSort() instead")]] Sort
4703 : : getRoundingModeSort() const;
4704 : :
4705 : : /**
4706 : : * Get the string sort.
4707 : : * @return Sort String.
4708 : : * @warning This function is deprecated and replaced by
4709 : : * `TermManager::getStringSort()`. It will be removed in a future
4710 : : * release.
4711 : : */
4712 : : [[deprecated("Use TermManager::getStringSort() instead")]] Sort
4713 : : getStringSort() const;
4714 : :
4715 : : /**
4716 : : * Create an array sort.
4717 : : * @param indexSort The array index sort.
4718 : : * @param elemSort The array element sort.
4719 : : * @return The array sort.
4720 : : * @warning This function is deprecated and replaced by
4721 : : * `TermManager::mkArraySort()`. It will be removed in a future
4722 : : * release.
4723 : : */
4724 : : [[deprecated("Use TermManager::mkArraySort() instead")]] Sort mkArraySort(
4725 : : const Sort& indexSort, const Sort& elemSort) const;
4726 : :
4727 : : /**
4728 : : * Create a bit-vector sort.
4729 : : * @param size The bit-width of the bit-vector sort.
4730 : : * @return The bit-vector sort.
4731 : : * @warning This function is deprecated and replaced by
4732 : : * `TermManager::mkBitVectorSort()`. It will be removed in a future
4733 : : * release.
4734 : : */
4735 : : [[deprecated("Use TermManager::mkBitVectorSort() instead")]] Sort
4736 : : mkBitVectorSort(uint32_t size) const;
4737 : :
4738 : : /**
4739 : : * Create a floating-point sort.
4740 : : * @param exp The bit-width of the exponent of the floating-point sort.
4741 : : * @param sig The bit-width of the significand of the floating-point sort.
4742 : : * @warning This function is deprecated and replaced by
4743 : : * `TermManager::mkFloatingPointSort()`. It will be removed in a
4744 : : * future release.
4745 : : */
4746 : : [[deprecated("Use TermManager::mkFloatingPointSort() instead")]] Sort
4747 : : mkFloatingPointSort(uint32_t exp, uint32_t sig) const;
4748 : :
4749 : : /**
4750 : : * Create a finite-field sort from a given string of
4751 : : * base n.
4752 : : *
4753 : : * @param size The modulus of the field. Must be prime.
4754 : : * @param base The base of the string representation of `size`.
4755 : : * @return The finite-field sort.
4756 : : * @warning This function is deprecated and replaced by
4757 : : * `TermManager::mkFiniteFieldSort()`. It will be removed in a future
4758 : : * release.
4759 : : */
4760 : : [[deprecated("Use TermManager::mkFiniteFieldSort() instead")]] Sort
4761 : : mkFiniteFieldSort(const std::string& size, uint32_t base = 10) const;
4762 : :
4763 : : /**
4764 : : * Create a datatype sort.
4765 : : * @param dtypedecl The datatype declaration from which the sort is created.
4766 : : * @return The datatype sort.
4767 : : * @warning This function is deprecated and replaced by
4768 : : * `TermManager::mkDatatypeSort()`. It will be removed in a future
4769 : : * release.
4770 : : */
4771 : : [[deprecated("Use TermManager::mkDatatypeSort() instead")]] Sort
4772 : : mkDatatypeSort(const DatatypeDecl& dtypedecl) const;
4773 : :
4774 : : /**
4775 : : * Create a vector of datatype sorts.
4776 : : * @note The names of the datatype declarations must be distinct.
4777 : : * @param dtypedecls The datatype declarations from which the sort is created.
4778 : : * @return The datatype sorts.
4779 : : * @warning This function is deprecated and replaced by
4780 : : * `TermManager::mkDatatypeSorts()`. It will be removed in a future
4781 : : * release.
4782 : : */
4783 : : [[deprecated("Use TermManager::mkDatatypeSorts() instead")]] std::vector<Sort>
4784 : : mkDatatypeSorts(const std::vector<DatatypeDecl>& dtypedecls) const;
4785 : :
4786 : : /**
4787 : : * Create function sort.
4788 : : * @param sorts The sort of the function arguments.
4789 : : * @param codomain The sort of the function return value.
4790 : : * @return The function sort.
4791 : : * @warning This function is deprecated and replaced by
4792 : : * `TermManager::mkFunctionSort()`. It will be removed in a future
4793 : : * release.
4794 : : */
4795 : : [[deprecated("Use TermManager::mkFunctionSort() instead")]] Sort
4796 : : mkFunctionSort(const std::vector<Sort>& sorts, const Sort& codomain) const;
4797 : :
4798 : : /**
4799 : : * Create a sort parameter.
4800 : : *
4801 : : * @warning This function is experimental and may change in future versions.
4802 : : *
4803 : : * @param symbol The name of the sort.
4804 : : * @return The sort parameter.
4805 : : * @warning This function is deprecated and replaced by
4806 : : * `TermManager::mkParamSort()`. It will be removed in a future
4807 : : * release.
4808 : : */
4809 : : [[deprecated("Use TermManager::mkParamSort() instead")]] Sort mkParamSort(
4810 : : const std::optional<std::string>& symbol = std::nullopt) const;
4811 : :
4812 : : /**
4813 : : * Create a predicate sort.
4814 : : *
4815 : : * This is equivalent to calling mkFunctionSort() with the Boolean sort as the
4816 : : * codomain.
4817 : : * @param sorts The list of sorts of the predicate.
4818 : : * @return The predicate sort.
4819 : : * @warning This function is deprecated and replaced by
4820 : : * `TermManager::mkPredicateSort()`. It will be removed in a future
4821 : : * release.
4822 : : */
4823 : : [[deprecated("Use TermManager::mkParamSort() instead")]] Sort mkPredicateSort(
4824 : : const std::vector<Sort>& sorts) const;
4825 : :
4826 : : /**
4827 : : * Create a record sort
4828 : : *
4829 : : * @warning This function is experimental and may change in future versions.
4830 : : *
4831 : : * @param fields The list of fields of the record.
4832 : : * @return The record sort.
4833 : : * @warning This function is deprecated and replaced by
4834 : : * `TermManager::mkRecordSort()`. It will be removed in a future
4835 : : * release.
4836 : : */
4837 : : [[deprecated("Use TermManager::mkRecordSort() instead")]] Sort mkRecordSort(
4838 : : const std::vector<std::pair<std::string, Sort>>& fields) const;
4839 : :
4840 : : /**
4841 : : * Create a set sort.
4842 : : * @param elemSort The sort of the set elements.
4843 : : * @return The set sort.
4844 : : * @warning This function is deprecated and replaced by
4845 : : * `TermManager::mkSetSort()`. It will be removed in a future
4846 : : * release.
4847 : : */
4848 : : [[deprecated("Use TermManager::mkSetSort() instead")]] Sort mkSetSort(
4849 : : const Sort& elemSort) const;
4850 : :
4851 : : /**
4852 : : * Create a bag sort.
4853 : : * @param elemSort The sort of the bag elements.
4854 : : * @return The bag sort.
4855 : : * @warning This function is deprecated and replaced by
4856 : : * `TermManager::mkBagSort()`. It will be removed in a future
4857 : : * release.
4858 : : */
4859 : : [[deprecated("Use TermManager::mkBagSort() instead")]] Sort mkBagSort(
4860 : : const Sort& elemSort) const;
4861 : :
4862 : : /**
4863 : : * Create a sequence sort.
4864 : : * @param elemSort The sort of the sequence elements.
4865 : : * @return The sequence sort.
4866 : : * @warning This function is deprecated and replaced by
4867 : : * `TermManager::mkSequenceSort()`. It will be removed in a future
4868 : : * release.
4869 : : */
4870 : : [[deprecated("Use TermManager::mkSequenceSort() instead")]] Sort
4871 : : mkSequenceSort(const Sort& elemSort) const;
4872 : :
4873 : : /**
4874 : : * Create an abstract sort. An abstract sort represents a sort for a given
4875 : : * kind whose parameters and arguments are unspecified.
4876 : : *
4877 : : * The kind `k` must be the kind of a sort that can be abstracted, i.e., a
4878 : : * sort that has indices or argument sorts. For example, #ARRAY_SORT and
4879 : : * #BITVECTOR_SORT can be passed as the kind `k` to this function, while
4880 : : * #INTEGER_SORT and #STRING_SORT cannot.
4881 : : *
4882 : : * @note Providing the kind #ABSTRACT_SORT as an argument to this function
4883 : : * returns the (fully) unspecified sort, denoted `?`.
4884 : : *
4885 : : * @note Providing a kind `k` that has no indices and a fixed arity
4886 : : * of argument sorts will return the sort of kind `k` whose arguments are the
4887 : : * unspecified sort. For example, `mkAbstractSort(SortKind::ARRAY_SORT)` will
4888 : : * return the sort `(ARRAY_SORT ? ?)` instead of the abstract sort whose
4889 : : * abstract kind is #ARRAY_SORT.
4890 : : *
4891 : : * @param k The kind of the abstract sort
4892 : : * @return The abstract sort.
4893 : : *
4894 : : * @warning This function is experimental and may change in future versions.
4895 : : * @warning This function is deprecated and replaced by
4896 : : * `TermManager::mkAbstractSort()`. It will be removed in a future
4897 : : * release.
4898 : : */
4899 : : [[deprecated("Use TermManager::mkAbstractSort() instead")]] Sort
4900 : : mkAbstractSort(SortKind k) const;
4901 : :
4902 : : /**
4903 : : * Create an uninterpreted sort.
4904 : : * @param symbol The name of the sort.
4905 : : * @return The uninterpreted sort.
4906 : : * @warning This function is deprecated and replaced by
4907 : : * `TermManager::mkUninterpretedSort()`. It will be removed in a
4908 : : * future release.
4909 : : */
4910 : : [[deprecated("Use TermManager::mkUninterpretedSort() instead")]] Sort
4911 : : mkUninterpretedSort(
4912 : : const std::optional<std::string>& symbol = std::nullopt) const;
4913 : :
4914 : : /**
4915 : : * Create an unresolved datatype sort.
4916 : : *
4917 : : * This is for creating yet unresolved sort placeholders for mutually
4918 : : * recursive parametric datatypes.
4919 : : *
4920 : : * @param symbol The symbol of the sort.
4921 : : * @param arity The number of sort parameters of the sort.
4922 : : * @return The unresolved sort.
4923 : : *
4924 : : * @warning This function is experimental and may change in future versions.
4925 : : * @warning This function is deprecated and replaced by
4926 : : * `TermManager::mkUnresolvedDatatypeSort()`. It will be removed in
4927 : : * a future release.
4928 : : */
4929 : : [[deprecated("Use TermManager::mkUnresolvedDatatypeSort() instead")]] Sort
4930 : : mkUnresolvedDatatypeSort(const std::string& symbol, size_t arity = 0) const;
4931 : :
4932 : : /**
4933 : : * Create an uninterpreted sort constructor sort.
4934 : : *
4935 : : * An uninterpreted sort constructor is an uninterpreted sort with arity > 0.
4936 : : *
4937 : : * @param symbol The symbol of the sort.
4938 : : * @param arity The arity of the sort (must be > 0)
4939 : : * @return The uninterpreted sort constructor sort.
4940 : : * @warning This function is deprecated and replaced by
4941 : : * `TermManager::mkUninterpretedSortConstructorerSort()`. It will be
4942 : : * removed in a future release.
4943 : : */
4944 : : [[deprecated(
4945 : : "Use TermManager::mkUninterpretedConstructorSort() instead")]] Sort
4946 : : mkUninterpretedSortConstructorSort(
4947 : : size_t arity,
4948 : : const std::optional<std::string>& symbol = std::nullopt) const;
4949 : :
4950 : : /**
4951 : : * Create a tuple sort.
4952 : : * @param sorts The sorts of the elements of the tuple.
4953 : : * @return The tuple sort.
4954 : : * @warning This function is deprecated and replaced by
4955 : : * `TermManager::mkTupleSort()`. It will be removed in a future
4956 : : * release.
4957 : : */
4958 : : [[deprecated("Use TermManager::mkTupleSort() instead")]] Sort mkTupleSort(
4959 : : const std::vector<Sort>& sorts) const;
4960 : :
4961 : : /**
4962 : : * Create a nullable sort.
4963 : : * @param sort The sort of the element of the nullable.
4964 : : * @return The nullable sort.
4965 : : * @warning This function is deprecated and replaced by
4966 : : * `TermManager::mkNullableSort()`. It will be removed in a future
4967 : : * release.
4968 : : */
4969 : : [[deprecated("Use TermManager::mkNullableSort() instead")]] Sort
4970 : : mkNullableSort(const Sort& sort) const;
4971 : :
4972 : : /* .................................................................... */
4973 : : /* Create Terms */
4974 : : /* .................................................................... */
4975 : :
4976 : : /**
4977 : : * Create n-ary term of given kind.
4978 : : * @param kind The kind of the term.
4979 : : * @param children The children of the term.
4980 : : * @return The Term
4981 : : * @warning This function is deprecated and replaced by
4982 : : * `TermManager::mkTerm()`. It will be removed in a future release.
4983 : : */
4984 : : [[deprecated("Use TermManager::mkTerm() instead")]] Term mkTerm(
4985 : : Kind kind, const std::vector<Term>& children = {}) const;
4986 : :
4987 : : /**
4988 : : * Create n-ary term of given kind from a given operator.
4989 : : * Create operators with mkOp().
4990 : : * @param op The operator.
4991 : : * @param children The children of the term.
4992 : : * @return The Term.
4993 : : * @warning This function is deprecated and replaced by
4994 : : * `TermManager::mkTerm()`. It will be removed in a future release.
4995 : : */
4996 : : [[deprecated("Use TermManager::mkTerm() instead")]] Term mkTerm(
4997 : : const Op& op, const std::vector<Term>& children = {}) const;
4998 : :
4999 : : /**
5000 : : * Create a tuple term.
5001 : : * @param terms The elements in the tuple.
5002 : : * @return The tuple Term.
5003 : : * @warning This function is deprecated and replaced by
5004 : : * `TermManager::mkTuple()`. It will be removed in a future release.
5005 : : */
5006 : : [[deprecated("Use TermManager::mkTuple() instead")]] Term mkTuple(
5007 : : const std::vector<Term>& terms) const;
5008 : : /**
5009 : : * Create a nullable some term.
5010 : : * @param term The element value.
5011 : : * @return the Element value wrapped in some constructor.
5012 : : * @warning This function is deprecated and replaced by
5013 : : * `TermManager::mkNullableSome()`. It will be removed in a future
5014 : : * release.
5015 : : */
5016 : : [[deprecated("Use TermManager::mkNullableSome() instead")]] Term
5017 : : mkNullableSome(const Term& term) const;
5018 : : /**
5019 : : * Create a selector for nullable term.
5020 : : * @param term A nullable term.
5021 : : * @return The element value of the nullable term.
5022 : : * @warning This function is deprecated and replaced by
5023 : : * `TermManager::mkNullableVal()`. It will be removed in a future
5024 : : * release.
5025 : : */
5026 : : [[deprecated("Use TermManager::mkNullableVal() instead")]] Term mkNullableVal(
5027 : : const Term& term) const;
5028 : : /**
5029 : : * Create a null tester for a nullable term.
5030 : : * @param term A nullable term.
5031 : : * @return A tester whether term is null.
5032 : : * @warning This function is deprecated and replaced by
5033 : : * `TermManager::mkNullableisNull()`. It will be removed in a future
5034 : : * release.
5035 : : */
5036 : : [[deprecated("Use TermManager::mkNullableisNull() instead")]] Term
5037 : : mkNullableIsNull(const Term& term) const;
5038 : : /**
5039 : : * Create a some tester for a nullable term.
5040 : : * @param term A nullable term.
5041 : : * @return A tester whether term is some.
5042 : : * @warning This function is deprecated and replaced by
5043 : : * `TermManager::mkNullableisSome()`. It will be removed in a future
5044 : : * release.
5045 : : */
5046 : : [[deprecated("Use TermManager::mkNullableisSome() instead")]] Term
5047 : : mkNullableIsSome(const Term& term) const;
5048 : :
5049 : : /**
5050 : : * Create a constant representing an null of the given sort.
5051 : : * @param sort The sort of the Nullable element.
5052 : : * @return The null constant.
5053 : : * @warning This function is deprecated and replaced by
5054 : : * `TermManager::mkNullableNull()`. It will be removed in a future
5055 : : * release.
5056 : : */
5057 : : [[deprecated("Use TermManager::mkNullableNull() instead")]] Term
5058 : : mkNullableNull(const Sort& sort) const;
5059 : : /**
5060 : : * Create a term that lifts kind to nullable terms.
5061 : : * Example:
5062 : : * If we have the term ((_ nullable.lift +) x y),
5063 : : * where x, y of type (Nullable Int), then
5064 : : * kind would be ADD, and args would be [x, y].
5065 : : * This function would return
5066 : : * (nullable.lift (lambda ((a Int) (b Int)) (+ a b)) x y)
5067 : : * @param kind The lifted operator.
5068 : : * @param args The arguments of the lifted operator.
5069 : : * @return A term of Kind NULLABLE_LIFT where the first child
5070 : : * is a lambda expression, and the remaining children are
5071 : : * the original arguments.
5072 : : * @warning This function is deprecated and replaced by
5073 : : * `TermManager::mkNullableLift()`. It will be removed in a future
5074 : : * release.
5075 : : */
5076 : : [[deprecated("Use TermManager::mkNullableLift() instead")]] Term
5077 : : mkNullableLift(Kind kind, const std::vector<Term>& args) const;
5078 : :
5079 : : /* .................................................................... */
5080 : : /* Create Operators */
5081 : : /* .................................................................... */
5082 : :
5083 : : /**
5084 : : * Create operator of Kind:
5085 : : * - #BITVECTOR_EXTRACT
5086 : : * - #BITVECTOR_REPEAT
5087 : : * - #BITVECTOR_ROTATE_LEFT
5088 : : * - #BITVECTOR_ROTATE_RIGHT
5089 : : * - #BITVECTOR_SIGN_EXTEND
5090 : : * - #BITVECTOR_ZERO_EXTEND
5091 : : * - #DIVISIBLE
5092 : : * - #FLOATINGPOINT_TO_FP_FROM_FP
5093 : : * - #FLOATINGPOINT_TO_FP_FROM_IEEE_BV
5094 : : * - #FLOATINGPOINT_TO_FP_FROM_REAL
5095 : : * - #FLOATINGPOINT_TO_FP_FROM_SBV
5096 : : * - #FLOATINGPOINT_TO_FP_FROM_UBV
5097 : : * - #FLOATINGPOINT_TO_SBV
5098 : : * - #FLOATINGPOINT_TO_UBV
5099 : : * - #INT_TO_BITVECTOR
5100 : : * - #TUPLE_PROJECT
5101 : : *
5102 : : * See cvc5::Kind for a description of the parameters.
5103 : : * @param kind The kind of the operator.
5104 : : * @param args The arguments (indices) of the operator.
5105 : : *
5106 : : * @note If ``args`` is empty, the Op simply wraps the cvc5::Kind. The
5107 : : * Kind can be used in TermManager::mkTerm directly without creating an Op
5108 : : * first.
5109 : : * @warning This function is deprecated and replaced by `TermManager::mkOp()`.
5110 : : * It will be removed in a future release.
5111 : : */
5112 : : [[deprecated("Use TermManager::mkOp() instead")]] Op mkOp(
5113 : : Kind kind, const std::vector<uint32_t>& args = {}) const;
5114 : :
5115 : : #ifndef DOXYGEN_SKIP
5116 : : // Overload is only used to disambiguate the std::vector and std::string
5117 : : // overloads.
5118 : : [[deprecated("Use TermManager::mkOp() instead")]] Op mkOp(
5119 : : Kind kind, const std::initializer_list<uint32_t>& args) const;
5120 : : #endif
5121 : :
5122 : : /**
5123 : : * Create operator of kind:
5124 : : * - #DIVISIBLE (to support arbitrary precision integers)
5125 : : * See cvc5::Kind for a description of the parameters.
5126 : : * @param kind The kind of the operator.
5127 : : * @param arg The string argument to this operator.
5128 : : * @warning This function is deprecated and replaced by `TermManager::mkOp()`.
5129 : : * It will be removed in a future release.
5130 : : */
5131 : : [[deprecated("Use TermManager::mkOp() instead")]] Op mkOp(
5132 : : Kind kind, const std::string& arg) const;
5133 : :
5134 : : /* .................................................................... */
5135 : : /* Create Constants */
5136 : : /* .................................................................... */
5137 : :
5138 : : /**
5139 : : * Create a Boolean true constant.
5140 : : * @return The true constant.
5141 : : * @warning This function is deprecated and replaced by
5142 : : * `TermManager::mkTrue()`. It will be removed in a future release.
5143 : : */
5144 : : [[deprecated("Use TermManager::mkTrue() instead")]] Term mkTrue() const;
5145 : :
5146 : : /**
5147 : : * Create a Boolean false constant.
5148 : : * @return The false constant.
5149 : : * @warning This function is deprecated and replaced by
5150 : : * `TermManager::mkFalse()`. It will be removed in a future release.
5151 : : */
5152 : : [[deprecated("Use TermManager::mkFalse() instead")]] Term mkFalse() const;
5153 : :
5154 : : /**
5155 : : * Create a Boolean constant.
5156 : : * @return The Boolean constant.
5157 : : * @param val The value of the constant.
5158 : : * @warning This function is deprecated and replaced by
5159 : : * `TermManager::mkBoolean()`. It will be removed in a future
5160 : : * release.
5161 : : */
5162 : : [[deprecated("Use TermManager::mkBoolean() instead")]] Term mkBoolean(
5163 : : bool val) const;
5164 : :
5165 : : /**
5166 : : * Create a constant representing the number Pi.
5167 : : * @return A constant representing Pi.
5168 : : * @warning This function is deprecated and replaced by
5169 : : * `TermManager::mkPi()`. It will be removed in a future release.
5170 : : * @warning This function is deprecated and replaced by
5171 : : * `TermManager::mkPi()`. It will be removed in a future release.
5172 : : */
5173 : : [[deprecated("Use TermManager::mkPi() instead")]] Term mkPi() const;
5174 : : /**
5175 : : * Create an integer constant from a string.
5176 : : * @param s The string representation of the constant, may represent an
5177 : : * integer (e.g., "123").
5178 : : * @return A constant of sort Integer assuming `s` represents an integer)
5179 : : * @warning This function is deprecated and replaced by
5180 : : * `TermManager::mkInteger()`. It will be removed in a future
5181 : : * release.
5182 : : */
5183 : : [[deprecated("Use TermManager::mkInteger() instead")]] Term mkInteger(
5184 : : const std::string& s) const;
5185 : :
5186 : : /**
5187 : : * Create an integer constant from a c++ int.
5188 : : * @param val The value of the constant.
5189 : : * @return A constant of sort Integer.
5190 : : * @warning This function is deprecated and replaced by
5191 : : * `TermManager::mkInteger()`. It will be removed in a future
5192 : : * release.
5193 : : */
5194 : : [[deprecated("Use TermManager::mkInteger() instead")]] Term mkInteger(
5195 : : int64_t val) const;
5196 : :
5197 : : /**
5198 : : * Create a real constant from a string.
5199 : : * @param s The string representation of the constant, may represent an
5200 : : * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
5201 : : * @return A constant of sort Real.
5202 : : * @warning This function is deprecated and replaced by
5203 : : * `TermManager::mkReal()`. It will be removed in a future
5204 : : * release.
5205 : : */
5206 : : [[deprecated("Use TermManager::mkReal() instead")]] Term mkReal(
5207 : : const std::string& s) const;
5208 : :
5209 : : /**
5210 : : * Create a real constant from an integer.
5211 : : * @param val The value of the constant.
5212 : : * @return A constant of sort Real.
5213 : : * @warning This function is deprecated and replaced by
5214 : : * `TermManager::mkReal()`. It will be removed in a future
5215 : : * release.
5216 : : */
5217 : : [[deprecated("Use TermManager::mkReal() instead")]] Term mkReal(
5218 : : int64_t val) const;
5219 : :
5220 : : /**
5221 : : * Create a real constant from a rational.
5222 : : * @param num The value of the numerator.
5223 : : * @param den The value of the denominator.
5224 : : * @return A constant of sort Real.
5225 : : * @warning This function is deprecated and replaced by
5226 : : * `TermManager::mkReal()`. It will be removed in a future
5227 : : * release.
5228 : : */
5229 : : [[deprecated("Use TermManager::mkReal() instead")]] Term mkReal(
5230 : : int64_t num, int64_t den) const;
5231 : :
5232 : : /**
5233 : : * Create a regular expression all (re.all) term.
5234 : : * @return The all term.
5235 : : * @warning This function is deprecated and replaced by
5236 : : * `TermManager::mkRegExpAll()`. It will be removed in a future
5237 : : * release.
5238 : : */
5239 : : [[deprecated("Use TermManager::mkRegExpAll() instead")]] Term mkRegexpAll()
5240 : : const;
5241 : :
5242 : : /**
5243 : : * Create a regular expression allchar (re.allchar) term.
5244 : : * @return The allchar term.
5245 : : * @warning This function is deprecated and replaced by
5246 : : * `TermManager::mkRegExpAllChar()`. It will be removed in a future
5247 : : * release.
5248 : : */
5249 : : [[deprecated("Use TermManager::mkRegExpAllChar() instead")]] Term
5250 : : mkRegexpAllchar() const;
5251 : :
5252 : : /**
5253 : : * Create a regular expression none (re.none) term.
5254 : : * @return The none term.
5255 : : * @warning This function is deprecated and replaced by
5256 : : * `TermManager::mkRegExpNone()`. It will be removed in a future
5257 : : * release.
5258 : : */
5259 : : [[deprecated("Use TermManager::mkRegExpNone() instead")]] Term mkRegexpNone()
5260 : : const;
5261 : :
5262 : : /**
5263 : : * Create a constant representing an empty set of the given sort.
5264 : : * @param sort The sort of the set elements.
5265 : : * @return The empty set constant.
5266 : : * @warning This function is deprecated and replaced by
5267 : : * `TermManager::mkEmptySet()`. It will be removed in a future
5268 : : * release.
5269 : : */
5270 : : [[deprecated("Use TermManager::mkEmptySet() instead")]] Term mkEmptySet(
5271 : : const Sort& sort) const;
5272 : :
5273 : : /**
5274 : : * Create a constant representing an empty bag of the given sort.
5275 : : * @param sort The sort of the bag elements.
5276 : : * @return The empty bag constant.
5277 : : * @warning This function is deprecated and replaced by
5278 : : * `TermManager::mkEmptyBag()`. It will be removed in a future
5279 : : * release.
5280 : : */
5281 : : [[deprecated("Use TermManager::mkEmptyBag() instead")]] Term mkEmptyBag(
5282 : : const Sort& sort) const;
5283 : :
5284 : : /**
5285 : : * Create a separation logic empty term.
5286 : : * @return The separation logic empty term.
5287 : : * @warning This function is experimental and may change in future versions.
5288 : : * @warning This function is deprecated and replaced by
5289 : : * `TermManager::mkSepEmp()`. It will be removed in a future release.
5290 : : */
5291 : : [[deprecated("Use TermManager::mkSepEmp() instead")]] Term mkSepEmp() const;
5292 : :
5293 : : /**
5294 : : * Create a separation logic nil term.
5295 : : * @param sort The sort of the nil term.
5296 : : * @return The separation logic nil term.
5297 : : * @warning This function is experimental and may change in future versions.
5298 : : * @warning This function is deprecated and replaced by
5299 : : * `TermManager::mkSepNil()`. It will be removed in a future release.
5300 : : */
5301 : : [[deprecated("Use TermManager::mkSepNil() instead")]] Term mkSepNil(
5302 : : const Sort& sort) const;
5303 : :
5304 : : /**
5305 : : * Create a String constant from a `std::string` which may contain SMT-LIB
5306 : : * compatible escape sequences like `\u1234` to encode unicode characters.
5307 : : * @param s The string this constant represents.
5308 : : * @param useEscSequences Determines whether escape sequences in `s` should.
5309 : : * be converted to the corresponding unicode character
5310 : : * @return The String constant.
5311 : : * @warning This function is deprecated and replaced by
5312 : : * `TermManager::mkString()`. It will be removed in a future release.
5313 : : */
5314 : : [[deprecated("Use TermManager::mkString() instead")]] Term mkString(
5315 : : const std::string& s, bool useEscSequences = false) const;
5316 : :
5317 : : /**
5318 : : * Create a String constant from a `std::wstring`.
5319 : : * This function does not support escape sequences as `std::wstring` already
5320 : : * supports unicode characters.
5321 : : * @param s The string this constant represents.
5322 : : * @return The String constant.
5323 : : * @warning This function is deprecated and replaced by
5324 : : * `TermManager::mkString(const std::u32string& s)`. It will be
5325 : : * removed in a future release.
5326 : : */
5327 : : [[deprecated(
5328 : : "Use TermManager::mkString(const std::u32string& s) instead")]] Term
5329 : : mkString(const std::wstring& s) const;
5330 : :
5331 : : /**
5332 : : * Create an empty sequence of the given element sort.
5333 : : * @param sort The element sort of the sequence.
5334 : : * @return The empty sequence with given element sort.
5335 : : * @warning This function is deprecated and replaced by
5336 : : * `TermManager::mkEmptySequence()`. It will be removed in a future
5337 : : * release.
5338 : : */
5339 : : [[deprecated("Use TermManager::mkEmptySequence() instead")]] Term
5340 : : mkEmptySequence(const Sort& sort) const;
5341 : :
5342 : : /**
5343 : : * Create a universe set of the given sort.
5344 : : * @param sort The sort of the set elements.
5345 : : * @return The universe set constant.
5346 : : * @warning This function is deprecated and replaced by
5347 : : * `TermManager::mkUniverseSet()`. It will be removed in a future
5348 : : * release.
5349 : : */
5350 : : [[deprecated("Use TermManager::mkUniverseSet() instead")]] Term mkUniverseSet(
5351 : : const Sort& sort) const;
5352 : :
5353 : : /**
5354 : : * Create a bit-vector constant of given size and value.
5355 : : *
5356 : : * @note The given value must fit into a bit-vector of the given size.
5357 : : *
5358 : : * @param size The bit-width of the bit-vector sort.
5359 : : * @param val The value of the constant.
5360 : : * @return The bit-vector constant.
5361 : : * @warning This function is deprecated and replaced by
5362 : : * `TermManager::mkBitVector()`. It will be removed in a future
5363 : : * release.
5364 : : */
5365 : : [[deprecated("Use TermManager::mkBitVector() instead")]] Term mkBitVector(
5366 : : uint32_t size, uint64_t val = 0) const;
5367 : :
5368 : : /**
5369 : : * Create a bit-vector constant of a given bit-width from a given string of
5370 : : * base 2, 10 or 16.
5371 : : *
5372 : : * @note The given value must fit into a bit-vector of the given size.
5373 : : *
5374 : : * @param size The bit-width of the constant.
5375 : : * @param s The string representation of the constant.
5376 : : * @param base The base of the string representation (`2` for binary, `10`
5377 : : * for decimal, and `16` for hexadecimal).
5378 : : * @return The bit-vector constant.
5379 : : * @warning This function is deprecated and replaced by
5380 : : * `TermManager::mkBitVector()`. It will be removed in a future
5381 : : * release.
5382 : : */
5383 : : [[deprecated("Use TermManager::mkBitVector() instead")]] Term mkBitVector(
5384 : : uint32_t size, const std::string& s, uint32_t base) const;
5385 : :
5386 : : /**
5387 : : * Create a finite field constant in a given field from a given string
5388 : : * of base n.
5389 : : *
5390 : : * @param value The string representation of the constant.
5391 : : * @param sort The field sort.
5392 : : * @param base The base of the string representation of `value`.
5393 : : *
5394 : : * If `size` is the field size, the constant needs not be in the range
5395 : : * [0,size). If it is outside this range, it will be reduced modulo size
5396 : : * before being constructed.
5397 : : * @warning This function is deprecated and replaced by
5398 : : * `TermManager::mkFiniteFieldElem()`. It will be removed in a future
5399 : : * release.
5400 : : */
5401 : : [[deprecated("Use TermManager::mkFiniteFieldElem() instead")]] Term
5402 : : mkFiniteFieldElem(const std::string& value,
5403 : : const Sort& sort,
5404 : : uint32_t base = 10) const;
5405 : :
5406 : : /**
5407 : : * Create a constant array with the provided constant value stored at every
5408 : : * index.
5409 : : * @param sort The sort of the constant array (must be an array sort).
5410 : : * @param val The constant value to store (must match the sort's element
5411 : : * sort).
5412 : : * @return The constant array term.
5413 : : * @warning This function is deprecated and replaced by
5414 : : * `TermManager::mkConstArray()`. It will be removed in a future
5415 : : * release.
5416 : : */
5417 : : [[deprecated("Use TermManager::mkConstArray() instead")]] Term mkConstArray(
5418 : : const Sort& sort, const Term& val) const;
5419 : :
5420 : : /**
5421 : : * Create a positive infinity floating-point constant (SMT-LIB: `+oo`).
5422 : : * @param exp Number of bits in the exponent.
5423 : : * @param sig Number of bits in the significand.
5424 : : * @return The floating-point constant.
5425 : : * @warning This function is deprecated and replaced by
5426 : : * `TermManager::mkFloatingPointPosInf()`. It will be removed in a
5427 : : * future release.
5428 : : */
5429 : : [[deprecated("Use TermManager::mkFloatingPointPosInf() instead")]] Term
5430 : : mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const;
5431 : :
5432 : : /**
5433 : : * Create a negative infinity floating-point constant (SMT-LIB: `-oo`).
5434 : : * @param exp Number of bits in the exponent.
5435 : : * @param sig Number of bits in the significand.
5436 : : * @return The floating-point constant.
5437 : : * @warning This function is deprecated and replaced by
5438 : : * `TermManager::mkFloatingPointNegInf()`. It will be removed in a
5439 : : * future release.
5440 : : */
5441 : : [[deprecated("Use TermManager::mkFloatingPointNegInf() instead")]] Term
5442 : : mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const;
5443 : :
5444 : : /**
5445 : : * Create a not-a-number floating-point constant (SMT-LIB: `NaN`).
5446 : : * @param exp Number of bits in the exponent.
5447 : : * @param sig Number of bits in the significand.
5448 : : * @return The floating-point constant.
5449 : : * @warning This function is deprecated and replaced by
5450 : : * `TermManager::mkFloatingPointNaN()`. It will be removed in a
5451 : : * future release.
5452 : : */
5453 : : [[deprecated("Use TermManager::mkFloatingPointNaN() instead")]] Term
5454 : : mkFloatingPointNaN(uint32_t exp, uint32_t sig) const;
5455 : :
5456 : : /**
5457 : : * Create a positive zero floating-point constant (SMT-LIB: +zero).
5458 : : * @param exp Number of bits in the exponent.
5459 : : * @param sig Number of bits in the significand.
5460 : : * @return The floating-point constant.
5461 : : * @warning This function is deprecated and replaced by
5462 : : * `TermManager::mkFloatingPointPosZero()`. It will be removed in a
5463 : : * future release.
5464 : : */
5465 : : [[deprecated("Use TermManager::mkFloatingPointPosZero() instead")]] Term
5466 : : mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const;
5467 : :
5468 : : /**
5469 : : * Create a negative zero floating-point constant (SMT-LIB: -zero).
5470 : : * @param exp Number of bits in the exponent.
5471 : : * @param sig Number of bits in the significand.
5472 : : * @return The floating-point constant.
5473 : : * @warning This function is deprecated and replaced by
5474 : : * `TermManager::mkFloatingPointNegZero()`. It will be removed in a
5475 : : * future release.
5476 : : */
5477 : : [[deprecated("Use TermManager::mkFloatingPointNegZero() instead")]] Term
5478 : : mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const;
5479 : :
5480 : : /**
5481 : : * Create a rounding mode value.
5482 : : * @param rm The floating point rounding mode this constant represents.
5483 : : * @return The rounding mode value.
5484 : : * @warning This function is deprecated and replaced by
5485 : : * `TermManager::mkRoundingMode()`. It will be removed in a future
5486 : : * release.
5487 : : */
5488 : : [[deprecated("Use TermManager::mkRoundingMode() instead")]] Term
5489 : : mkRoundingMode(RoundingMode rm) const;
5490 : :
5491 : : /**
5492 : : * Create a floating-point value from a bit-vector given in IEEE-754
5493 : : * format.
5494 : : * @param exp Size of the exponent.
5495 : : * @param sig Size of the significand.
5496 : : * @param val Value of the floating-point constant as a bit-vector term.
5497 : : * @return The floating-point value.
5498 : : * @warning This function is deprecated and replaced by
5499 : : * `TermManager::mkFloatingPoint()`. It will be removed in a future
5500 : : * release.
5501 : : */
5502 : : [[deprecated("Use TermManager::mkFloatingPoint() instead")]] Term
5503 : : mkFloatingPoint(uint32_t exp, uint32_t sig, const Term& val) const;
5504 : : /**
5505 : : * Create a floating-point value from its three IEEE-754 bit-vector
5506 : : * value components (sign bit, exponent, significand).
5507 : : * @param sign The sign bit.
5508 : : * @param exp The bit-vector representing the exponent.
5509 : : * @param sig The bit-vector representing the significand.
5510 : : * @return The floating-point value.
5511 : : * @warning This function is deprecated and replaced by
5512 : : * `TermManager::mkFloatingPoint()`. It will be removed in a future
5513 : : * release.
5514 : : */
5515 : : [[deprecated("Use TermManager::mkFloatingPoint() instead")]] Term
5516 : : mkFloatingPoint(const Term& sign, const Term& exp, const Term& sig) const;
5517 : :
5518 : : /**
5519 : : * Create a cardinality constraint for an uninterpreted sort.
5520 : : *
5521 : : * @warning This function is experimental and may change in future versions.
5522 : : *
5523 : : * @param sort The sort the cardinality constraint is for.
5524 : : * @param upperBound The upper bound on the cardinality of the sort.
5525 : : * @return The cardinality constraint.
5526 : : * @warning This function is deprecated and replaced by
5527 : : * `TermManager::mkCardinalityConstraint()`. It will be removed in a
5528 : : * future release.
5529 : : */
5530 : : [[deprecated("Use TermManager::mkCardinalityConstraint() instead")]] Term
5531 : : mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const;
5532 : :
5533 : : /* .................................................................... */
5534 : : /* Create Variables */
5535 : : /* .................................................................... */
5536 : :
5537 : : /**
5538 : : * Create a free constant.
5539 : : *
5540 : : * Note that the returned term is always fresh, even if the same arguments
5541 : : * were provided on a previous call to mkConst().
5542 : : *
5543 : : * SMT-LIB:
5544 : : *
5545 : : * \verbatim embed:rst:leading-asterisk
5546 : : * .. code:: smtlib
5547 : : *
5548 : : * (declare-const <symbol> <sort>)
5549 : : * (declare-fun <symbol> () <sort>)
5550 : : * \endverbatim
5551 : : *
5552 : : * @param sort The sort of the constant.
5553 : : * @param symbol The name of the constant (optional).
5554 : : * @return The constant.
5555 : : * @warning This function is deprecated and replaced by
5556 : : * `TermManager::mkConst()`. It will be removed in a future release.
5557 : : */
5558 : : [[deprecated("Use TermManager::mkConst() instead")]] Term mkConst(
5559 : : const Sort& sort,
5560 : : const std::optional<std::string>& symbol = std::nullopt) const;
5561 : :
5562 : : /**
5563 : : * Create a bound variable to be used in a binder (i.e., a quantifier, a
5564 : : * lambda, or a witness binder).
5565 : : *
5566 : : * Note that the returned term is always fresh, even if the same arguments
5567 : : * were provided on a previous call to mkConst.
5568 : : *
5569 : : * @param sort The sort of the variable.
5570 : : * @param symbol The name of the variable (optional).
5571 : : * @return The variable.
5572 : : * @warning This function is deprecated and replaced by
5573 : : * `TermManager::mkVar()`. It will be removed in a future release.
5574 : : */
5575 : : [[deprecated("Use TermManager::mkVar() instead")]] Term mkVar(
5576 : : const Sort& sort,
5577 : : const std::optional<std::string>& symbol = std::nullopt) const;
5578 : :
5579 : : /* .................................................................... */
5580 : : /* Create datatype constructor declarations */
5581 : : /* .................................................................... */
5582 : :
5583 : : /**
5584 : : * Create a datatype constructor declaration.
5585 : : * @param name The name of the datatype constructor.
5586 : : * @return The DatatypeConstructorDecl.
5587 : : * @warning This function is deprecated and replaced by
5588 : : * `TermManager::mkDatatypeConstructorDecl()`. It will be removed in
5589 : : * a future release.
5590 : : */
5591 : : [[deprecated(
5592 : : "Use TermManager::mkDatatypeConstructorDecl() "
5593 : : "instead")]] DatatypeConstructorDecl
5594 : : mkDatatypeConstructorDecl(const std::string& name);
5595 : :
5596 : : /* .................................................................... */
5597 : : /* Create datatype declarations */
5598 : : /* .................................................................... */
5599 : :
5600 : : /**
5601 : : * Create a datatype declaration.
5602 : : * @param name The name of the datatype.
5603 : : * @param isCoDatatype True if a codatatype is to be constructed.
5604 : : * @return The DatatypeDecl.
5605 : : * @warning This function is deprecated and replaced by
5606 : : * `TermManager::mkDatatypeDecl()`. It will be removed in a future
5607 : : * release.
5608 : : */
5609 : : [[deprecated("Use TermManager::mkDatatypeDecl() instead")]] DatatypeDecl
5610 : : mkDatatypeDecl(const std::string& name, bool isCoDatatype = false);
5611 : :
5612 : : /**
5613 : : * Create a datatype declaration.
5614 : : * Create sorts parameter with TermManager::mkParamSort().
5615 : : *
5616 : : * @warning This function is experimental and may change in future versions.
5617 : : *
5618 : : * @param name The name of the datatype.
5619 : : * @param params A list of sort parameters.
5620 : : * @param isCoDatatype True if a codatatype is to be constructed.
5621 : : * @return The DatatypeDecl.
5622 : : * @warning This function is deprecated and replaced by
5623 : : * `TermManager::mkDatatypeDecl()`. It will be removed in a future
5624 : : * release.
5625 : : */
5626 : : [[deprecated("Use TermManager::mkDatatypeDecl() instead")]] DatatypeDecl
5627 : : mkDatatypeDecl(const std::string& name,
5628 : : const std::vector<Sort>& params,
5629 : : bool isCoDatatype = false);
5630 : :
5631 : : /* .................................................................... */
5632 : : /* Formula Handling */
5633 : : /* .................................................................... */
5634 : :
5635 : : /**
5636 : : * Simplify a term or formula based on rewriting and (optionally) applying
5637 : : * substitutions for solved variables.
5638 : : *
5639 : : * If applySubs is true, then for example, if `(= x 0)` was asserted to this
5640 : : * solver, this method may replace occurrences of `x` with `0`.
5641 : : *
5642 : : * @warning This function is experimental and may change in future versions.
5643 : : *
5644 : : * @param t The term to simplify.
5645 : : * @param applySubs True to apply substitutions for solved variables.
5646 : : * @return The simplified term.
5647 : : */
5648 : : Term simplify(const Term& t, bool applySubs = false);
5649 : :
5650 : : /**
5651 : : * Assert a formula.
5652 : : *
5653 : : * SMT-LIB:
5654 : : *
5655 : : * \verbatim embed:rst:leading-asterisk
5656 : : * .. code:: smtlib
5657 : : *
5658 : : * (assert <term>)
5659 : : * \endverbatim
5660 : : *
5661 : : * @param term The formula to assert.
5662 : : */
5663 : : void assertFormula(const Term& term) const;
5664 : :
5665 : : /**
5666 : : * Check satisfiability.
5667 : : *
5668 : : * SMT-LIB:
5669 : : *
5670 : : * \verbatim embed:rst:leading-asterisk
5671 : : * .. code:: smtlib
5672 : : *
5673 : : * (check-sat)
5674 : : * \endverbatim
5675 : : *
5676 : : * @return The result of the satisfiability check.
5677 : : */
5678 : : Result checkSat() const;
5679 : :
5680 : : /**
5681 : : * Check satisfiability assuming the given formula.
5682 : : *
5683 : : * SMT-LIB:
5684 : : *
5685 : : * \verbatim embed:rst:leading-asterisk
5686 : : * .. code:: smtlib
5687 : : *
5688 : : * (check-sat-assuming ( <prop_literal> ))
5689 : : * \endverbatim
5690 : : *
5691 : : * @param assumption The formula to assume.
5692 : : * @return The result of the satisfiability check.
5693 : : */
5694 : : Result checkSatAssuming(const Term& assumption) const;
5695 : :
5696 : : /**
5697 : : * Check satisfiability assuming the given formulas.
5698 : : *
5699 : : * SMT-LIB:
5700 : : *
5701 : : * \verbatim embed:rst:leading-asterisk
5702 : : * .. code:: smtlib
5703 : : *
5704 : : * (check-sat-assuming ( <prop_literal>+ ))
5705 : : * \endverbatim
5706 : : *
5707 : : * @param assumptions The formulas to assume.
5708 : : * @return The result of the satisfiability check.
5709 : : */
5710 : : Result checkSatAssuming(const std::vector<Term>& assumptions) const;
5711 : :
5712 : : /**
5713 : : * Create datatype sort.
5714 : : *
5715 : : * SMT-LIB:
5716 : : *
5717 : : * \verbatim embed:rst:leading-asterisk
5718 : : * .. code:: smtlib
5719 : : *
5720 : : * (declare-datatype <symbol> <datatype_decl>)
5721 : : * \endverbatim
5722 : : *
5723 : : * @param symbol The name of the datatype sort.
5724 : : * @param ctors The constructor declarations of the datatype sort.
5725 : : * @return The datatype sort.
5726 : : */
5727 : : Sort declareDatatype(const std::string& symbol,
5728 : : const std::vector<DatatypeConstructorDecl>& ctors) const;
5729 : :
5730 : : /**
5731 : : * Declare n-ary function symbol.
5732 : : *
5733 : : * SMT-LIB:
5734 : : *
5735 : : * \verbatim embed:rst:leading-asterisk
5736 : : * .. code:: smtlib
5737 : : *
5738 : : * (declare-fun <symbol> ( <sort>* ) <sort>)
5739 : : * \endverbatim
5740 : : *
5741 : : * @param symbol The name of the function.
5742 : : * @param sorts The sorts of the parameters to this function.
5743 : : * @param sort The sort of the return value of this function.
5744 : : * @param fresh If true, then this method always returns a new Term.
5745 : : * Otherwise, this method will always return the same Term
5746 : : * for each call with the given sorts and symbol where fresh is false.
5747 : : * @return The function.
5748 : : */
5749 : : Term declareFun(const std::string& symbol,
5750 : : const std::vector<Sort>& sorts,
5751 : : const Sort& sort,
5752 : : bool fresh = true) const;
5753 : :
5754 : : /**
5755 : : * Declare uninterpreted sort.
5756 : : *
5757 : : * SMT-LIB:
5758 : : *
5759 : : * \verbatim embed:rst:leading-asterisk
5760 : : * .. code:: smtlib
5761 : : *
5762 : : * (declare-sort <symbol> <numeral>)
5763 : : * \endverbatim
5764 : : *
5765 : : * @note This corresponds to
5766 : : * mkUninterpretedSort(const std::optional<std::string>&)
5767 : : * if arity = 0, and to
5768 : : * mkUninterpretedSortConstructorSort(size_t arity, const
5769 : : * std::optional<std::string>&) if arity > 0.
5770 : : *
5771 : : * @param symbol The name of the sort.
5772 : : * @param arity The arity of the sort.
5773 : : * @param fresh If true, then this method always returns a new Sort.
5774 : : * Otherwise, this method will always return the same Sort
5775 : : * for each call with the given arity and symbol where fresh is false.
5776 : : * @return The sort.
5777 : : */
5778 : : Sort declareSort(const std::string& symbol,
5779 : : uint32_t arity,
5780 : : bool fresh = true) const;
5781 : :
5782 : : /**
5783 : : * Define n-ary function.
5784 : : *
5785 : : * SMT-LIB:
5786 : : *
5787 : : * \verbatim embed:rst:leading-asterisk
5788 : : * .. code:: smtlib
5789 : : *
5790 : : * (define-fun <function_def>)
5791 : : * \endverbatim
5792 : : *
5793 : : * @param symbol The name of the function.
5794 : : * @param bound_vars The parameters to this function.
5795 : : * @param sort The sort of the return value of this function.
5796 : : * @param term The function body.
5797 : : * @param global Determines whether this definition is global (i.e., persists
5798 : : * when popping the context).
5799 : : * @return The function.
5800 : : */
5801 : : Term defineFun(const std::string& symbol,
5802 : : const std::vector<Term>& bound_vars,
5803 : : const Sort& sort,
5804 : : const Term& term,
5805 : : bool global = false) const;
5806 : :
5807 : : /**
5808 : : * Define recursive function.
5809 : : *
5810 : : * SMT-LIB:
5811 : : *
5812 : : * \verbatim embed:rst:leading-asterisk
5813 : : * .. code:: smtlib
5814 : : *
5815 : : * (define-fun-rec <function_def>)
5816 : : * \endverbatim
5817 : : *
5818 : : * @param symbol The name of the function.
5819 : : * @param bound_vars The parameters to this function.
5820 : : * @param sort The sort of the return value of this function.
5821 : : * @param term The function body.
5822 : : * @param global Determines whether this definition is global (i.e., persists
5823 : : * when popping the context).
5824 : : * @return The function.
5825 : : */
5826 : : Term defineFunRec(const std::string& symbol,
5827 : : const std::vector<Term>& bound_vars,
5828 : : const Sort& sort,
5829 : : const Term& term,
5830 : : bool global = false) const;
5831 : :
5832 : : /**
5833 : : * Define recursive function.
5834 : : *
5835 : : * SMT-LIB:
5836 : : *
5837 : : * \verbatim embed:rst:leading-asterisk
5838 : : * .. code:: smtlib
5839 : : *
5840 : : * (define-fun-rec <function_def>)
5841 : : * \endverbatim
5842 : : *
5843 : : * Create parameter `fun` with TermManager::mkConst().
5844 : : *
5845 : : * @param fun The sorted function.
5846 : : * @param bound_vars The parameters to this function.
5847 : : * @param term The function body.
5848 : : * @param global Determines whether this definition is global (i.e., persists
5849 : : * when popping the context).
5850 : : * @return The function.
5851 : : */
5852 : : Term defineFunRec(const Term& fun,
5853 : : const std::vector<Term>& bound_vars,
5854 : : const Term& term,
5855 : : bool global = false) const;
5856 : :
5857 : : /**
5858 : : * Define recursive functions.
5859 : : *
5860 : : * SMT-LIB:
5861 : : *
5862 : : * \verbatim embed:rst:leading-asterisk
5863 : : * .. code:: smtlib
5864 : : *
5865 : : * (define-funs-rec
5866 : : * ( <function_decl>_1 ... <function_decl>_n )
5867 : : * ( <term>_1 ... <term>_n )
5868 : : * )
5869 : : * \endverbatim
5870 : : *
5871 : : * Create elements of parameter `funs` with `TermManager::mkConst()`.
5872 : : *
5873 : : * @param funs The sorted functions.
5874 : : * @param bound_vars The list of parameters to the functions.
5875 : : * @param terms The list of function bodies of the functions.
5876 : : * @param global Determines whether this definition is global (i.e., persists
5877 : : * when popping the context).
5878 : : */
5879 : : void defineFunsRec(const std::vector<Term>& funs,
5880 : : const std::vector<std::vector<Term>>& bound_vars,
5881 : : const std::vector<Term>& terms,
5882 : : bool global = false) const;
5883 : :
5884 : : /**
5885 : : * Get the list of asserted formulas.
5886 : : *
5887 : : * SMT-LIB:
5888 : : *
5889 : : * \verbatim embed:rst:leading-asterisk
5890 : : * .. code:: smtlib
5891 : : *
5892 : : * (get-assertions)
5893 : : * \endverbatim
5894 : : *
5895 : : * @return The list of asserted formulas.
5896 : : */
5897 : : std::vector<Term> getAssertions() const;
5898 : :
5899 : : /**
5900 : : * Get info from the solver.
5901 : : *
5902 : : * SMT-LIB:
5903 : : *
5904 : : * \verbatim embed:rst:leading-asterisk
5905 : : * .. code:: smtlib
5906 : : *
5907 : : * (get-info <info_flag>)
5908 : : * \endverbatim
5909 : : *
5910 : : * @param flag The info flag.
5911 : : * @return The info.
5912 : : */
5913 : : std::string getInfo(const std::string& flag) const;
5914 : :
5915 : : /**
5916 : : * Get the value of a given option.
5917 : : *
5918 : : * SMT-LIB:
5919 : : *
5920 : : * \verbatim embed:rst:leading-asterisk
5921 : : * .. code:: smtlib
5922 : : *
5923 : : * (get-option <keyword>)
5924 : : * \endverbatim
5925 : : *
5926 : : * @param option The option for which the value is queried.
5927 : : * @return A string representation of the option value.
5928 : : */
5929 : : std::string getOption(const std::string& option) const;
5930 : :
5931 : : /**
5932 : : * Get all option names that can be used with setOption(), getOption() and
5933 : : * getOptionInfo().
5934 : : * @return All option names.
5935 : : */
5936 : : std::vector<std::string> getOptionNames() const;
5937 : :
5938 : : /**
5939 : : * Get some information about the given option.
5940 : : *
5941 : : * Check the OptionInfo class for more details on which information is
5942 : : * available.
5943 : : *
5944 : : * @return Information about the given option.
5945 : : */
5946 : : OptionInfo getOptionInfo(const std::string& option) const;
5947 : :
5948 : : /**
5949 : : * Get the driver options, which provide access to options that can not be
5950 : : * communicated properly via getOption() and getOptionInfo().
5951 : : * @return A DriverOptions object.
5952 : : */
5953 : : DriverOptions getDriverOptions() const;
5954 : :
5955 : : /**
5956 : : * Get the set of unsat ("failed") assumptions.
5957 : : *
5958 : : * SMT-LIB:
5959 : : *
5960 : : * \verbatim embed:rst:leading-asterisk
5961 : : * .. code:: smtlib
5962 : : *
5963 : : * (get-unsat-assumptions)
5964 : : *
5965 : : * Requires to enable option
5966 : : * :ref:`produce-unsat-assumptions <lbl-option-produce-unsat-assumptions>`.
5967 : : * \endverbatim
5968 : : *
5969 : : * @return The set of unsat assumptions.
5970 : : */
5971 : : std::vector<Term> getUnsatAssumptions() const;
5972 : :
5973 : : /**
5974 : : * Get the unsatisfiable core.
5975 : : *
5976 : : * SMT-LIB:
5977 : : *
5978 : : * \verbatim embed:rst:leading-asterisk
5979 : : * .. code:: smtlib
5980 : : *
5981 : : * (get-unsat-core)
5982 : : *
5983 : : * Requires to enable option
5984 : : * :ref:`produce-unsat-cores <lbl-option-produce-unsat-cores>`.
5985 : : *
5986 : : * .. note::
5987 : : * In contrast to SMT-LIB, cvc5's API does not distinguish between named
5988 : : * and unnamed assertions when producing an unsatisfiable core.
5989 : : * Additionally, the API allows this option to be called after a check with
5990 : : * assumptions. A subset of those assumptions may be included in the
5991 : : * unsatisfiable core returned by this function.
5992 : : * \endverbatim
5993 : : *
5994 : : * @return A set of terms representing the unsatisfiable core.
5995 : : */
5996 : : std::vector<Term> getUnsatCore() const;
5997 : :
5998 : : /**
5999 : : * Get the lemmas used to derive unsatisfiability.
6000 : : *
6001 : : * SMT-LIB:
6002 : : *
6003 : : * \verbatim embed:rst:leading-asterisk
6004 : : * .. code:: smtlib
6005 : : *
6006 : : * (get-unsat-core-lemmas)
6007 : : *
6008 : : * Requires the SAT proof unsat core mode, so to enable option
6009 : : * :ref:`unsat-cores-mode=sat-proof <lbl-option-unsat-cores-mode>`.
6010 : : * \endverbatim
6011 : : *
6012 : : * @warning This function is experimental and may change in future versions.
6013 : : *
6014 : : * @return A set of terms representing the lemmas used to derive
6015 : : * unsatisfiability.
6016 : : */
6017 : : std::vector<Term> getUnsatCoreLemmas() const;
6018 : :
6019 : : /**
6020 : : * Get a difficulty estimate for an asserted formula. This function is
6021 : : * intended to be called immediately after any response to a checkSat.
6022 : : *
6023 : : * @warning This function is experimental and may change in future versions.
6024 : : *
6025 : : * @return A map from (a subset of) the input assertions to a real value that.
6026 : : * is an estimate of how difficult each assertion was to solve.
6027 : : * Unmentioned assertions can be assumed to have zero difficulty.
6028 : : */
6029 : : std::map<Term, Term> getDifficulty() const;
6030 : :
6031 : : /**
6032 : : * Get a timeout core.
6033 : : *
6034 : : * \verbatim embed:rst:leading-asterisk
6035 : : * This function computes a subset of the current assertions that cause a
6036 : : * timeout. It may make multiple checks for satisfiability internally, each
6037 : : * limited by the timeout value given by
6038 : : * :ref:`timeout-core-timeout <lbl-option-timeout-core-timeout>`.
6039 : : *
6040 : : * If the result is unknown and the reason is timeout, then returned the set
6041 : : * of assertions corresponds to a subset of the current assertions that cause
6042 : : * a timeout in the specified time :ref:`timeout-core-timeout
6043 : : * <lbl-option-timeout-core-timeout>`. If the result is unsat, then the list
6044 : : * of formulas correspond to an unsat core for the current assertions.
6045 : : * Otherwise, the result is sat, indicating that the current assertions are
6046 : : * satisfiable, and the returned set of assertions is empty.
6047 : : * \endverbatim
6048 : : *
6049 : : * SMT-LIB:
6050 : : *
6051 : : * \verbatim embed:rst:leading-asterisk
6052 : : * .. code:: smtlib
6053 : : *
6054 : : * (get-timeout-core)
6055 : : *
6056 : : * \endverbatim
6057 : : *
6058 : : * @warning This function is experimental and may change in future versions.
6059 : : *
6060 : : * @return The result of the timeout core computation. This is a pair
6061 : : * containing a result and a set of assertions.
6062 : : */
6063 : : std::pair<Result, std::vector<Term>> getTimeoutCore() const;
6064 : :
6065 : : /**
6066 : : * Get a timeout core of the given assumptions.
6067 : : *
6068 : : * This function computes a subset of the given assumptions that cause a
6069 : : * timeout when added to the current assertions.
6070 : : *
6071 : : * \verbatim embed:rst:leading-asterisk
6072 : : * If the result is unknown and the reason is timeout, then the set of
6073 : : * assumptions corresponds to a subset of the given assumptions that cause a
6074 : : * timeout when added to the current assertions in the specified time
6075 : : * :ref:`timeout-core-timeout <lbl-option-timeout-core-timeout>`. If the
6076 : : * result is unsat, then the set of assumptions together with the current
6077 : : * assertions correspond to an unsat core for the current assertions.
6078 : : * Otherwise, the result is sat, indicating that the given assumptions plus
6079 : : * the current assertions are satisfiable, and the returned set of
6080 : : * assumptions is empty.
6081 : : * \endverbatim
6082 : : *
6083 : : * @note This command does not require being preceeded by a call to
6084 : : * `checkSat()`.
6085 : : *
6086 : : * SMT-LIB:
6087 : : *
6088 : : * \verbatim embed:rst:leading-asterisk
6089 : : * .. code:: smtlib
6090 : : *
6091 : : * (get-timeout-core (<assert>*))
6092 : : * \endverbatim
6093 : : *
6094 : : * @warning This function is experimental and may change in future versions.
6095 : : *
6096 : : * @param assumptions The (non-empty) set of formulas to assume.
6097 : : *
6098 : : * @return The result of the timeout core computation. This is a pair
6099 : : * containing a result and a set of assumptions.
6100 : : */
6101 : : std::pair<Result, std::vector<Term>> getTimeoutCoreAssuming(
6102 : : const std::vector<Term>& assumptions) const;
6103 : : /**
6104 : : * Get a proof associated with the most recent call to checkSat.
6105 : : *
6106 : : * SMT-LIB:
6107 : : *
6108 : : * \verbatim embed:rst:leading-asterisk
6109 : : * .. code:: smtlib
6110 : : *
6111 : : * (get-proof :c)
6112 : : *
6113 : : * Requires to enable option
6114 : : * :ref:`produce-proofs <lbl-option-produce-proofs>`.
6115 : : * The string representation depends on the value of option
6116 : : * :ref:`produce-proofs <lbl-option-proof-format-mode>`.
6117 : : * \endverbatim
6118 : : *
6119 : : * @warning This function is experimental and may change in future versions.
6120 : : *
6121 : : * @param c The component of the proof to return
6122 : : * @return A vector of proofs.
6123 : : */
6124 : : std::vector<Proof> getProof(
6125 : : modes::ProofComponent c = modes::ProofComponent::FULL) const;
6126 : :
6127 : : /**
6128 : : * Prints a proof as a string in a selected proof format mode.
6129 : : * Other aspects of printing are taken from the solver options.
6130 : : *
6131 : : * @warning This function is experimental and may change in future versions.
6132 : : *
6133 : : * @param proof A proof, usually obtained from Solver::getProof().
6134 : : * @param format The proof format used to print the proof. Must be
6135 : : * `modes::ProofFormat::NONE` if the proof is from a component other than
6136 : : * `modes::ProofComponent::FULL`.
6137 : : * @param assertionNames Mapping between assertions and names, if they were
6138 : : * given by the user. This is used by the Alethe proof format.
6139 : : * @return The string representation of the proof in the given format.
6140 : : */
6141 : : std::string proofToString(
6142 : : Proof proof,
6143 : : modes::ProofFormat format = modes::ProofFormat::DEFAULT,
6144 : : const std::map<cvc5::Term, std::string>& assertionNames =
6145 : : std::map<cvc5::Term, std::string>()) const;
6146 : :
6147 : : /**
6148 : : * Get a list of learned literals that are entailed by the current set of
6149 : : * assertions.
6150 : : *
6151 : : * @warning This function is experimental and may change in future versions.
6152 : : *
6153 : : * @param t The type of learned literals to return
6154 : : * @return A list of literals that were learned at top-level.
6155 : : */
6156 : : std::vector<Term> getLearnedLiterals(
6157 : : modes::LearnedLitType t = modes::LearnedLitType::INPUT) const;
6158 : :
6159 : : /**
6160 : : * Get the value of the given term in the current model.
6161 : : *
6162 : : * SMT-LIB:
6163 : : *
6164 : : * \verbatim embed:rst:leading-asterisk
6165 : : * .. code:: smtlib
6166 : : *
6167 : : * (get-value ( <term> ))
6168 : : * \endverbatim
6169 : : *
6170 : : * @param term The term for which the value is queried.
6171 : : * @return The value of the given term.
6172 : : */
6173 : : Term getValue(const Term& term) const;
6174 : :
6175 : : /**
6176 : : * Get the values of the given terms in the current model.
6177 : : *
6178 : : * SMT-LIB:
6179 : : *
6180 : : * \verbatim embed:rst:leading-asterisk
6181 : : * .. code:: smtlib
6182 : : *
6183 : : * (get-value ( <term>* ))
6184 : : * \endverbatim
6185 : : *
6186 : : * @param terms The terms for which the value is queried.
6187 : : * @return The values of the given terms.
6188 : : */
6189 : : std::vector<Term> getValue(const std::vector<Term>& terms) const;
6190 : :
6191 : : /**
6192 : : * Get the domain elements of uninterpreted sort s in the current model. The
6193 : : * current model interprets s as the finite sort whose domain elements are
6194 : : * given in the return value of this function.
6195 : : *
6196 : : * @param s The uninterpreted sort in question.
6197 : : * @return The domain elements of s in the current model.
6198 : : */
6199 : : std::vector<Term> getModelDomainElements(const Sort& s) const;
6200 : :
6201 : : /**
6202 : : * Determine if the model value of the given free constant was essential for
6203 : : * showing satisfiability of the last `checkSat()` query based on the current
6204 : : * model.
6205 : : *
6206 : : * For any free constant `v`, this will only return false if
6207 : : * \verbatim embed:rst:inline :ref:`model-cores
6208 : : * <lbl-option-model-cores>`\endverbatim
6209 : : * has been set to true.
6210 : : * @warning This function is experimental and may change in future versions.
6211 : : *
6212 : : * @param v The term in question.
6213 : : * @return True if `v` is a model core symbol.
6214 : : */
6215 : : bool isModelCoreSymbol(const Term& v) const;
6216 : :
6217 : : /**
6218 : : * Get the model
6219 : : *
6220 : : * SMT-LIB:
6221 : : *
6222 : : * \verbatim embed:rst:leading-asterisk
6223 : : * .. code:: smtlib
6224 : : *
6225 : : * (get-model)
6226 : : *
6227 : : * Requires to enable option
6228 : : * :ref:`produce-models <lbl-option-produce-models>`.
6229 : : * \endverbatim
6230 : : *
6231 : : * @warning This function is experimental and may change in future versions.
6232 : : *
6233 : : * @param sorts The list of uninterpreted sorts that should be printed in
6234 : : * the model.
6235 : : * @param consts The list of free constants that should be printed in the
6236 : : * model. A subset of these may be printed based on
6237 : : * isModelCoreSymbol().
6238 : : * @return A string representing the model.
6239 : : */
6240 : : std::string getModel(const std::vector<Sort>& sorts,
6241 : : const std::vector<Term>& consts) const;
6242 : :
6243 : : /**
6244 : : * Do quantifier elimination.
6245 : : *
6246 : : * SMT-LIB:
6247 : : *
6248 : : * \verbatim embed:rst:leading-asterisk
6249 : : * .. code:: smtlib
6250 : : *
6251 : : * (get-qe <q>)
6252 : : * \endverbatim
6253 : : *
6254 : : * @note Quantifier Elimination is is only complete for logics such as LRA,
6255 : : * LIA and BV.
6256 : : *
6257 : : * @warning This function is experimental and may change in future versions.
6258 : : *
6259 : : * @param q A quantified formula of the form
6260 : : * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
6261 : : * where
6262 : : * @f$Q\bar{x}@f$ is a set of quantified variables of the form
6263 : : * @f$Q x_1...x_k@f$ and
6264 : : * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
6265 : : * @return A formula @f$\phi@f$ such that, given the current set of formulas
6266 : : * @f$A@f$ asserted to this solver:
6267 : : * - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent
6268 : : * - @f$\phi@f$ is quantifier-free formula containing only free
6269 : : * variables in @f$y_1...y_n@f$.
6270 : : */
6271 : : Term getQuantifierElimination(const Term& q) const;
6272 : :
6273 : : /**
6274 : : * Do partial quantifier elimination, which can be used for incrementally
6275 : : * computing the result of a quantifier elimination.
6276 : : *
6277 : : * SMT-LIB:
6278 : : *
6279 : : * \verbatim embed:rst:leading-asterisk
6280 : : * .. code:: smtlib
6281 : : *
6282 : : * (get-qe-disjunct <q>)
6283 : : * \endverbatim
6284 : : *
6285 : : * @note Quantifier Elimination is is only complete for logics such as LRA,
6286 : : * LIA and BV.
6287 : : *
6288 : : * @warning This function is experimental and may change in future versions.
6289 : : *
6290 : : * @param q A quantified formula of the form
6291 : : * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$
6292 : : * where
6293 : : * @f$Q\bar{x}@f$ is a set of quantified variables of the form
6294 : : * @f$Q x_1...x_k@f$ and
6295 : : * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula
6296 : : * @return A formula @f$\phi@f$ such that, given the current set of formulas
6297 : : * @f$A@f$ asserted to this solver:
6298 : : * - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is
6299 : : * @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if
6300 : : * @f$Q@f$ is @f$\exists@f$
6301 : : * - @f$\phi@f$ is quantifier-free formula containing only free
6302 : : * variables in @f$y_1...y_n@f$
6303 : : * - If @f$Q@f$ is @f$\exists@f$, let @f$(A \wedge Q_n)@f$ be the
6304 : : * formula
6305 : : * @f$(A \wedge \neg (\phi \wedge Q_1) \wedge ... \wedge
6306 : : * \neg (\phi \wedge Q_n))@f$
6307 : : * where for each @f$i = 1...n@f$,
6308 : : * formula @f$(\phi \wedge Q_i)@f$ is the result of calling
6309 : : * Solver::getQuantifierEliminationDisjunct() for @f$q@f$ with the
6310 : : * set of assertions @f$(A \wedge Q_{i-1})@f$.
6311 : : * Similarly, if @f$Q@f$ is @f$\forall@f$, then let
6312 : : * @f$(A \wedge Q_n)@f$ be
6313 : : * @f$(A \wedge (\phi \wedge Q_1) \wedge ... \wedge (\phi \wedge
6314 : : * Q_n))@f$
6315 : : * where @f$(\phi \wedge Q_i)@f$ is the same as above.
6316 : : * In either case, we have that @f$(\phi \wedge Q_j)@f$ will
6317 : : * eventually be true or false, for some finite j.
6318 : : */
6319 : : Term getQuantifierEliminationDisjunct(const Term& q) const;
6320 : :
6321 : : /**
6322 : : * When using separation logic, this sets the location sort and the
6323 : : * datatype sort to the given ones. This function should be invoked exactly
6324 : : * once, before any separation logic constraints are provided.
6325 : : *
6326 : : * @warning This function is experimental and may change in future versions.
6327 : : *
6328 : : * @param locSort The location sort of the heap.
6329 : : * @param dataSort The data sort of the heap.
6330 : : */
6331 : : void declareSepHeap(const Sort& locSort, const Sort& dataSort) const;
6332 : :
6333 : : /**
6334 : : * When using separation logic, obtain the term for the heap.
6335 : : *
6336 : : * @warning This function is experimental and may change in future versions.
6337 : : *
6338 : : * @return The term for the heap.
6339 : : */
6340 : : Term getValueSepHeap() const;
6341 : :
6342 : : /**
6343 : : * When using separation logic, obtain the term for nil.
6344 : : *
6345 : : * @warning This function is experimental and may change in future versions.
6346 : : *
6347 : : * @return The term for nil.
6348 : : */
6349 : : Term getValueSepNil() const;
6350 : :
6351 : : /**
6352 : : * Declare a symbolic pool of terms with the given initial value.
6353 : : *
6354 : : * For details on how pools are used to specify instructions for quantifier
6355 : : * instantiation, see documentation for the #INST_POOL kind.
6356 : : *
6357 : : * SMT-LIB:
6358 : : *
6359 : : * \verbatim embed:rst:leading-asterisk
6360 : : * .. code:: smtlib
6361 : : *
6362 : : * (declare-pool <symbol> <sort> ( <term>* ))
6363 : : * \endverbatim
6364 : : *
6365 : : * @warning This function is experimental and may change in future versions.
6366 : : *
6367 : : * @param symbol The name of the pool.
6368 : : * @param sort The sort of the elements of the pool.
6369 : : * @param initValue The initial value of the pool.
6370 : : * @return The pool symbol.
6371 : : */
6372 : : Term declarePool(const std::string& symbol,
6373 : : const Sort& sort,
6374 : : const std::vector<Term>& initValue) const;
6375 : : /**
6376 : : * Declare an oracle function with reference to an implementation.
6377 : : *
6378 : : * Oracle functions have a different semantics with respect to ordinary
6379 : : * declared functions. In particular, for an input to be satisfiable,
6380 : : * its oracle functions are implicitly universally quantified.
6381 : : *
6382 : : * This function is used in part for implementing this command:
6383 : : *
6384 : : * \verbatim embed:rst:leading-asterisk
6385 : : * .. code:: smtlib
6386 : : *
6387 : : * (declare-oracle-fun <sym> (<sort>*) <sort> <sym>)
6388 : : * \endverbatim
6389 : : *
6390 : : * In particular, the above command is implemented by constructing a
6391 : : * function over terms that wraps a call to binary sym via a text interface.
6392 : : *
6393 : : * @warning This function is experimental and may change in future versions.
6394 : : *
6395 : : * @param symbol The name of the oracle
6396 : : * @param sorts The sorts of the parameters to this function
6397 : : * @param sort The sort of the return value of this function
6398 : : * @param fn The function that implements the oracle function.
6399 : : * @return The oracle function
6400 : : */
6401 : : Term declareOracleFun(const std::string& symbol,
6402 : : const std::vector<Sort>& sorts,
6403 : : const Sort& sort,
6404 : : std::function<Term(const std::vector<Term>&)> fn) const;
6405 : : /**
6406 : : * Add plugin to this solver. Its callbacks will be called throughout the
6407 : : * lifetime of this solver.
6408 : : * @warning This function is experimental and may change in future versions.
6409 : : * @param p The plugin to add to this solver.
6410 : : */
6411 : : void addPlugin(Plugin& p);
6412 : : /**
6413 : : * Pop (a) level(s) from the assertion stack.
6414 : : *
6415 : : * SMT-LIB:
6416 : : *
6417 : : * \verbatim embed:rst:leading-asterisk
6418 : : * .. code:: smtlib
6419 : : *
6420 : : * (pop <numeral>)
6421 : : * \endverbatim
6422 : : *
6423 : : * @param nscopes The number of levels to pop.
6424 : : */
6425 : : void pop(uint32_t nscopes = 1) const;
6426 : :
6427 : : /**
6428 : : * Get an interpolant.
6429 : : *
6430 : : * Given that @f$A\rightarrow B@f$ is valid, this function
6431 : : * determines a term @f$I@f$ over the shared variables of
6432 : : * @f$A@f$ and @f$B@f$, such that @f$A \rightarrow I@f$ and
6433 : : * @f$I \rightarrow B@f$ are valid. @f$A@f$ is the
6434 : : * current set of assertions and @f$B@f$ is the conjecture, given as `conj`.
6435 : : *
6436 : : * SMT-LIB:
6437 : : *
6438 : : * \verbatim embed:rst:leading-asterisk
6439 : : * .. code:: smtlib
6440 : : *
6441 : : * (get-interpolant <symbol> <conj>)
6442 : : *
6443 : : * .. note:: In SMT-LIB, `<symbol>` assigns a symbol to the interpolant.
6444 : : *
6445 : : * .. note:: Requires option
6446 : : * :ref:`produce-interpolants <lbl-option-produce-interpolants>` to
6447 : : * be set to a mode different from `none`.
6448 : : * \endverbatim
6449 : : *
6450 : : * @warning This function is experimental and may change in future versions.
6451 : : *
6452 : : * @param conj The conjecture term.
6453 : : * @return The interpolant, if an interpolant exists, else the null term.
6454 : : */
6455 : : Term getInterpolant(const Term& conj) const;
6456 : :
6457 : : /**
6458 : : * Get an interpolant.
6459 : : *
6460 : : *
6461 : : *
6462 : : * Given that @f$A\rightarrow B@f$ is valid, this function
6463 : : * determines a term @f$I@f$ over the shared variables of
6464 : : * @f$A@f$ and @f$B@f$, such that @f$A \rightarrow I@f$ and
6465 : : * @f$I \rightarrow B@f$ are valid.
6466 : : * @f$I@f$ is constructed from the given grammar.
6467 : : * @f$A@f$ is the
6468 : : * current set of assertions and @f$B@f$ is the conjecture, given as `conj`.
6469 : : *
6470 : : * SMT-LIB:
6471 : : *
6472 : : * \verbatim embed:rst:leading-asterisk
6473 : : * .. code:: smtlib
6474 : : *
6475 : : * (get-interpolant <symbol> <conj> <grammar>)
6476 : : *
6477 : : * .. note:: In SMT-LIB, `<symbol>` assigns a symbol to the interpolant.
6478 : : *
6479 : : * .. note:: Requires option
6480 : : * :ref:`produce-interpolants <lbl-option-produce-interpolants>` to
6481 : : * be set to a mode different from `none`.
6482 : : * \endverbatim
6483 : : *
6484 : : * @warning This function is experimental and may change in future versions.
6485 : : *
6486 : : * @param conj The conjecture term.
6487 : : * @param grammar The grammar for the interpolant I.
6488 : : * @return The interpolant, if an interpolant exists, else the null term.
6489 : : */
6490 : : Term getInterpolant(const Term& conj, Grammar& grammar) const;
6491 : :
6492 : : /**
6493 : : * Get the next interpolant. Can only be called immediately after a successful
6494 : : * call to get-interpolant or get-interpolant-next. Is guaranteed to produce a
6495 : : * syntactically different interpolant wrt the last returned interpolant if
6496 : : * successful.
6497 : : *
6498 : : * SMT-LIB:
6499 : : *
6500 : : * \verbatim embed:rst:leading-asterisk
6501 : : * .. code:: smtlib
6502 : : *
6503 : : * (get-interpolant-next)
6504 : : *
6505 : : * Requires to enable incremental mode, and option
6506 : : * :ref:`produce-interpolants <lbl-option-produce-interpolants>` to be set to
6507 : : * a mode different from `none`. \endverbatim
6508 : : *
6509 : : * @warning This function is experimental and may change in future versions.
6510 : : *
6511 : : * @return A Term @f$I@f$ such that @f$A \rightarrow I@f$ and
6512 : : * @f$I \rightarrow B@f$ are valid, where @f$A@f$ is the
6513 : : * current set of assertions and @f$B@f$ is given in the input by
6514 : : * `conj`, or the null term if such a term cannot be found.
6515 : : */
6516 : : Term getInterpolantNext() const;
6517 : :
6518 : : /**
6519 : : * Get an abduct.
6520 : : *
6521 : : * SMT-LIB:
6522 : : *
6523 : : * \verbatim embed:rst:leading-asterisk
6524 : : * .. code:: smtlib
6525 : : *
6526 : : * (get-abduct <conj>)
6527 : : *
6528 : : * Requires to enable option
6529 : : * :ref:`produce-abducts <lbl-option-produce-abducts>`.
6530 : : * \endverbatim
6531 : : *
6532 : : * @warning This function is experimental and may change in future versions.
6533 : : *
6534 : : * @param conj The conjecture term.
6535 : : * @return A term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable,
6536 : : * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where
6537 : : * @f$A@f$ is the current set of assertions and @f$B@f$ is
6538 : : * given in the input by ``conj``, or the null term if such a term
6539 : : * cannot be found.
6540 : : */
6541 : : Term getAbduct(const Term& conj) const;
6542 : :
6543 : : /**
6544 : : * Get an abduct.
6545 : : *
6546 : : * SMT-LIB:
6547 : : *
6548 : : * \verbatim embed:rst:leading-asterisk
6549 : : * .. code:: smtlib
6550 : : *
6551 : : * (get-abduct <conj> <grammar>)
6552 : : *
6553 : : * Requires to enable option
6554 : : * :ref:`produce-abducts <lbl-option-produce-abducts>`.
6555 : : * \endverbatim
6556 : : *
6557 : : * @warning This function is experimental and may change in future versions.
6558 : : *
6559 : : *
6560 : : * @param conj The conjecture term.
6561 : : * @param grammar The grammar for the abduct @f$C@f$
6562 : : * @return A term C such that @f$(A \wedge C)@f$ is satisfiable, and
6563 : : * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
6564 : : * the current set of assertions and @f$B@f$ is given in the input by
6565 : : * `conj`, or the null term if such a term cannot be found.
6566 : : */
6567 : : Term getAbduct(const Term& conj, Grammar& grammar) const;
6568 : :
6569 : : /**
6570 : : * Get the next abduct. Can only be called immediately after a successful
6571 : : * call to get-abduct or get-abduct-next. Is guaranteed to produce a
6572 : : * syntactically different abduct wrt the last returned abduct if successful.
6573 : : *
6574 : : * SMT-LIB:
6575 : : *
6576 : : * \verbatim embed:rst:leading-asterisk
6577 : : * .. code:: smtlib
6578 : : *
6579 : : * (get-abduct-next)
6580 : : *
6581 : : * Requires to enable incremental mode, and option
6582 : : * :ref:`produce-abducts <lbl-option-produce-abducts>`.
6583 : : * \endverbatim
6584 : : *
6585 : : * @warning This function is experimental and may change in future versions.
6586 : : *
6587 : : * @return A term C such that @f$(A \wedge C)@f$ is satisfiable, and
6588 : : * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is
6589 : : * the current set of assertions and @f$B@f$ is given in the input by
6590 : : * the last call to getAbduct(), or the null term if such a term
6591 : : * cannot be found.
6592 : : */
6593 : : Term getAbductNext() const;
6594 : :
6595 : : /**
6596 : : * Block the current model. Can be called only if immediately preceded by a
6597 : : * SAT or INVALID query.
6598 : : *
6599 : : * SMT-LIB:
6600 : : *
6601 : : * \verbatim embed:rst:leading-asterisk
6602 : : * .. code:: smtlib
6603 : : *
6604 : : * (block-model)
6605 : : *
6606 : : * Requires enabling option
6607 : : * :ref:`produce-models <lbl-option-produce-models>`.
6608 : : * \endverbatim
6609 : : *
6610 : : * @warning This function is experimental and may change in future versions.
6611 : : *
6612 : : * @param mode The mode to use for blocking.
6613 : : */
6614 : : void blockModel(modes::BlockModelsMode mode) const;
6615 : :
6616 : : /**
6617 : : * Block the current model values of (at least) the values in terms. Can be
6618 : : * called only if immediately preceded by a SAT query.
6619 : : *
6620 : : * SMT-LIB:
6621 : : *
6622 : : * \verbatim embed:rst:leading-asterisk
6623 : : * .. code:: smtlib
6624 : : *
6625 : : * (block-model-values ( <terms>+ ))
6626 : : *
6627 : : * Requires enabling option
6628 : : * :ref:`produce-models <lbl-option-produce-models>`.
6629 : : * \endverbatim
6630 : : *
6631 : : * @warning This function is experimental and may change in future versions.
6632 : : * @param terms The model values to block.
6633 : : */
6634 : : void blockModelValues(const std::vector<Term>& terms) const;
6635 : :
6636 : : /**
6637 : : * @warning This function is experimental and may change in future versions.
6638 : : *
6639 : : * @return A string that contains information about all instantiations made
6640 : : * by the quantifiers module.
6641 : : */
6642 : : std::string getInstantiations() const;
6643 : :
6644 : : /**
6645 : : * Push (a) level(s) to the assertion stack.
6646 : : *
6647 : : * SMT-LIB:
6648 : : *
6649 : : * \verbatim embed:rst:leading-asterisk
6650 : : * .. code:: smtlib
6651 : : *
6652 : : * (push <numeral>)
6653 : : * \endverbatim
6654 : : *
6655 : : * @param nscopes The number of levels to push.
6656 : : */
6657 : : void push(uint32_t nscopes = 1) const;
6658 : :
6659 : : /**
6660 : : * Remove all assertions.
6661 : : *
6662 : : * SMT-LIB:
6663 : : *
6664 : : * \verbatim embed:rst:leading-asterisk
6665 : : * .. code:: smtlib
6666 : : *
6667 : : * (reset-assertions)
6668 : : * \endverbatim
6669 : : *
6670 : : */
6671 : : void resetAssertions() const;
6672 : :
6673 : : /**
6674 : : * Set info.
6675 : : *
6676 : : * SMT-LIB:
6677 : : *
6678 : : * \verbatim embed:rst:leading-asterisk
6679 : : * .. code:: smtlib
6680 : : *
6681 : : * (set-info <attribute>)
6682 : : * \endverbatim
6683 : : *
6684 : : * @param keyword The info flag.
6685 : : * @param value The value of the info flag.
6686 : : */
6687 : : void setInfo(const std::string& keyword, const std::string& value) const;
6688 : :
6689 : : /**
6690 : : * Set logic.
6691 : : *
6692 : : * SMT-LIB:
6693 : : *
6694 : : * \verbatim embed:rst:leading-asterisk
6695 : : * .. code:: smtlib
6696 : : *
6697 : : * (set-logic <symbol>)
6698 : : * \endverbatim
6699 : : *
6700 : : * @param logic The logic to set.
6701 : : */
6702 : : void setLogic(const std::string& logic) const;
6703 : :
6704 : : /**
6705 : : * Determine if `setLogic()` has been called.
6706 : : *
6707 : : * @return True if `setLogic()` has already been called for this solver
6708 : : * instance.
6709 : : */
6710 : : bool isLogicSet() const;
6711 : :
6712 : : /**
6713 : : * Get the logic set the solver.
6714 : : *
6715 : : * @note Asserts isLogicSet().
6716 : : *
6717 : : * @return The logic used by the solver.
6718 : : */
6719 : : std::string getLogic() const;
6720 : :
6721 : : /**
6722 : : * Set option.
6723 : : *
6724 : : * SMT-LIB:
6725 : : *
6726 : : * \verbatim embed:rst:leading-asterisk
6727 : : * .. code:: smtlib
6728 : : *
6729 : : * (set-option :<option> <value>)
6730 : : * \endverbatim
6731 : : *
6732 : : * @param option The option name.
6733 : : * @param value The option value.
6734 : : */
6735 : : void setOption(const std::string& option, const std::string& value) const;
6736 : :
6737 : : /**
6738 : : * Append \p symbol to the current list of universal variables.
6739 : : *
6740 : : * SyGuS v2:
6741 : : *
6742 : : * \verbatim embed:rst:leading-asterisk
6743 : : * .. code:: smtlib
6744 : : *
6745 : : * (declare-var <symbol> <sort>)
6746 : : * \endverbatim
6747 : : *
6748 : : * @param sort The sort of the universal variable.
6749 : : * @param symbol The name of the universal variable.
6750 : : * @return The universal variable.
6751 : : */
6752 : : Term declareSygusVar(const std::string& symbol, const Sort& sort) const;
6753 : :
6754 : : /**
6755 : : * Create a Sygus grammar. The first non-terminal is treated as the starting
6756 : : * non-terminal, so the order of non-terminals matters.
6757 : : *
6758 : : * @param boundVars The parameters to corresponding synth-fun/synth-inv.
6759 : : * @param ntSymbols The pre-declaration of the non-terminal symbols.
6760 : : * @return The grammar.
6761 : : */
6762 : : Grammar mkGrammar(const std::vector<Term>& boundVars,
6763 : : const std::vector<Term>& ntSymbols) const;
6764 : :
6765 : : /**
6766 : : * Synthesize n-ary function.
6767 : : *
6768 : : * SyGuS v2:
6769 : : *
6770 : : * \verbatim embed:rst:leading-asterisk
6771 : : * .. code:: smtlib
6772 : : *
6773 : : * (synth-fun <symbol> ( <boundVars>* ) <sort>)
6774 : : * \endverbatim
6775 : : *
6776 : : * @param symbol The name of the function.
6777 : : * @param boundVars The parameters to this function.
6778 : : * @param sort The sort of the return value of this function.
6779 : : * @return The function.
6780 : : */
6781 : : Term synthFun(const std::string& symbol,
6782 : : const std::vector<Term>& boundVars,
6783 : : const Sort& sort) const;
6784 : :
6785 : : /**
6786 : : * Synthesize n-ary function following specified syntactic constraints.
6787 : : *
6788 : : * SyGuS v2:
6789 : : *
6790 : : * \verbatim embed:rst:leading-asterisk
6791 : : * .. code:: smtlib
6792 : : *
6793 : : * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>)
6794 : : * \endverbatim
6795 : : *
6796 : : * @param symbol The name of the function.
6797 : : * @param boundVars The parameters to this function.
6798 : : * @param sort The sort of the return value of this function.
6799 : : * @param grammar The syntactic constraints.
6800 : : * @return The function.
6801 : : */
6802 : : Term synthFun(const std::string& symbol,
6803 : : const std::vector<Term>& boundVars,
6804 : : Sort sort,
6805 : : Grammar& grammar) const;
6806 : :
6807 : : /**
6808 : : * Add a forumla to the set of Sygus constraints.
6809 : : *
6810 : : * SyGuS v2:
6811 : : *
6812 : : * \verbatim embed:rst:leading-asterisk
6813 : : * .. code:: smtlib
6814 : : *
6815 : : * (constraint <term>)
6816 : : * \endverbatim
6817 : : *
6818 : : * @param term The formula to add as a constraint.
6819 : : */
6820 : : void addSygusConstraint(const Term& term) const;
6821 : :
6822 : : /**
6823 : : * Get the list of sygus constraints.
6824 : : *
6825 : : * @return The list of sygus constraints.
6826 : : */
6827 : : std::vector<Term> getSygusConstraints() const;
6828 : :
6829 : : /**
6830 : : * Add a forumla to the set of Sygus assumptions.
6831 : : *
6832 : : * SyGuS v2:
6833 : : *
6834 : : * \verbatim embed:rst:leading-asterisk
6835 : : * .. code:: smtlib
6836 : : *
6837 : : * (assume <term>)
6838 : : * \endverbatim
6839 : : *
6840 : : * @param term The formula to add as an assumption.
6841 : : */
6842 : : void addSygusAssume(const Term& term) const;
6843 : :
6844 : : /**
6845 : : * Get the list of sygus assumptions.
6846 : : *
6847 : : * @return The list of sygus assumptions.
6848 : : */
6849 : : std::vector<Term> getSygusAssumptions() const;
6850 : :
6851 : : /**
6852 : : * Add a set of Sygus constraints to the current state that correspond to an
6853 : : * invariant synthesis problem.
6854 : : *
6855 : : * SyGuS v2:
6856 : : *
6857 : : * \verbatim embed:rst:leading-asterisk
6858 : : * .. code:: smtlib
6859 : : *
6860 : : * (inv-constraint <inv> <pre> <trans> <post>)
6861 : : * \endverbatim
6862 : : *
6863 : : * @param inv The function-to-synthesize.
6864 : : * @param pre The pre-condition.
6865 : : * @param trans The transition relation.
6866 : : * @param post The post-condition.
6867 : : */
6868 : : void addSygusInvConstraint(const Term& inv,
6869 : : const Term& pre,
6870 : : const Term& trans,
6871 : : const Term& post) const;
6872 : :
6873 : : /**
6874 : : * Try to find a solution for the synthesis conjecture corresponding to the
6875 : : * current list of functions-to-synthesize, universal variables and
6876 : : * constraints.
6877 : : *
6878 : : * SyGuS v2:
6879 : : *
6880 : : * \verbatim embed:rst:leading-asterisk
6881 : : * .. code:: smtlib
6882 : : *
6883 : : * (check-synth)
6884 : : * \endverbatim
6885 : : *
6886 : : * @return The result of the check, which is "solution" if the check found a
6887 : : * solution in which case solutions are available via
6888 : : * getSynthSolutions, "no solution" if it was determined there is no
6889 : : * solution, or "unknown" otherwise.
6890 : : */
6891 : : SynthResult checkSynth() const;
6892 : :
6893 : : /**
6894 : : * Try to find a next solution for the synthesis conjecture corresponding to
6895 : : * the current list of functions-to-synthesize, universal variables and
6896 : : * constraints. Must be called immediately after a successful call to
6897 : : * check-synth or check-synth-next. Requires incremental mode.
6898 : : *
6899 : : * SyGuS v2:
6900 : : *
6901 : : * \verbatim embed:rst:leading-asterisk
6902 : : * .. code:: smtlib
6903 : : *
6904 : : * (check-synth-next)
6905 : : * \endverbatim
6906 : : *
6907 : : * @return The result of the check, which is "solution" if the check found a
6908 : : * solution in which case solutions are available via
6909 : : * getSynthSolutions, "no solution" if it was determined there is no
6910 : : * solution, or "unknown" otherwise.
6911 : : */
6912 : : SynthResult checkSynthNext() const;
6913 : :
6914 : : /**
6915 : : * Get the synthesis solution of the given term. This function should be
6916 : : * called immediately after the solver answers unsat for sygus input.
6917 : : * @param term The term for which the synthesis solution is queried.
6918 : : * @return The synthesis solution of the given term.
6919 : : */
6920 : : Term getSynthSolution(const Term& term) const;
6921 : :
6922 : : /**
6923 : : * Get the synthesis solutions of the given terms. This function should be
6924 : : * called immediately after the solver answers unsat for sygus input.
6925 : : * @param terms The terms for which the synthesis solutions is queried.
6926 : : * @return The synthesis solutions of the given terms.
6927 : : */
6928 : : std::vector<Term> getSynthSolutions(const std::vector<Term>& terms) const;
6929 : :
6930 : : /**
6931 : : * Find a target term of interest using sygus enumeration, with no provided
6932 : : * grammar.
6933 : : *
6934 : : * The solver will infer which grammar to use in this call, which by default
6935 : : * will be the grammars specified by the function(s)-to-synthesize in the
6936 : : * current context.
6937 : : *
6938 : : * SyGuS v2:
6939 : : *
6940 : : * \verbatim embed:rst:leading-asterisk
6941 : : * .. code:: smtlib
6942 : : *
6943 : : * (find-synth :target)
6944 : : * \endverbatim
6945 : : *
6946 : : * @param fst The identifier specifying what kind of term to find
6947 : : * @return The result of the find, which is the null term if this call failed.
6948 : : *
6949 : : * @warning This function is experimental and may change in future versions.
6950 : : */
6951 : : Term findSynth(modes::FindSynthTarget fst) const;
6952 : : /**
6953 : : * Find a target term of interest using sygus enumeration with a provided
6954 : : * grammar.
6955 : : *
6956 : : * SyGuS v2:
6957 : : *
6958 : : * \verbatim embed:rst:leading-asterisk
6959 : : * .. code:: smtlib
6960 : : *
6961 : : * (find-synth :target G)
6962 : : * \endverbatim
6963 : : *
6964 : : * @param fst The identifier specifying what kind of term to find
6965 : : * @param grammar The grammar for the term
6966 : : * @return The result of the find, which is the null term if this call failed.
6967 : : *
6968 : : * @warning This function is experimental and may change in future versions.
6969 : : */
6970 : : Term findSynth(modes::FindSynthTarget fst, Grammar& grammar) const;
6971 : : /**
6972 : : * Try to find a next target term of interest using sygus enumeration. Must
6973 : : * be called immediately after a successful call to find-synth or
6974 : : * find-synth-next.
6975 : : *
6976 : : * SyGuS v2:
6977 : : *
6978 : : * \verbatim embed:rst:leading-asterisk
6979 : : * .. code:: smtlib
6980 : : *
6981 : : * (find-synth-next)
6982 : : * \endverbatim
6983 : : *
6984 : : * @return The result of the find, which is the null term if this call failed.
6985 : : *
6986 : : * @warning This function is experimental and may change in future versions.
6987 : : */
6988 : : Term findSynthNext() const;
6989 : :
6990 : : /**
6991 : : * Get a snapshot of the current state of the statistic values of this
6992 : : * solver. The returned object is completely decoupled from the solver and
6993 : : * will not change when the solver is used again.
6994 : : * @return A snapshot of the current state of the statistic values.
6995 : : */
6996 : : Statistics getStatistics() const;
6997 : :
6998 : : /**
6999 : : * Print the statistics to the given file descriptor, suitable for usage in
7000 : : * signal handlers.
7001 : : * @param fd The file descriptor.
7002 : : */
7003 : : void printStatisticsSafe(int fd) const;
7004 : :
7005 : : /**
7006 : : * Determines if the output stream for the given tag is enabled. Tags can be
7007 : : * enabled with the `output` option (and `-o <tag>` on the command line).
7008 : : *
7009 : : * Requires that a valid tag is given.
7010 : : * @param tag The output tag.
7011 : : * @return True if the given tag is enabled.
7012 : : */
7013 : : bool isOutputOn(const std::string& tag) const;
7014 : :
7015 : : /**
7016 : : * Get an output stream for the given tag.
7017 : : *
7018 : : * Tags can be enabled with the `output` option (and `-o <tag>` on the
7019 : : * command line). Raises an exception when an invalid tag is given.
7020 : : *
7021 : : * @warning This function is experimental and may change in future versions.
7022 : : *
7023 : : * @param tag The output tag.
7024 : : * @return The output stream.
7025 : : */
7026 : : std::ostream& getOutput(const std::string& tag) const;
7027 : :
7028 : : /**
7029 : : * Get a string representation of the version of this solver.
7030 : : * @return The version string.
7031 : : */
7032 : : std::string getVersion() const;
7033 : :
7034 : : /**
7035 : : * Get the associated term manager instance.
7036 : : * @return The term manager.
7037 : : */
7038 : : TermManager& getTermManager() const;
7039 : :
7040 : : private:
7041 : : /**
7042 : : * Constructs a solver with the given original options. This should only be
7043 : : * used internally when the Solver is reset.
7044 : : * @param tm The associated term manager.
7045 : : * @param original The original set of configuration options.
7046 : : */
7047 : : Solver(TermManager& tm, std::unique_ptr<internal::Options>&& original);
7048 : :
7049 : : /**
7050 : : * Synthesize n-ary function following specified syntactic constraints.
7051 : : *
7052 : : * SMT-LIB:
7053 : : *
7054 : : * \verbatim embed:rst:leading-asterisk
7055 : : * .. code:: smtlib
7056 : : *
7057 : : * (synth-fun <symbol> ( <boundVars>* ) <sort> <grammar>?)
7058 : : * \endverbatim
7059 : : *
7060 : : * @param symbol The name of the function.
7061 : : * @param boundVars The parameters to this function.
7062 : : * @param sort The sort of the return value of this function.
7063 : : * @param grammar The syntactic constraints.
7064 : : * @return The function.
7065 : : */
7066 : : Term synthFunHelper(const std::string& symbol,
7067 : : const std::vector<Term>& boundVars,
7068 : : const Sort& sort,
7069 : : Grammar* grammar = nullptr) const;
7070 : :
7071 : : /** Helper for getting timeout cores */
7072 : : std::pair<Result, std::vector<Term>> getTimeoutCoreHelper(
7073 : : const std::vector<Term>& assumptions) const;
7074 : : /**
7075 : : * Get value helper, which accounts for subtyping.
7076 : : * @param term The term to get the value from.
7077 : : * @return The value term.
7078 : : */
7079 : : Term getValueHelper(const Term& term) const;
7080 : :
7081 : : /**
7082 : : * Check that the given term is a valid closed term, which can be used as an
7083 : : * argument to, e.g., assert, get-value, block-model-values, etc.
7084 : : *
7085 : : * @param t The term to check.
7086 : : */
7087 : : void ensureWellFormedTerm(const Term& t) const;
7088 : : /** Vector version of above. */
7089 : : void ensureWellFormedTerms(const std::vector<Term>& ts) const;
7090 : :
7091 : : /** Keep a copy of the original option settings (for resets). */
7092 : : std::unique_ptr<internal::Options> d_originalOptions;
7093 : : /** The SMT engine of this solver. */
7094 : : std::unique_ptr<internal::SolverEngine> d_slv;
7095 : : /** The random number generator of this solver. */
7096 : : std::unique_ptr<internal::Random> d_rng;
7097 : :
7098 : : /** The associated term manager. */
7099 : : TermManager& d_tm;
7100 : : };
7101 : :
7102 : : } // namespace cvc5
7103 : :
7104 : : #endif
|
