1 /******************************************************************************
2 * Top contributors (to current version):
3 * Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
5 * This file is part of the cvc5 project.
7 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8 * in the top-level source directory and their institutional affiliations.
9 * All rights reserved. See the file COPYING in the top-level source
10 * directory for licensing information.
11 * ****************************************************************************
16 #include "cvc5_export.h"
18 #ifndef CVC5__API__CVC5_H
19 #define CVC5__API__CVC5_H
27 #include <unordered_map>
28 #include <unordered_set>
32 #include "api/cpp/cvc5_kind.h"
37 template <bool ref_count
>
39 typedef NodeTemplate
<true> Node
;
44 class DTypeConstructor
;
53 class StatisticsRegistry
;
56 class CommandExecutor
;
65 /* -------------------------------------------------------------------------- */
67 /* -------------------------------------------------------------------------- */
70 * Base class for all API exceptions.
71 * If thrown, all API objects may be in an unsafe state.
73 class CVC5_EXPORT CVC5ApiException
: public std::exception
77 * Construct with message from a string.
78 * @param str The error message.
80 CVC5ApiException(const std::string
& str
) : d_msg(str
) {}
82 * Construct with message from a string stream.
83 * @param stream The error message.
85 CVC5ApiException(const std::stringstream
& stream
) : d_msg(stream
.str()) {}
87 * Retrieve the message from this exception.
88 * @return The error message.
90 const std::string
& getMessage() const { return d_msg
; }
92 * Retrieve the message as a C-style array.
93 * @return The error message.
95 const char* what() const noexcept override
{ return d_msg
.c_str(); }
98 /** The stored error message. */
103 * A recoverable API exception.
104 * If thrown, API objects can still be used.
106 class CVC5_EXPORT CVC5ApiRecoverableException
: public CVC5ApiException
110 * Construct with message from a string.
111 * @param str The error message.
113 CVC5ApiRecoverableException(const std::string
& str
) : CVC5ApiException(str
) {}
115 * Construct with message from a string stream.
116 * @param stream The error message.
118 CVC5ApiRecoverableException(const std::stringstream
& stream
)
119 : CVC5ApiException(stream
.str())
125 * Exception for unsupported command arguments.
126 * If thrown, API objects can still be used.
128 class CVC5_EXPORT CVC5ApiUnsupportedException
: public CVC5ApiRecoverableException
132 * Construct with message from a string.
133 * @param str The error message.
135 CVC5ApiUnsupportedException(const std::string
& str
)
136 : CVC5ApiRecoverableException(str
)
140 * Construct with message from a string stream.
141 * @param stream The error message.
143 CVC5ApiUnsupportedException(const std::stringstream
& stream
)
144 : CVC5ApiRecoverableException(stream
.str())
150 * An option-related API exception.
151 * If thrown, API objects can still be used.
153 class CVC5_EXPORT CVC5ApiOptionException
: public CVC5ApiRecoverableException
157 * Construct with message from a string.
158 * @param str The error message.
160 CVC5ApiOptionException(const std::string
& str
)
161 : CVC5ApiRecoverableException(str
)
165 * Construct with message from a string stream.
166 * @param stream The error message.
168 CVC5ApiOptionException(const std::stringstream
& stream
)
169 : CVC5ApiRecoverableException(stream
.str())
174 /* -------------------------------------------------------------------------- */
176 /* -------------------------------------------------------------------------- */
179 * Encapsulation of a three-valued solver result, with explanations.
181 class CVC5_EXPORT Result
186 enum UnknownExplanation
204 * Return true if Result is empty, i.e., a nullary Result, and not an actual
205 * result returned from a checkSat() (and friends) query.
210 * Return true if query was a satisfiable checkSat() or checkSatAssuming()
216 * Return true if query was an unsatisfiable checkSat() or
217 * checkSatAssuming() query.
219 bool isUnsat() const;
222 * Return true if query was a checkSat() or checkSatAssuming() query and
223 * cvc5 was not able to determine (un)satisfiability.
225 bool isSatUnknown() const;
228 * Return true if corresponding query was an entailed checkEntailed() query.
230 bool isEntailed() const;
233 * Return true if corresponding query was a checkEntailed() query that is
236 bool isNotEntailed() const;
239 * Return true if query was a checkEntailed() query and cvc5 was not able to
240 * determine if it is entailed.
242 bool isEntailmentUnknown() const;
245 * Operator overloading for equality of two results.
246 * @param r the result to compare to for equality
247 * @return true if the results are equal
249 bool operator==(const Result
& r
) const;
252 * Operator overloading for disequality of two results.
253 * @param r the result to compare to for disequality
254 * @return true if the results are disequal
256 bool operator!=(const Result
& r
) const;
259 * @return an explanation for an unknown query result.
261 UnknownExplanation
getUnknownExplanation() const;
264 * @return a string representation of this result.
266 std::string
toString() const;
271 * @param r the internal result that is to be wrapped by this result
274 Result(const cvc5::Result
& r
);
277 * The interal result wrapped by this result.
278 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::Result is
281 std::shared_ptr
<cvc5::Result
> d_result
;
285 * Serialize a Result to given stream.
286 * @param out the output stream
287 * @param r the result to be serialized to the given output stream
288 * @return the output stream
290 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
) CVC5_EXPORT
;
293 * Serialize an UnknownExplanation to given stream.
294 * @param out the output stream
295 * @param e the explanation to be serialized to the given output stream
296 * @return the output stream
298 std::ostream
& operator<<(std::ostream
& out
,
299 enum Result::UnknownExplanation e
) CVC5_EXPORT
;
301 /* -------------------------------------------------------------------------- */
303 /* -------------------------------------------------------------------------- */
308 * The sort of a cvc5 term.
310 class CVC5_EXPORT Sort
312 friend class cvc5::Command
;
313 friend class DatatypeConstructor
;
314 friend class DatatypeConstructorDecl
;
315 friend class DatatypeSelector
;
316 friend class DatatypeDecl
;
319 friend class Grammar
;
320 friend struct std::hash
<Sort
>;
335 * Comparison for structural equality.
336 * @param s the sort to compare to
337 * @return true if the sorts are equal
339 bool operator==(const Sort
& s
) const;
342 * Comparison for structural disequality.
343 * @param s the sort to compare to
344 * @return true if the sorts are not equal
346 bool operator!=(const Sort
& s
) const;
349 * Comparison for ordering on sorts.
350 * @param s the sort to compare to
351 * @return true if this sort is less than s
353 bool operator<(const Sort
& s
) const;
356 * Comparison for ordering on sorts.
357 * @param s the sort to compare to
358 * @return true if this sort is greater than s
360 bool operator>(const Sort
& s
) const;
363 * Comparison for ordering on sorts.
364 * @param s the sort to compare to
365 * @return true if this sort is less than or equal to s
367 bool operator<=(const Sort
& s
) const;
370 * Comparison for ordering on sorts.
371 * @param s the sort to compare to
372 * @return true if this sort is greater than or equal to s
374 bool operator>=(const Sort
& s
) const;
377 * @return true if this Sort is a null sort.
382 * Is this a Boolean sort?
383 * @return true if the sort is the Boolean sort
385 bool isBoolean() const;
388 * Is this a integer sort?
389 * @return true if the sort is the integer sort
391 bool isInteger() const;
394 * Is this a real sort?
395 * @return true if the sort is the real sort
400 * Is this a string sort?
401 * @return true if the sort is the string sort
403 bool isString() const;
406 * Is this a regexp sort?
407 * @return true if the sort is the regexp sort
409 bool isRegExp() const;
412 * Is this a rounding mode sort?
413 * @return true if the sort is the rounding mode sort
415 bool isRoundingMode() const;
418 * Is this a bit-vector sort?
419 * @return true if the sort is a bit-vector sort
421 bool isBitVector() const;
424 * Is this a floating-point sort?
425 * @return true if the sort is a floating-point sort
427 bool isFloatingPoint() const;
430 * Is this a datatype sort?
431 * @return true if the sort is a datatype sort
433 bool isDatatype() const;
436 * Is this a parametric datatype sort?
437 * @return true if the sort is a parametric datatype sort
439 bool isParametricDatatype() const;
442 * Is this a constructor sort?
443 * @return true if the sort is a constructor sort
445 bool isConstructor() const;
448 * Is this a selector sort?
449 * @return true if the sort is a selector sort
451 bool isSelector() const;
454 * Is this a tester sort?
455 * @return true if the sort is a tester sort
457 bool isTester() const;
459 * Is this a datatype updater sort?
460 * @return true if the sort is a datatype updater sort
462 bool isUpdater() const;
464 * Is this a function sort?
465 * @return true if the sort is a function sort
467 bool isFunction() const;
470 * Is this a predicate sort?
471 * That is, is this a function sort mapping to Boolean? All predicate
472 * sorts are also function sorts.
473 * @return true if the sort is a predicate sort
475 bool isPredicate() const;
478 * Is this a tuple sort?
479 * @return true if the sort is a tuple sort
481 bool isTuple() const;
484 * Is this a record sort?
485 * @return true if the sort is a record sort
487 bool isRecord() const;
490 * Is this an array sort?
491 * @return true if the sort is an array sort
493 bool isArray() const;
496 * Is this a Set sort?
497 * @return true if the sort is a Set sort
502 * Is this a Bag sort?
503 * @return true if the sort is a Bag sort
508 * Is this a Sequence sort?
509 * @return true if the sort is a Sequence sort
511 bool isSequence() const;
514 * Is this an uninterpreted sort?
515 * @return true if this is an uninterpreted sort
517 bool isUninterpretedSort() const;
520 * Is this a sort constructor kind?
521 * @return true if this is a sort constructor kind
523 bool isSortConstructor() const;
526 * Is this a first-class sort?
527 * First-class sorts are sorts for which:
528 * 1. we handle equalities between terms of that type, and
529 * 2. they are allowed to be parameters of parametric sorts (e.g. index or
530 * element sorts of arrays).
532 * Examples of sorts that are not first-class include sort constructor sorts
533 * and regular expression sorts.
535 * @return true if this is a first-class sort
537 bool isFirstClass() const;
540 * Is this a function-LIKE sort?
542 * Anything function-like except arrays (e.g., datatype selectors) is
543 * considered a function here. Function-like terms can not be the argument
544 * or return value for any term that is function-like.
545 * This is mainly to avoid higher order.
547 * Note that arrays are explicitly not considered function-like here.
549 * @return true if this is a function-like sort
551 bool isFunctionLike() const;
554 * Is this sort a subsort of the given sort?
555 * @return true if this sort is a subsort of s
557 bool isSubsortOf(const Sort
& s
) const;
560 * Is this sort comparable to the given sort (i.e., do they share
561 * a common ancestor in the subsort tree)?
562 * @return true if this sort is comparable to s
564 bool isComparableTo(const Sort
& s
) const;
567 * @return the underlying datatype of a datatype sort
569 Datatype
getDatatype() const;
572 * Instantiate a parameterized datatype/sort sort.
573 * Create sorts parameter with Solver::mkParamSort().
574 * @param params the list of sort parameters to instantiate with
576 Sort
instantiate(const std::vector
<Sort
>& params
) const;
579 * Substitution of Sorts.
580 * @param sort the subsort to be substituted within this sort.
581 * @param replacement the sort replacing the substituted subsort.
583 Sort
substitute(const Sort
& sort
, const Sort
& replacement
) const;
586 * Simultaneous substitution of Sorts.
587 * @param sorts the subsorts to be substituted within this sort.
588 * @param replacements the sort replacing the substituted subsorts.
590 Sort
substitute(const std::vector
<Sort
>& sorts
,
591 const std::vector
<Sort
>& replacements
) const;
594 * Output a string representation of this sort to a given stream.
595 * @param out the output stream
597 void toStream(std::ostream
& out
) const;
600 * @return a string representation of this sort
602 std::string
toString() const;
604 /* Constructor sort ------------------------------------------------------- */
607 * @return the arity of a constructor sort
609 size_t getConstructorArity() const;
612 * @return the domain sorts of a constructor sort
614 std::vector
<Sort
> getConstructorDomainSorts() const;
617 * @return the codomain sort of a constructor sort
619 Sort
getConstructorCodomainSort() const;
621 /* Selector sort ------------------------------------------------------- */
624 * @return the domain sort of a selector sort
626 Sort
getSelectorDomainSort() const;
629 * @return the codomain sort of a selector sort
631 Sort
getSelectorCodomainSort() const;
633 /* Tester sort ------------------------------------------------------- */
636 * @return the domain sort of a tester sort
638 Sort
getTesterDomainSort() const;
641 * @return the codomain sort of a tester sort, which is the Boolean sort
643 Sort
getTesterCodomainSort() const;
645 /* Function sort ------------------------------------------------------- */
648 * @return the arity of a function sort
650 size_t getFunctionArity() const;
653 * @return the domain sorts of a function sort
655 std::vector
<Sort
> getFunctionDomainSorts() const;
658 * @return the codomain sort of a function sort
660 Sort
getFunctionCodomainSort() const;
662 /* Array sort ---------------------------------------------------------- */
665 * @return the array index sort of an array sort
667 Sort
getArrayIndexSort() const;
670 * @return the array element sort of an array sort
672 Sort
getArrayElementSort() const;
674 /* Set sort ------------------------------------------------------------ */
677 * @return the element sort of a set sort
679 Sort
getSetElementSort() const;
681 /* Bag sort ------------------------------------------------------------ */
684 * @return the element sort of a bag sort
686 Sort
getBagElementSort() const;
688 /* Sequence sort ------------------------------------------------------- */
691 * @return the element sort of a sequence sort
693 Sort
getSequenceElementSort() const;
695 /* Uninterpreted sort -------------------------------------------------- */
698 * @return the name of an uninterpreted sort
700 std::string
getUninterpretedSortName() const;
703 * @return true if an uninterpreted sort is parameterized
705 bool isUninterpretedSortParameterized() const;
708 * @return the parameter sorts of an uninterpreted sort
710 std::vector
<Sort
> getUninterpretedSortParamSorts() const;
712 /* Sort constructor sort ----------------------------------------------- */
715 * @return the name of a sort constructor sort
717 std::string
getSortConstructorName() const;
720 * @return the arity of a sort constructor sort
722 size_t getSortConstructorArity() const;
724 /* Bit-vector sort ----------------------------------------------------- */
727 * @return the bit-width of the bit-vector sort
729 uint32_t getBitVectorSize() const;
731 /* Floating-point sort ------------------------------------------------- */
734 * @return the bit-width of the exponent of the floating-point sort
736 uint32_t getFloatingPointExponentSize() const;
739 * @return the width of the significand of the floating-point sort
741 uint32_t getFloatingPointSignificandSize() const;
743 /* Datatype sort ------------------------------------------------------- */
747 * Return the parameters of a parametric datatype sort. If this sort is a
748 * non-instantiated parametric datatype, this returns the parameter sorts of
749 * the underlying datatype. If this sort is an instantiated parametric
750 * datatype, then this returns the sort parameters that were used to
751 * construct the sort via ``Sort::instantiate``.
753 * @return the parameter sorts of a parametric datatype sort.
755 std::vector
<Sort
> getDatatypeParamSorts() const;
758 * @return the arity of a datatype sort
760 size_t getDatatypeArity() const;
762 /* Tuple sort ---------------------------------------------------------- */
765 * @return the length of a tuple sort
767 size_t getTupleLength() const;
770 * @return the element sorts of a tuple sort
772 std::vector
<Sort
> getTupleSorts() const;
775 /** @return the internal wrapped TypeNode of this sort. */
776 const cvc5::TypeNode
& getTypeNode(void) const;
778 /** Helper to convert a set of Sorts to internal TypeNodes. */
779 std::set
<TypeNode
> static sortSetToTypeNodes(const std::set
<Sort
>& sorts
);
780 /** Helper to convert a vector of Sorts to internal TypeNodes. */
781 std::vector
<TypeNode
> static sortVectorToTypeNodes(
782 const std::vector
<Sort
>& sorts
);
783 /** Helper to convert a vector of internal TypeNodes to Sorts. */
784 std::vector
<Sort
> static typeNodeVectorToSorts(
785 const Solver
* slv
, const std::vector
<TypeNode
>& types
);
789 * @param slv the associated solver object
790 * @param t the internal type that is to be wrapped by this sort
793 Sort(const Solver
* slv
, const cvc5::TypeNode
& t
);
796 * Helper for isNull checks. This prevents calling an API function with
797 * CVC5_API_CHECK_NOT_NULL
799 bool isNullHelper() const;
802 * The associated solver object.
804 const Solver
* d_solver
;
807 * The internal type wrapped by this sort.
808 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
809 * to memory allocation (cvc5::Type is already ref counted, so this
810 * could be a unique_ptr instead).
812 std::shared_ptr
<cvc5::TypeNode
> d_type
;
816 * Serialize a sort to given stream.
817 * @param out the output stream
818 * @param s the sort to be serialized to the given output stream
819 * @return the output stream
821 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
) CVC5_EXPORT
;
829 * Hash function for Sorts.
832 struct CVC5_EXPORT hash
<cvc5::api::Sort
>
834 size_t operator()(const cvc5::api::Sort
& s
) const;
839 namespace cvc5::api
{
841 /* -------------------------------------------------------------------------- */
843 /* -------------------------------------------------------------------------- */
849 * An operator is a term that represents certain operators, instantiated
850 * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
856 friend struct std::hash
<Op
>;
870 * Syntactic equality operator.
871 * Return true if both operators are syntactically identical.
872 * Both operators must belong to the same solver object.
873 * @param t the operator to compare to for equality
874 * @return true if the operators are equal
876 bool operator==(const Op
& t
) const;
879 * Syntactic disequality operator.
880 * Return true if both operators differ syntactically.
881 * Both terms must belong to the same solver object.
882 * @param t the operator to compare to for disequality
883 * @return true if operators are disequal
885 bool operator!=(const Op
& t
) const;
888 * @return the kind of this operator
890 Kind
getKind() const;
893 * @return true if this operator is a null term
898 * @return true iff this operator is indexed
900 bool isIndexed() const;
903 * @return the number of indices of this op
905 size_t getNumIndices() const;
908 * Get the index at position i.
909 * @param i the position of the index to return
910 * @return the index at position i
913 Term
operator[](size_t i
) const;
916 * Get the indices used to create this Op.
917 * Supports the following template arguments:
921 * - pair<uint32_t, uint32_t>
922 * Check the Op Kind with getKind() to determine which argument to use.
923 * @return the indices used to create this Op
925 template <typename T
>
926 T
getIndices() const;
929 * @return a string representation of this operator
931 std::string
toString() const;
935 * Constructor for a single kind (non-indexed operator).
936 * @param slv the associated solver object
937 * @param k the kind of this Op
939 Op(const Solver
* slv
, const Kind k
);
943 * @param slv the associated solver object
944 * @param k the kind of this Op
945 * @param n the internal node that is to be wrapped by this term
948 Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
);
951 * Helper for isNull checks. This prevents calling an API function with
952 * CVC5_API_CHECK_NOT_NULL
954 bool isNullHelper() const;
957 * Note: An indexed operator has a non-null internal node, d_node
958 * Note 2: We use a helper method to avoid having API functions call
959 * other API functions (we need to call this internally)
960 * @return true iff this Op is indexed
962 bool isIndexedHelper() const;
965 * Helper for getNumIndices
966 * @return the number of indices of this op
968 size_t getNumIndicesHelper() const;
971 * Helper for operator[](size_t index).
972 * @param index position of the index. Should be less than getNumIndicesHelper().
973 * @return the index at position index
975 Term
getIndexHelper(size_t index
) const;
978 * The associated solver object.
980 const Solver
* d_solver
;
982 /** The kind of this operator. */
986 * The internal node wrapped by this operator.
987 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
988 * to memory allocation (cvc5::Node is already ref counted, so this
989 * could be a unique_ptr instead).
991 std::shared_ptr
<cvc5::Node
> d_node
;
995 * Serialize an operator to given stream.
996 * @param out the output stream
997 * @param t the operator to be serialized to the given output stream
998 * @return the output stream
1000 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
) CVC5_EXPORT
;
1002 } // namespace cvc5::api
1006 * Hash function for Ops.
1009 struct CVC5_EXPORT hash
<cvc5::api::Op
>
1011 size_t operator()(const cvc5::api::Op
& t
) const;
1015 namespace cvc5::api
{
1016 /* -------------------------------------------------------------------------- */
1018 /* -------------------------------------------------------------------------- */
1023 class CVC5_EXPORT Term
1025 friend class cvc5::Command
;
1026 friend class Datatype
;
1027 friend class DatatypeConstructor
;
1028 friend class DatatypeSelector
;
1029 friend class Solver
;
1030 friend class Grammar
;
1031 friend struct std::hash
<Term
>;
1035 * Constructor for a null term.
1045 * Syntactic equality operator.
1046 * Return true if both terms are syntactically identical.
1047 * Both terms must belong to the same solver object.
1048 * @param t the term to compare to for equality
1049 * @return true if the terms are equal
1051 bool operator==(const Term
& t
) const;
1054 * Syntactic disequality operator.
1055 * Return true if both terms differ syntactically.
1056 * Both terms must belong to the same solver object.
1057 * @param t the term to compare to for disequality
1058 * @return true if terms are disequal
1060 bool operator!=(const Term
& t
) const;
1063 * Comparison for ordering on terms by their id.
1064 * @param t the term to compare to
1065 * @return true if this term is less than t
1067 bool operator<(const Term
& t
) const;
1070 * Comparison for ordering on terms by their id.
1071 * @param t the term to compare to
1072 * @return true if this term is greater than t
1074 bool operator>(const Term
& t
) const;
1077 * Comparison for ordering on terms by their id.
1078 * @param t the term to compare to
1079 * @return true if this term is less than or equal to t
1081 bool operator<=(const Term
& t
) const;
1084 * Comparison for ordering on terms by their id.
1085 * @param t the term to compare to
1086 * @return true if this term is greater than or equal to t
1088 bool operator>=(const Term
& t
) const;
1090 /** @return the number of children of this term */
1091 size_t getNumChildren() const;
1094 * Get the child term at a given index.
1095 * @param index the index of the child term to return
1096 * @return the child term with the given index
1098 Term
operator[](size_t index
) const;
1101 * @return the id of this term
1103 uint64_t getId() const;
1106 * @return the kind of this term
1108 Kind
getKind() const;
1111 * @return the sort of this term
1113 Sort
getSort() const;
1116 * @return the result of replacing 'term' by 'replacement' in this term
1118 Term
substitute(const Term
& term
, const Term
& replacement
) const;
1121 * @return the result of simultaneously replacing 'terms' by 'replacements'
1124 Term
substitute(const std::vector
<Term
>& terms
,
1125 const std::vector
<Term
>& replacements
) const;
1128 * @return true iff this term has an operator
1133 * @return the Op used to create this term
1134 * Note: This is safe to call when hasOp() returns true.
1139 * @return true if the term has a symbol.
1141 bool hasSymbol() const;
1144 * Asserts hasSymbol().
1145 * @return the raw symbol of the term.
1147 std::string
getSymbol() const;
1150 * @return true if this Term is a null term
1152 bool isNull() const;
1156 * @return the Boolean negation of this term
1158 Term
notTerm() const;
1162 * @param t a Boolean term
1163 * @return the conjunction of this term and the given term
1165 Term
andTerm(const Term
& t
) const;
1169 * @param t a Boolean term
1170 * @return the disjunction of this term and the given term
1172 Term
orTerm(const Term
& t
) const;
1175 * Boolean exclusive or.
1176 * @param t a Boolean term
1177 * @return the exclusive disjunction of this term and the given term
1179 Term
xorTerm(const Term
& t
) const;
1183 * @param t a Boolean term
1184 * @return the Boolean equivalence of this term and the given term
1186 Term
eqTerm(const Term
& t
) const;
1189 * Boolean implication.
1190 * @param t a Boolean term
1191 * @return the implication of this term and the given term
1193 Term
impTerm(const Term
& t
) const;
1196 * If-then-else with this term as the Boolean condition.
1197 * @param then_t the 'then' term
1198 * @param else_t the 'else' term
1199 * @return the if-then-else term with this term as the Boolean condition
1201 Term
iteTerm(const Term
& then_t
, const Term
& else_t
) const;
1204 * @return a string representation of this term
1206 std::string
toString() const;
1209 * Iterator for the children of a Term.
1210 * Note: This treats uninterpreted functions as Term just like any other term
1211 * for example, the term f(x, y) will have Kind APPLY_UF and three
1212 * children: f, x, and y
1214 class CVC5_EXPORT const_iterator
1219 /* The following types are required by trait std::iterator_traits */
1222 using iterator_category
= std::forward_iterator_tag
;
1224 /** The type of the item */
1225 using value_type
= Term
;
1227 /** The pointer type of the item */
1228 using pointer
= const Term
*;
1230 /** The reference type of the item */
1231 using reference
= const Term
&;
1233 /** The type returned when two iterators are subtracted */
1234 using difference_type
= std::ptrdiff_t;
1236 /* End of std::iterator_traits required types */
1245 * @param slv the associated solver object
1246 * @param e a shared pointer to the node that we're iterating over
1247 * @param p the position of the iterator (e.g. which child it's on)
1249 const_iterator(const Solver
* slv
,
1250 const std::shared_ptr
<cvc5::Node
>& e
,
1256 const_iterator(const const_iterator
& it
);
1259 * Assignment operator.
1260 * @param it the iterator to assign to
1261 * @return the reference to the iterator after assignment
1263 const_iterator
& operator=(const const_iterator
& it
);
1266 * Equality operator.
1267 * @param it the iterator to compare to for equality
1268 * @return true if the iterators are equal
1270 bool operator==(const const_iterator
& it
) const;
1273 * Disequality operator.
1274 * @param it the iterator to compare to for disequality
1275 * @return true if the iterators are disequal
1277 bool operator!=(const const_iterator
& it
) const;
1280 * Increment operator (prefix).
1281 * @return a reference to the iterator after incrementing by one
1283 const_iterator
& operator++();
1286 * Increment operator (postfix).
1287 * @return a reference to the iterator after incrementing by one
1289 const_iterator
operator++(int);
1292 * Dereference operator.
1293 * @return the term this iterator points to
1295 Term
operator*() const;
1299 * The associated solver object.
1301 const Solver
* d_solver
;
1302 /** The original node to be iterated over. */
1303 std::shared_ptr
<cvc5::Node
> d_origNode
;
1304 /** Keeps track of the iteration position. */
1309 * @return an iterator to the first child of this Term
1311 const_iterator
begin() const;
1314 * @return an iterator to one-off-the-last child of this Term
1316 const_iterator
end() const;
1319 * @return true if the term is an integer value that fits within int32_t.
1321 bool isInt32Value() const;
1323 * Asserts isInt32Value().
1324 * @return the integer term as a int32_t.
1326 int32_t getInt32Value() const;
1328 * @return true if the term is an integer value that fits within uint32_t.
1330 bool isUInt32Value() const;
1332 * Asserts isUInt32Value().
1333 * @return the integer term as a uint32_t.
1335 uint32_t getUInt32Value() const;
1337 * @return true if the term is an integer value that fits within int64_t.
1339 bool isInt64Value() const;
1341 * Asserts isInt64Value().
1342 * @return the integer term as a int64_t.
1344 int64_t getInt64Value() const;
1346 * @return true if the term is an integer value that fits within uint64_t.
1348 bool isUInt64Value() const;
1350 * Asserts isUInt64Value().
1351 * @return the integer term as a uint64_t.
1353 uint64_t getUInt64Value() const;
1355 * @return true if the term is an integer value.
1357 bool isIntegerValue() const;
1359 * Asserts isIntegerValue().
1360 * @return the integer term in (decimal) string representation.
1362 std::string
getIntegerValue() const;
1365 * @return true if the term is a string value.
1367 bool isStringValue() const;
1369 * Note: This method is not to be confused with toString() which returns
1370 * the term in some string representation, whatever data it may hold. Asserts
1372 * @return the string term as a native string value.
1374 std::wstring
getStringValue() const;
1377 * @return true if the term is a rational value whose numerator and
1378 * denominator fit within int32_t and uint32_t, respectively.
1380 bool isReal32Value() const;
1382 * Asserts isReal32Value().
1383 * @return the representation of a rational value as a pair of its numerator
1386 std::pair
<int32_t, uint32_t> getReal32Value() const;
1388 * @return true if the term is a rational value whose numerator and
1389 * denominator fit within int64_t and uint64_t, respectively.
1391 bool isReal64Value() const;
1393 * Asserts isReal64Value().
1394 * @return the representation of a rational value as a pair of its numerator
1397 std::pair
<int64_t, uint64_t> getReal64Value() const;
1399 * @return true if the term is a rational value.
1401 * Note that a term of kind PI is not considered to be a real value.
1403 bool isRealValue() const;
1405 * Asserts isRealValue().
1406 * @return the representation of a rational value as a (rational) string.
1408 std::string
getRealValue() const;
1411 * @return true if the term is a constant array.
1413 bool isConstArray() const;
1415 * Asserts isConstArray().
1416 * @return the base (element stored at all indices) of a constant array
1418 Term
getConstArrayBase() const;
1421 * @return true if the term is a Boolean value.
1423 bool isBooleanValue() const;
1425 * Asserts isBooleanValue().
1426 * @return the representation of a Boolean value as a native Boolean value.
1428 bool getBooleanValue() const;
1431 * @return true if the term is a bit-vector value.
1433 bool isBitVectorValue() const;
1435 * Asserts isBitVectorValue().
1436 * @return the representation of a bit-vector value in string representation.
1437 * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal
1440 std::string
getBitVectorValue(uint32_t base
= 2) const;
1443 * @return true if the term is an abstract value.
1445 bool isAbstractValue() const;
1447 * Asserts isAbstractValue().
1448 * @return the representation of an abstract value as a string.
1450 std::string
getAbstractValue() const;
1453 * @return true if the term is a tuple value.
1455 bool isTupleValue() const;
1457 * Asserts isTupleValue().
1458 * @return the representation of a tuple value as a vector of terms.
1460 std::vector
<Term
> getTupleValue() const;
1463 * @return true if the term is the floating-point value for positive zero.
1465 bool isFloatingPointPosZero() const;
1467 * @return true if the term is the floating-point value for negative zero.
1469 bool isFloatingPointNegZero() const;
1471 * @return true if the term is the floating-point value for positive
1474 bool isFloatingPointPosInf() const;
1476 * @return true if the term is the floating-point value for negative
1479 bool isFloatingPointNegInf() const;
1481 * @return true if the term is the floating-point value for not a number.
1483 bool isFloatingPointNaN() const;
1485 * @return true if the term is a floating-point value.
1487 bool isFloatingPointValue() const;
1489 * Asserts isFloatingPointValue().
1490 * @return the representation of a floating-point value as a tuple of the
1491 * exponent width, the significand width and a bit-vector value.
1493 std::tuple
<uint32_t, uint32_t, Term
> getFloatingPointValue() const;
1496 * @return true if the term is a set value.
1498 * A term is a set value if it is considered to be a (canonical) constant set
1499 * value. A canonical set value is one whose AST is:
1501 * (union (singleton c1) ... (union (singleton c_{n-1}) (singleton c_n))))
1503 * where `c1 ... cn` are values ordered by id such that `c1 > ... > cn` (see
1504 * also @ref Term::operator>(const Term&) const).
1506 * Note that a universe set term (kind SET_UNIVERSE) is not considered to be
1509 bool isSetValue() const;
1511 * Asserts isSetValue().
1512 * @return the representation of a set value as a set of terms.
1514 std::set
<Term
> getSetValue() const;
1517 * @return true if the term is a sequence value.
1519 bool isSequenceValue() const;
1521 * Asserts isSequenceValue().
1522 * Note that it is usually necessary for sequences to call
1523 * `Solver::simplify()` to turn a sequence that is constructed by, e.g.,
1524 * concatenation of unit sequences, into a sequence value.
1525 * @return the representation of a sequence value as a vector of terms.
1527 std::vector
<Term
> getSequenceValue() const;
1530 * @return true if the term is a value from an uninterpreted sort.
1532 bool isUninterpretedValue() const;
1534 bool @return() const;
1535 * Asserts isUninterpretedValue().
1536 * @return the representation of an uninterpreted value as a pair of its
1540 std::pair
<Sort
, int32_t> getUninterpretedValue() const;
1544 * The associated solver object.
1546 const Solver
* d_solver
;
1549 /** Helper to convert a vector of Terms to internal Nodes. */
1550 std::vector
<Node
> static termVectorToNodes(const std::vector
<Term
>& terms
);
1552 /** Helper method to collect all elements of a set. */
1553 static void collectSet(std::set
<Term
>& set
,
1554 const cvc5::Node
& node
,
1556 /** Helper method to collect all elements of a sequence. */
1557 static void collectSequence(std::vector
<Term
>& seq
,
1558 const cvc5::Node
& node
,
1563 * @param slv the associated solver object
1564 * @param n the internal node that is to be wrapped by this term
1567 Term(const Solver
* slv
, const cvc5::Node
& n
);
1569 /** @return the internal wrapped Node of this term. */
1570 const cvc5::Node
& getNode(void) const;
1573 * Helper for isNull checks. This prevents calling an API function with
1574 * CVC5_API_CHECK_NOT_NULL
1576 bool isNullHelper() const;
1579 * Helper function that returns the kind of the term, which takes into
1580 * account special cases of the conversion for internal to external kinds.
1581 * @return the kind of this term
1583 Kind
getKindHelper() const;
1586 * @return true if the current term is a constant integer that is casted into
1587 * real using the operator CAST_TO_REAL, and returns false otherwise
1589 bool isCastedReal() const;
1591 * The internal node wrapped by this term.
1592 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
1593 * to memory allocation (cvc5::Node is already ref counted, so this
1594 * could be a unique_ptr instead).
1596 std::shared_ptr
<cvc5::Node
> d_node
;
1600 * Serialize a term to given stream.
1601 * @param out the output stream
1602 * @param t the term to be serialized to the given output stream
1603 * @return the output stream
1605 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
) CVC5_EXPORT
;
1608 * Serialize a vector of terms to given stream.
1609 * @param out the output stream
1610 * @param vector the vector of terms to be serialized to the given stream
1611 * @return the output stream
1613 std::ostream
& operator<<(std::ostream
& out
,
1614 const std::vector
<Term
>& vector
) CVC5_EXPORT
;
1617 * Serialize a set of terms to the given stream.
1618 * @param out the output stream
1619 * @param set the set of terms to be serialized to the given stream
1620 * @return the output stream
1622 std::ostream
& operator<<(std::ostream
& out
,
1623 const std::set
<Term
>& set
) CVC5_EXPORT
;
1626 * Serialize an unordered_set of terms to the given stream.
1628 * @param out the output stream
1629 * @param unordered_set the set of terms to be serialized to the given stream
1630 * @return the output stream
1632 std::ostream
& operator<<(std::ostream
& out
,
1633 const std::unordered_set
<Term
>& unordered_set
)
1637 * Serialize a map of terms to the given stream.
1639 * @param out the output stream
1640 * @param map the map of terms to be serialized to the given stream
1641 * @return the output stream
1643 template <typename V
>
1644 std::ostream
& operator<<(std::ostream
& out
,
1645 const std::map
<Term
, V
>& map
) CVC5_EXPORT
;
1648 * Serialize an unordered_map of terms to the given stream.
1650 * @param out the output stream
1651 * @param unordered_map the map of terms to be serialized to the given stream
1652 * @return the output stream
1654 template <typename V
>
1655 std::ostream
& operator<<(std::ostream
& out
,
1656 const std::unordered_map
<Term
, V
>& unordered_map
)
1659 } // namespace cvc5::api
1663 * Hash function for Terms.
1666 struct CVC5_EXPORT hash
<cvc5::api::Term
>
1668 size_t operator()(const cvc5::api::Term
& t
) const;
1672 namespace cvc5::api
{
1674 /* -------------------------------------------------------------------------- */
1676 /* -------------------------------------------------------------------------- */
1678 class DatatypeConstructorIterator
;
1679 class DatatypeIterator
;
1682 * A cvc5 datatype constructor declaration.
1684 class CVC5_EXPORT DatatypeConstructorDecl
1686 friend class DatatypeDecl
;
1687 friend class Solver
;
1691 DatatypeConstructorDecl();
1696 ~DatatypeConstructorDecl();
1699 * Add datatype selector declaration.
1700 * @param name the name of the datatype selector declaration to add
1701 * @param sort the range sort of the datatype selector declaration to add
1703 void addSelector(const std::string
& name
, const Sort
& sort
);
1705 * Add datatype selector declaration whose range type is the datatype itself.
1706 * @param name the name of the datatype selector declaration to add
1708 void addSelectorSelf(const std::string
& name
);
1711 * @return true if this DatatypeConstructorDecl is a null declaration.
1713 bool isNull() const;
1716 * @return a string representation of this datatype constructor declaration
1718 std::string
toString() const;
1723 * @param slv the associated solver object
1724 * @param name the name of the datatype constructor
1725 * @return the DatatypeConstructorDecl
1727 DatatypeConstructorDecl(const Solver
* slv
, const std::string
& name
);
1730 * Helper for isNull checks. This prevents calling an API function with
1731 * CVC5_API_CHECK_NOT_NULL
1733 bool isNullHelper() const;
1736 * Is the underlying constructor resolved (i.e. has it been used to declare
1737 * a datatype already)?
1739 bool isResolved() const;
1742 * The associated solver object.
1744 const Solver
* d_solver
;
1747 * The internal (intermediate) datatype constructor wrapped by this
1748 * datatype constructor declaration.
1749 * Note: This is a shared_ptr rather than a unique_ptr since
1750 * cvc5::DTypeConstructor is not ref counted.
1752 std::shared_ptr
<cvc5::DTypeConstructor
> d_ctor
;
1758 * A cvc5 datatype declaration.
1760 class CVC5_EXPORT DatatypeDecl
1762 friend class DatatypeConstructorArg
;
1763 friend class Solver
;
1764 friend class Grammar
;
1776 * Add datatype constructor declaration.
1777 * @param ctor the datatype constructor declaration to add
1779 void addConstructor(const DatatypeConstructorDecl
& ctor
);
1781 /** Get the number of constructors (so far) for this Datatype declaration. */
1782 size_t getNumConstructors() const;
1784 /** Is this Datatype declaration parametric? */
1785 bool isParametric() const;
1788 * @return true if this DatatypeDecl is a null object
1790 bool isNull() const;
1793 * @return a string representation of this datatype declaration
1795 std::string
toString() const;
1797 /** @return the name of this datatype declaration. */
1798 std::string
getName() const;
1803 * @param slv the associated solver object
1804 * @param name the name of the datatype
1805 * @param isCoDatatype true if a codatatype is to be constructed
1806 * @return the DatatypeDecl
1808 DatatypeDecl(const Solver
* slv
,
1809 const std::string
& name
,
1810 bool isCoDatatype
= false);
1813 * Constructor for parameterized datatype declaration.
1814 * Create sorts parameter with Solver::mkParamSort().
1815 * @param slv the associated solver object
1816 * @param name the name of the datatype
1817 * @param param the sort parameter
1818 * @param isCoDatatype true if a codatatype is to be constructed
1820 DatatypeDecl(const Solver
* slv
,
1821 const std::string
& name
,
1823 bool isCoDatatype
= false);
1826 * Constructor for parameterized datatype declaration.
1827 * Create sorts parameter with Solver::mkParamSort().
1828 * @param slv the associated solver object
1829 * @param name the name of the datatype
1830 * @param params a list of sort parameters
1831 * @param isCoDatatype true if a codatatype is to be constructed
1833 DatatypeDecl(const Solver
* slv
,
1834 const std::string
& name
,
1835 const std::vector
<Sort
>& params
,
1836 bool isCoDatatype
= false);
1838 /** @return the internal wrapped Dtype of this datatype declaration. */
1839 cvc5::DType
& getDatatype(void) const;
1842 * Helper for isNull checks. This prevents calling an API function with
1843 * CVC5_API_CHECK_NOT_NULL
1845 bool isNullHelper() const;
1848 * The associated solver object.
1850 const Solver
* d_solver
;
1853 * The internal (intermediate) datatype wrapped by this datatype
1855 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1858 std::shared_ptr
<cvc5::DType
> d_dtype
;
1862 * A cvc5 datatype selector.
1864 class CVC5_EXPORT DatatypeSelector
1866 friend class Datatype
;
1867 friend class DatatypeConstructor
;
1868 friend class Solver
;
1879 ~DatatypeSelector();
1881 /** @return the name of this Datatype selector. */
1882 std::string
getName() const;
1885 * Get the selector operator of this datatype selector.
1886 * @return the selector term
1888 Term
getSelectorTerm() const;
1891 * Get the updater operator of this datatype selector.
1892 * @return the updater term
1894 Term
getUpdaterTerm() const;
1896 /** @return the range sort of this selector. */
1897 Sort
getRangeSort() const;
1900 * @return true if this DatatypeSelector is a null object
1902 bool isNull() const;
1905 * @return a string representation of this datatype selector
1907 std::string
toString() const;
1912 * @param slv the associated solver object
1913 * @param stor the internal datatype selector to be wrapped
1914 * @return the DatatypeSelector
1916 DatatypeSelector(const Solver
* slv
, const cvc5::DTypeSelector
& stor
);
1919 * Helper for isNull checks. This prevents calling an API function with
1920 * CVC5_API_CHECK_NOT_NULL
1922 bool isNullHelper() const;
1925 * The associated solver object.
1927 const Solver
* d_solver
;
1930 * The internal datatype selector wrapped by this datatype selector.
1931 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1934 std::shared_ptr
<cvc5::DTypeSelector
> d_stor
;
1938 * A cvc5 datatype constructor.
1940 class CVC5_EXPORT DatatypeConstructor
1942 friend class Datatype
;
1943 friend class Solver
;
1949 DatatypeConstructor();
1954 ~DatatypeConstructor();
1956 /** @return the name of this Datatype constructor. */
1957 std::string
getName() const;
1960 * Get the constructor operator of this datatype constructor.
1961 * @return the constructor term
1963 Term
getConstructorTerm() const;
1966 * Get the constructor operator of this datatype constructor whose return
1967 * type is retSort. This method is intended to be used on constructors of
1968 * parametric datatypes and can be seen as returning the constructor
1969 * term that has been explicitly cast to the given sort.
1971 * This method is required for constructors of parametric datatypes whose
1972 * return type cannot be determined by type inference. For example, given:
1973 * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
1974 * The type of nil terms need to be provided by the user. In SMT version 2.6,
1975 * this is done via the syntax for qualified identifiers:
1976 * (as nil (List Int))
1977 * This method is equivalent of applying the above, where this
1978 * DatatypeConstructor is the one corresponding to nil, and retSort is
1981 * Furthermore note that the returned constructor term t is an operator,
1982 * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
1983 * (nullary) application of nil.
1985 * @param retSort the desired return sort of the constructor
1986 * @return the constructor term
1988 Term
getSpecializedConstructorTerm(const Sort
& retSort
) const;
1991 * Get the tester operator of this datatype constructor.
1992 * @return the tester operator
1994 Term
getTesterTerm() const;
1997 * @return the number of selectors (so far) of this Datatype constructor.
1999 size_t getNumSelectors() const;
2001 /** @return the i^th DatatypeSelector. */
2002 DatatypeSelector
operator[](size_t index
) const;
2004 * Get the datatype selector with the given name.
2005 * This is a linear search through the selectors, so in case of
2006 * multiple, similarly-named selectors, the first is returned.
2007 * @param name the name of the datatype selector
2008 * @return the first datatype selector with the given name
2010 DatatypeSelector
operator[](const std::string
& name
) const;
2011 DatatypeSelector
getSelector(const std::string
& name
) const;
2014 * Get the term representation of the datatype selector with the given name.
2015 * This is a linear search through the arguments, so in case of multiple,
2016 * similarly-named arguments, the selector for the first is returned.
2017 * @param name the name of the datatype selector
2018 * @return a term representing the datatype selector with the given name
2020 Term
getSelectorTerm(const std::string
& name
) const;
2023 * @return true if this DatatypeConstructor is a null object
2025 bool isNull() const;
2028 * @return a string representation of this datatype constructor
2030 std::string
toString() const;
2033 * Iterator for the selectors of a datatype constructor.
2035 class const_iterator
2037 friend class DatatypeConstructor
; // to access constructor
2040 /* The following types are required by trait std::iterator_traits */
2043 using iterator_category
= std::forward_iterator_tag
;
2045 /** The type of the item */
2046 using value_type
= DatatypeConstructor
;
2048 /** The pointer type of the item */
2049 using pointer
= const DatatypeConstructor
*;
2051 /** The reference type of the item */
2052 using reference
= const DatatypeConstructor
&;
2054 /** The type returned when two iterators are subtracted */
2055 using difference_type
= std::ptrdiff_t;
2057 /* End of std::iterator_traits required types */
2059 /** Nullary constructor (required for Cython). */
2063 * Assignment operator.
2064 * @param it the iterator to assign to
2065 * @return the reference to the iterator after assignment
2067 const_iterator
& operator=(const const_iterator
& it
);
2070 * Equality operator.
2071 * @param it the iterator to compare to for equality
2072 * @return true if the iterators are equal
2074 bool operator==(const const_iterator
& it
) const;
2077 * Disequality operator.
2078 * @param it the iterator to compare to for disequality
2079 * @return true if the iterators are disequal
2081 bool operator!=(const const_iterator
& it
) const;
2084 * Increment operator (prefix).
2085 * @return a reference to the iterator after incrementing by one
2087 const_iterator
& operator++();
2090 * Increment operator (postfix).
2091 * @return a reference to the iterator after incrementing by one
2093 const_iterator
operator++(int);
2096 * Dereference operator.
2097 * @return a reference to the selector this iterator points to
2099 const DatatypeSelector
& operator*() const;
2102 * Dereference operator.
2103 * @return a pointer to the selector this iterator points to
2105 const DatatypeSelector
* operator->() const;
2110 * @param slv the associated Solver object
2111 * @param ctor the internal datatype constructor to iterate over
2112 * @param begin true if this is a begin() iterator
2114 const_iterator(const Solver
* slv
,
2115 const cvc5::DTypeConstructor
& ctor
,
2119 * The associated solver object.
2121 const Solver
* d_solver
;
2124 * A pointer to the list of selectors of the internal datatype
2125 * constructor to iterate over.
2126 * This pointer is maintained for operators == and != only.
2128 const void* d_int_stors
;
2130 /** The list of datatype selector (wrappers) to iterate over. */
2131 std::vector
<DatatypeSelector
> d_stors
;
2133 /** The current index of the iterator. */
2138 * @return an iterator to the first selector of this constructor
2140 const_iterator
begin() const;
2143 * @return an iterator to one-off-the-last selector of this constructor
2145 const_iterator
end() const;
2150 * @param slv the associated solver instance
2151 * @param ctor the internal datatype constructor to be wrapped
2152 * @return the DatatypeConstructor
2154 DatatypeConstructor(const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
);
2157 * Return selector for name.
2158 * @param name The name of selector to find
2159 * @return the selector object for the name
2161 DatatypeSelector
getSelectorForName(const std::string
& name
) const;
2164 * Helper for isNull checks. This prevents calling an API function with
2165 * CVC5_API_CHECK_NOT_NULL
2167 bool isNullHelper() const;
2170 * The associated solver object.
2172 const Solver
* d_solver
;
2175 * The internal datatype constructor wrapped by this datatype constructor.
2176 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
2179 std::shared_ptr
<cvc5::DTypeConstructor
> d_ctor
;
2185 class CVC5_EXPORT Datatype
2187 friend class Solver
;
2200 * Get the datatype constructor at a given index.
2201 * @param idx the index of the datatype constructor to return
2202 * @return the datatype constructor with the given index
2204 DatatypeConstructor
operator[](size_t idx
) const;
2207 * Get the datatype constructor with the given name.
2208 * This is a linear search through the constructors, so in case of multiple,
2209 * similarly-named constructors, the first is returned.
2210 * @param name the name of the datatype constructor
2211 * @return the datatype constructor with the given name
2213 DatatypeConstructor
operator[](const std::string
& name
) const;
2214 DatatypeConstructor
getConstructor(const std::string
& name
) const;
2217 * Get a term representing the datatype constructor with the given name.
2218 * This is a linear search through the constructors, so in case of multiple,
2219 * similarly-named constructors, the
2220 * first is returned.
2222 Term
getConstructorTerm(const std::string
& name
) const;
2225 * Get the datatype constructor with the given name.
2226 * This is a linear search through the constructors and their selectors, so
2227 * in case of multiple, similarly-named selectors, the first is returned.
2228 * @param name the name of the datatype selector
2229 * @return the datatype selector with the given name
2231 DatatypeSelector
getSelector(const std::string
& name
) const;
2233 /** @return the name of this Datatype. */
2234 std::string
getName() const;
2236 /** @return the number of constructors for this Datatype. */
2237 size_t getNumConstructors() const;
2239 /** @return true if this datatype is parametric */
2240 bool isParametric() const;
2242 /** @return true if this datatype corresponds to a co-datatype */
2243 bool isCodatatype() const;
2245 /** @return true if this datatype corresponds to a tuple */
2246 bool isTuple() const;
2248 /** @return true if this datatype corresponds to a record */
2249 bool isRecord() const;
2251 /** @return true if this datatype is finite */
2252 bool isFinite() const;
2255 * Is this datatype well-founded? If this datatype is not a codatatype,
2256 * this returns false if there are no values of this datatype that are of
2259 * @return true if this datatype is well-founded
2261 bool isWellFounded() const;
2264 * Does this datatype have nested recursion? This method returns false if a
2265 * value of this datatype includes a subterm of its type that is nested
2266 * beneath a non-datatype type constructor. For example, a datatype
2267 * T containing a constructor having a selector with range type (Set T) has
2270 * @return true if this datatype has nested recursion
2272 bool hasNestedRecursion() const;
2275 * @return true if this Datatype is a null object
2277 bool isNull() const;
2280 * @return a string representation of this datatype
2282 std::string
toString() const;
2285 * Iterator for the constructors of a datatype.
2287 class const_iterator
2289 friend class Datatype
; // to access constructor
2292 /* The following types are required by trait std::iterator_traits */
2295 using iterator_category
= std::forward_iterator_tag
;
2297 /** The type of the item */
2298 using value_type
= Datatype
;
2300 /** The pointer type of the item */
2301 using pointer
= const Datatype
*;
2303 /** The reference type of the item */
2304 using reference
= const Datatype
&;
2306 /** The type returned when two iterators are subtracted */
2307 using difference_type
= std::ptrdiff_t;
2309 /* End of std::iterator_traits required types */
2311 /** Nullary constructor (required for Cython). */
2315 * Assignment operator.
2316 * @param it the iterator to assign to
2317 * @return the reference to the iterator after assignment
2319 const_iterator
& operator=(const const_iterator
& it
);
2322 * Equality operator.
2323 * @param it the iterator to compare to for equality
2324 * @return true if the iterators are equal
2326 bool operator==(const const_iterator
& it
) const;
2329 * Disequality operator.
2330 * @param it the iterator to compare to for disequality
2331 * @return true if the iterators are disequal
2333 bool operator!=(const const_iterator
& it
) const;
2336 * Increment operator (prefix).
2337 * @return a reference to the iterator after incrementing by one
2339 const_iterator
& operator++();
2342 * Increment operator (postfix).
2343 * @return a reference to the iterator after incrementing by one
2345 const_iterator
operator++(int);
2348 * Dereference operator.
2349 * @return a reference to the constructor this iterator points to
2351 const DatatypeConstructor
& operator*() const;
2354 * Dereference operator.
2355 * @return a pointer to the constructor this iterator points to
2357 const DatatypeConstructor
* operator->() const;
2362 * @param slv the associated Solver object
2363 * @param dtype the internal datatype to iterate over
2364 * @param begin true if this is a begin() iterator
2366 const_iterator(const Solver
* slv
, const cvc5::DType
& dtype
, bool begin
);
2369 * The associated solver object.
2371 const Solver
* d_solver
;
2374 * A pointer to the list of constructors of the internal datatype
2376 * This pointer is maintained for operators == and != only.
2378 const void* d_int_ctors
;
2380 /** The list of datatype constructor (wrappers) to iterate over. */
2381 std::vector
<DatatypeConstructor
> d_ctors
;
2383 /** The current index of the iterator. */
2388 * @return an iterator to the first constructor of this datatype
2390 const_iterator
begin() const;
2393 * @return an iterator to one-off-the-last constructor of this datatype
2395 const_iterator
end() const;
2400 * @param slv the associated solver instance
2401 * @param dtype the internal datatype to be wrapped
2402 * @return the Datatype
2404 Datatype(const Solver
* slv
, const cvc5::DType
& dtype
);
2407 * Return constructor for name.
2408 * @param name The name of constructor to find
2409 * @return the constructor object for the name
2411 DatatypeConstructor
getConstructorForName(const std::string
& name
) const;
2414 * Return selector for name.
2415 * @param name The name of selector to find
2416 * @return the selector object for the name
2418 DatatypeSelector
getSelectorForName(const std::string
& name
) const;
2421 * Helper for isNull checks. This prevents calling an API function with
2422 * CVC5_API_CHECK_NOT_NULL
2424 bool isNullHelper() const;
2427 * The associated solver object.
2429 const Solver
* d_solver
;
2432 * The internal datatype wrapped by this datatype.
2433 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
2436 std::shared_ptr
<cvc5::DType
> d_dtype
;
2440 * Serialize a datatype declaration to given stream.
2441 * @param out the output stream
2442 * @param dtdecl the datatype declaration to be serialized to the given stream
2443 * @return the output stream
2445 std::ostream
& operator<<(std::ostream
& out
,
2446 const DatatypeDecl
& dtdecl
) CVC5_EXPORT
;
2449 * Serialize a datatype constructor declaration to given stream.
2450 * @param out the output stream
2451 * @param ctordecl the datatype constructor declaration to be serialized
2452 * @return the output stream
2454 std::ostream
& operator<<(std::ostream
& out
,
2455 const DatatypeConstructorDecl
& ctordecl
) CVC5_EXPORT
;
2458 * Serialize a vector of datatype constructor declarations to given stream.
2459 * @param out the output stream
2460 * @param vector the vector of datatype constructor declarations to be
2461 * serialized to the given stream
2462 * @return the output stream
2464 std::ostream
& operator<<(std::ostream
& out
,
2465 const std::vector
<DatatypeConstructorDecl
>& vector
)
2469 * Serialize a datatype to given stream.
2470 * @param out the output stream
2471 * @param dtype the datatype to be serialized to given stream
2472 * @return the output stream
2474 std::ostream
& operator<<(std::ostream
& out
, const Datatype
& dtype
) CVC5_EXPORT
;
2477 * Serialize a datatype constructor to given stream.
2478 * @param out the output stream
2479 * @param ctor the datatype constructor to be serialized to given stream
2480 * @return the output stream
2482 std::ostream
& operator<<(std::ostream
& out
,
2483 const DatatypeConstructor
& ctor
) CVC5_EXPORT
;
2486 * Serialize a datatype selector to given stream.
2487 * @param out the output stream
2488 * @param stor the datatype selector to be serialized to given stream
2489 * @return the output stream
2491 std::ostream
& operator<<(std::ostream
& out
,
2492 const DatatypeSelector
& stor
) CVC5_EXPORT
;
2494 /* -------------------------------------------------------------------------- */
2496 /* -------------------------------------------------------------------------- */
2501 class CVC5_EXPORT Grammar
2503 friend class cvc5::Command
;
2504 friend class Solver
;
2508 * Add \p rule to the set of rules corresponding to \p ntSymbol.
2509 * @param ntSymbol the non-terminal to which the rule is added
2510 * @param rule the rule to add
2512 void addRule(const Term
& ntSymbol
, const Term
& rule
);
2515 * Add \p rules to the set of rules corresponding to \p ntSymbol.
2516 * @param ntSymbol the non-terminal to which the rules are added
2517 * @param rules the rules to add
2519 void addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
);
2522 * Allow \p ntSymbol to be an arbitrary constant.
2523 * @param ntSymbol the non-terminal allowed to be any constant
2525 void addAnyConstant(const Term
& ntSymbol
);
2528 * Allow \p ntSymbol to be any input variable to corresponding
2529 * synth-fun/synth-inv with the same sort as \p ntSymbol.
2530 * @param ntSymbol the non-terminal allowed to be any input variable
2532 void addAnyVariable(const Term
& ntSymbol
);
2535 * @return a string representation of this grammar.
2537 std::string
toString() const;
2540 * Nullary constructor. Needed for the Cython API.
2547 * @param slv the solver that created this grammar
2548 * @param sygusVars the input variables to synth-fun/synth-var
2549 * @param ntSymbols the non-terminals of this grammar
2551 Grammar(const Solver
* slv
,
2552 const std::vector
<Term
>& sygusVars
,
2553 const std::vector
<Term
>& ntSymbols
);
2556 * @return the resolved datatype of the Start symbol of the grammar
2561 * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
2563 * \p ntsToUnres contains a mapping from non-terminal symbols to the
2564 * unresolved sorts they correspond to. This map indicates how the argument
2565 * <term> should be interpreted (instances of symbols from the domain of
2566 * \p ntsToUnres correspond to constructor arguments).
2568 * The sygus operator that is actually added to <dt> corresponds to replacing
2569 * each occurrence of non-terminal symbols from the domain of \p ntsToUnres
2570 * with bound variables via purifySygusGTerm, and binding these variables
2573 * @param dt the non-terminal's datatype to which a constructor is added
2574 * @param term the sygus operator of the constructor
2575 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2577 void addSygusConstructorTerm(
2580 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const;
2583 * Purify SyGuS grammar term.
2585 * This returns a term where all occurrences of non-terminal symbols (those
2586 * in the domain of \p ntsToUnres) are replaced by fresh variables. For
2587 * each variable replaced in this way, we add the fresh variable it is
2588 * replaced with to \p args, and the unresolved sorts corresponding to the
2589 * non-terminal symbol to \p cargs (constructor args). In other words,
2590 * \p args contains the free variables in the term returned by this method
2591 * (which should be bound by a lambda), and \p cargs contains the sorts of
2592 * the arguments of the sygus constructor.
2594 * @param term the term to purify
2595 * @param args the free variables in the term returned by this method
2596 * @param cargs the sorts of the arguments of the sygus constructor
2597 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2598 * @return the purfied term
2600 Term
purifySygusGTerm(const Term
& term
,
2601 std::vector
<Term
>& args
,
2602 std::vector
<Sort
>& cargs
,
2603 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const;
2606 * This adds constructors to \p dt for sygus variables in \p d_sygusVars
2607 * whose sort is argument \p sort. This method should be called when the
2608 * sygus grammar term (Variable sort) is encountered.
2610 * @param dt the non-terminal's datatype to which the constructors are added
2611 * @param sort the sort of the sygus variables to add
2613 void addSygusConstructorVariables(DatatypeDecl
& dt
, const Sort
& sort
) const;
2616 * Check if \p rule contains variables that are neither parameters of
2617 * the corresponding synthFun/synthInv nor non-terminals.
2618 * @param rule the non-terminal allowed to be any constant
2619 * @return true if \p rule contains free variables and false otherwise
2621 bool containsFreeVariables(const Term
& rule
) const;
2623 /** The solver that created this grammar. */
2624 const Solver
* d_solver
;
2625 /** Input variables to the corresponding function/invariant to synthesize.*/
2626 std::vector
<Term
> d_sygusVars
;
2627 /** The non-terminal symbols of this grammar. */
2628 std::vector
<Term
> d_ntSyms
;
2629 /** The mapping from non-terminal symbols to their production terms. */
2630 std::unordered_map
<Term
, std::vector
<Term
>> d_ntsToTerms
;
2631 /** The set of non-terminals that can be arbitrary constants. */
2632 std::unordered_set
<Term
> d_allowConst
;
2633 /** The set of non-terminals that can be sygus variables. */
2634 std::unordered_set
<Term
> d_allowVars
;
2635 /** Did we call resolve() before? */
2640 * Serialize a grammar to given stream.
2641 * @param out the output stream
2642 * @param g the grammar to be serialized to the given output stream
2643 * @return the output stream
2645 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& g
) CVC5_EXPORT
;
2647 /* -------------------------------------------------------------------------- */
2648 /* Rounding Mode for Floating-Points */
2649 /* -------------------------------------------------------------------------- */
2652 * Rounding modes for floating-point numbers.
2654 * For many floating-point operations, infinitely precise results may not be
2655 * representable with the number of available bits. Thus, the results are
2656 * rounded in a certain way to one of the representable floating-point numbers.
2658 * \verbatim embed:rst:leading-asterisk
2659 * These rounding modes directly follow the SMT-LIB theory for floating-point
2660 * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
2661 * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
2668 * Round to the nearest even number.
2669 * If the two nearest floating-point numbers bracketing an unrepresentable
2670 * infinitely precise result are equally near, the one with an even least
2671 * significant digit will be delivered.
2673 ROUND_NEAREST_TIES_TO_EVEN
,
2675 * Round towards positive infinity (+oo).
2676 * The result shall be the format's floating-point number (possibly +oo)
2677 * closest to and no less than the infinitely precise result.
2679 ROUND_TOWARD_POSITIVE
,
2681 * Round towards negative infinity (-oo).
2682 * The result shall be the format's floating-point number (possibly -oo)
2683 * closest to and no less than the infinitely precise result.
2685 ROUND_TOWARD_NEGATIVE
,
2687 * Round towards zero.
2688 * The result shall be the format's floating-point number closest to and no
2689 * greater in magnitude than the infinitely precise result.
2693 * Round to the nearest number away from zero.
2694 * If the two nearest floating-point numbers bracketing an unrepresentable
2695 * infinitely precise result are equally near, the one with larger magnitude
2698 ROUND_NEAREST_TIES_TO_AWAY
,
2701 } // namespace cvc5::api
2706 * Hash function for RoundingModes.
2709 struct CVC5_EXPORT hash
<cvc5::api::RoundingMode
>
2711 size_t operator()(cvc5::api::RoundingMode rm
) const;
2714 namespace cvc5::api
{
2716 /* -------------------------------------------------------------------------- */
2718 /* -------------------------------------------------------------------------- */
2721 * Provides access to options that can not be communicated via the regular
2722 * getOption() or getOptionInfo() methods. This class does not store the options
2723 * itself, but only acts as a wrapper to the solver object. It can thus no
2724 * longer be used after the solver object has been destroyed.
2726 class CVC5_EXPORT DriverOptions
2728 friend class Solver
;
2731 /** Access the solvers input stream */
2732 std::istream
& in() const;
2733 /** Access the solvers error output stream */
2734 std::ostream
& err() const;
2735 /** Access the solvers output stream */
2736 std::ostream
& out() const;
2739 DriverOptions(const Solver
& solver
);
2740 const Solver
& d_solver
;
2744 * Holds some description about a particular option, including its name, its
2745 * aliases, whether the option was explicitly set by the user, and information
2746 * concerning its value. The `valueInfo` member holds any of the following
2748 * - VoidInfo if the option holds no value (or the value has no native type)
2749 * - ValueInfo<T> if the option is of type bool or std::string, holds the
2750 * current value and the default value.
2751 * - NumberInfo<T> if the option is of type int64_t, uint64_t or double, holds
2752 * the current and default value, as well as the minimum and maximum.
2753 * - ModeInfo if the option is a mode option, holds the current and default
2754 * values, as well as a list of valid modes.
2755 * Additionally, this class provides convenience functions to obtain the
2756 * current value of an option in a type-safe manner using boolValue(),
2757 * stringValue(), intValue(), uintValue() and doubleValue(). They assert that
2758 * the option has the respective type and return the current value.
2760 struct CVC5_EXPORT OptionInfo
2762 /** Has no value information */
2764 /** Has the current and the default value */
2765 template <typename T
>
2771 /** Default value, current value, minimum and maximum of a numeric value */
2772 template <typename T
>
2777 std::optional
<T
> minimum
;
2778 std::optional
<T
> maximum
;
2780 /** Default value, current value and choices of a mode option */
2783 std::string defaultValue
;
2784 std::string currentValue
;
2785 std::vector
<std::string
> modes
;
2788 /** The option name */
2790 /** The option name aliases */
2791 std::vector
<std::string
> aliases
;
2792 /** Whether the option was explicitly set by the user */
2794 /** The option value information */
2795 std::variant
<VoidInfo
,
2797 ValueInfo
<std::string
>,
2798 NumberInfo
<int64_t>,
2799 NumberInfo
<uint64_t>,
2803 /** Obtain the current value as a bool. Asserts that valueInfo holds a bool.
2805 bool boolValue() const;
2806 /** Obtain the current value as a string. Asserts that valueInfo holds a
2808 std::string
stringValue() const;
2809 /** Obtain the current value as as int. Asserts that valueInfo holds an int.
2811 int64_t intValue() const;
2812 /** Obtain the current value as a uint. Asserts that valueInfo holds a uint.
2814 uint64_t uintValue() const;
2815 /** Obtain the current value as a double. Asserts that valueInfo holds a
2817 double doubleValue() const;
2821 * Print a `OptionInfo` object to an ``std::ostream``.
2823 std::ostream
& operator<<(std::ostream
& os
, const OptionInfo
& oi
) CVC5_EXPORT
;
2825 /* -------------------------------------------------------------------------- */
2827 /* -------------------------------------------------------------------------- */
2830 * Represents a snapshot of a single statistic value.
2831 * A value can be of type `int64_t`, `double`, `std::string` or a histogram
2832 * (`std::map<std::string, uint64_t>`).
2833 * The value type can be queried (using `isInt()`, `isDouble()`, etc.) and
2834 * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
2835 * It is possible to query whether this statistic is an expert statistic by
2836 * `isExpert()` and whether its value is the default value by `isDefault()`.
2838 class CVC5_EXPORT Stat
2843 friend class Statistics
;
2844 friend std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
);
2845 /** Representation of a histogram: maps names to frequencies. */
2846 using HistogramData
= std::map
<std::string
, uint64_t>;
2847 /** Can only be obtained from a `Statistics` object. */
2849 /** Copy constructor */
2850 Stat(const Stat
& s
);
2853 /** Copy assignment */
2854 Stat
& operator=(const Stat
& s
);
2857 * Is this value intended for experts only?
2858 * @return Whether this is an expert statistic.
2860 bool isExpert() const;
2862 * Does this value hold the default value?
2863 * @return Whether this is a defaulted statistic.
2865 bool isDefault() const;
2868 * Is this value an integer?
2869 * @return Whether the value is an integer.
2873 * Return the integer value.
2874 * @return The integer value.
2876 int64_t getInt() const;
2878 * Is this value a double?
2879 * @return Whether the value is a double.
2881 bool isDouble() const;
2883 * Return the double value.
2884 * @return The double value.
2886 double getDouble() const;
2888 * Is this value a string?
2889 * @return Whether the value is a string.
2891 bool isString() const;
2893 * Return the string value.
2894 * @return The string value.
2896 const std::string
& getString() const;
2898 * Is this value a histogram?
2899 * @return Whether the value is a histogram.
2901 bool isHistogram() const;
2903 * Return the histogram value.
2904 * @return The histogram value.
2906 const HistogramData
& getHistogram() const;
2909 Stat(bool expert
, bool def
, StatData
&& sd
);
2910 /** Whether this statistic is only meant for experts */
2912 /** Whether this statistic has the default value */
2914 std::unique_ptr
<StatData
> d_data
;
2918 * Print a `Stat` object to an ``std::ostream``.
2920 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
) CVC5_EXPORT
;
2923 * Represents a snapshot of the solver statistics.
2924 * Once obtained, an instance of this class is independent of the `Solver`
2925 * object: it will not change when the solvers internal statistics do, it
2926 * will not be invalidated if the solver is destroyed.
2927 * Iterating on this class (via `begin()` and `end()`) shows only public
2928 * statistics that have been changed. By passing appropriate flags to
2929 * `begin()`, statistics that are expert, defaulted, or both, can be
2930 * included as well. A single statistic value is represented as `Stat`.
2932 class CVC5_EXPORT Statistics
2935 friend class Solver
;
2936 /** How the statistics are stored internally. */
2937 using BaseType
= std::map
<std::string
, Stat
>;
2939 /** Custom iterator to hide certain statistics from regular iteration */
2940 class CVC5_EXPORT iterator
2943 friend class Statistics
;
2944 BaseType::const_reference
operator*() const;
2945 BaseType::const_pointer
operator->() const;
2946 iterator
& operator++();
2947 iterator
operator++(int);
2948 iterator
& operator--();
2949 iterator
operator--(int);
2950 bool operator==(const iterator
& rhs
) const;
2951 bool operator!=(const iterator
& rhs
) const;
2954 iterator(BaseType::const_iterator it
,
2955 const BaseType
& base
,
2958 bool isVisible() const;
2959 BaseType::const_iterator d_it
;
2960 const BaseType
* d_base
;
2961 bool d_showExpert
= false;
2962 bool d_showDefault
= false;
2966 * Retrieve the statistic with the given name.
2967 * Asserts that a statistic with the given name actually exists and throws
2968 * a `CVC5ApiRecoverableException` if it does not.
2969 * @param name Name of the statistic.
2970 * @return The statistic with the given name.
2972 const Stat
& get(const std::string
& name
);
2974 * Begin iteration over the statistics values.
2975 * By default, only entries that are public (non-expert) and have been set
2976 * are visible while the others are skipped.
2977 * @param expert If set to true, expert statistics are shown as well.
2978 * @param defaulted If set to true, defaulted statistics are shown as well.
2980 iterator
begin(bool expert
= false, bool defaulted
= false) const;
2981 /** End iteration */
2982 iterator
end() const;
2985 Statistics() = default;
2986 Statistics(const StatisticsRegistry
& reg
);
2987 /** Internal data */
2990 std::ostream
& operator<<(std::ostream
& out
,
2991 const Statistics
& stats
) CVC5_EXPORT
;
2993 /* -------------------------------------------------------------------------- */
2995 /* -------------------------------------------------------------------------- */
3000 class CVC5_EXPORT Solver
3002 friend class Datatype
;
3003 friend class DatatypeDecl
;
3004 friend class DatatypeConstructor
;
3005 friend class DatatypeConstructorDecl
;
3006 friend class DatatypeSelector
;
3007 friend class DriverOptions
;
3008 friend class Grammar
;
3010 friend class cvc5::Command
;
3011 friend class cvc5::main::CommandExecutor
;
3017 * Constructs a solver with the given original options. This should only be
3018 * used internally when the Solver is reset.
3020 Solver(std::unique_ptr
<Options
>&& original
);
3023 /* .................................................................... */
3024 /* Constructors/Destructors */
3025 /* .................................................................... */
3029 * @return the Solver
3039 * Disallow copy/assignment.
3041 Solver(const Solver
&) = delete;
3042 Solver
& operator=(const Solver
&) = delete;
3044 /* .................................................................... */
3045 /* Sorts Handling */
3046 /* .................................................................... */
3051 Sort
getNullSort() const;
3054 * @return sort Boolean
3056 Sort
getBooleanSort() const;
3059 * @return sort Integer (in cvc5, Integer is a subtype of Real)
3061 Sort
getIntegerSort() const;
3066 Sort
getRealSort() const;
3069 * @return sort RegExp
3071 Sort
getRegExpSort() const;
3074 * @return sort RoundingMode
3076 Sort
getRoundingModeSort() const;
3079 * @return sort String
3081 Sort
getStringSort() const;
3084 * Create an array sort.
3085 * @param indexSort the array index sort
3086 * @param elemSort the array element sort
3087 * @return the array sort
3089 Sort
mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const;
3092 * Create a bit-vector sort.
3093 * @param size the bit-width of the bit-vector sort
3094 * @return the bit-vector sort
3096 Sort
mkBitVectorSort(uint32_t size
) const;
3099 * Create a floating-point sort.
3100 * @param exp the bit-width of the exponent of the floating-point sort.
3101 * @param sig the bit-width of the significand of the floating-point sort.
3103 Sort
mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const;
3106 * Create a datatype sort.
3107 * @param dtypedecl the datatype declaration from which the sort is created
3108 * @return the datatype sort
3110 Sort
mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const;
3113 * Create a vector of datatype sorts. The names of the datatype declarations
3116 * @param dtypedecls the datatype declarations from which the sort is created
3117 * @return the datatype sorts
3119 std::vector
<Sort
> mkDatatypeSorts(
3120 const std::vector
<DatatypeDecl
>& dtypedecls
) const;
3123 * Create a vector of datatype sorts using unresolved sorts. The names of
3124 * the datatype declarations in dtypedecls must be distinct.
3126 * This method is called when the DatatypeDecl objects dtypedecls have been
3127 * built using "unresolved" sorts.
3129 * We associate each sort in unresolvedSorts with exactly one datatype from
3130 * dtypedecls. In particular, it must have the same name as exactly one
3131 * datatype declaration in dtypedecls.
3133 * When constructing datatypes, unresolved sorts are replaced by the datatype
3134 * sort constructed for the datatype declaration it is associated with.
3136 * @param dtypedecls the datatype declarations from which the sort is created
3137 * @param unresolvedSorts the list of unresolved sorts
3138 * @return the datatype sorts
3140 std::vector
<Sort
> mkDatatypeSorts(
3141 const std::vector
<DatatypeDecl
>& dtypedecls
,
3142 const std::set
<Sort
>& unresolvedSorts
) const;
3145 * Create function sort.
3146 * @param domain the sort of the function argument
3147 * @param codomain the sort of the function return value
3148 * @return the function sort
3150 Sort
mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const;
3153 * Create function sort.
3154 * @param sorts the sort of the function arguments
3155 * @param codomain the sort of the function return value
3156 * @return the function sort
3158 Sort
mkFunctionSort(const std::vector
<Sort
>& sorts
,
3159 const Sort
& codomain
) const;
3162 * Create a sort parameter.
3163 * @param symbol the name of the sort
3164 * @return the sort parameter
3166 Sort
mkParamSort(const std::string
& symbol
) const;
3169 * Create a predicate sort.
3170 * @param sorts the list of sorts of the predicate
3171 * @return the predicate sort
3173 Sort
mkPredicateSort(const std::vector
<Sort
>& sorts
) const;
3176 * Create a record sort
3177 * @param fields the list of fields of the record
3178 * @return the record sort
3181 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const;
3184 * Create a set sort.
3185 * @param elemSort the sort of the set elements
3186 * @return the set sort
3188 Sort
mkSetSort(const Sort
& elemSort
) const;
3191 * Create a bag sort.
3192 * @param elemSort the sort of the bag elements
3193 * @return the bag sort
3195 Sort
mkBagSort(const Sort
& elemSort
) const;
3198 * Create a sequence sort.
3199 * @param elemSort the sort of the sequence elements
3200 * @return the sequence sort
3202 Sort
mkSequenceSort(const Sort
& elemSort
) const;
3205 * Create an uninterpreted sort.
3206 * @param symbol the name of the sort
3207 * @return the uninterpreted sort
3209 Sort
mkUninterpretedSort(const std::string
& symbol
) const;
3212 * Create a sort constructor sort.
3213 * @param symbol the symbol of the sort
3214 * @param arity the arity of the sort
3215 * @return the sort constructor sort
3217 Sort
mkSortConstructorSort(const std::string
& symbol
, size_t arity
) const;
3220 * Create a tuple sort.
3221 * @param sorts of the elements of the tuple
3222 * @return the tuple sort
3224 Sort
mkTupleSort(const std::vector
<Sort
>& sorts
) const;
3226 /* .................................................................... */
3228 /* .................................................................... */
3231 * Create 0-ary term of given kind.
3232 * @param kind the kind of the term
3235 Term
mkTerm(Kind kind
) const;
3238 * Create a unary term of given kind.
3239 * @param kind the kind of the term
3240 * @param child the child of the term
3243 Term
mkTerm(Kind kind
, const Term
& child
) const;
3246 * Create binary term of given kind.
3247 * @param kind the kind of the term
3248 * @param child1 the first child of the term
3249 * @param child2 the second child of the term
3252 Term
mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const;
3255 * Create ternary term of given kind.
3256 * @param kind the kind of the term
3257 * @param child1 the first child of the term
3258 * @param child2 the second child of the term
3259 * @param child3 the third child of the term
3262 Term
mkTerm(Kind kind
,
3265 const Term
& child3
) const;
3268 * Create n-ary term of given kind.
3269 * @param kind the kind of the term
3270 * @param children the children of the term
3273 Term
mkTerm(Kind kind
, const std::vector
<Term
>& children
) const;
3276 * Create nullary term of given kind from a given operator.
3277 * Create operators with mkOp().
3278 * @param op the operator
3281 Term
mkTerm(const Op
& op
) const;
3284 * Create unary term of given kind from a given operator.
3285 * Create operators with mkOp().
3286 * @param op the operator
3287 * @param child the child of the term
3290 Term
mkTerm(const Op
& op
, const Term
& child
) const;
3293 * Create binary term of given kind from a given operator.
3294 * Create operators with mkOp().
3295 * @param op the operator
3296 * @param child1 the first child of the term
3297 * @param child2 the second child of the term
3300 Term
mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const;
3303 * Create ternary term of given kind from a given operator.
3304 * Create operators with mkOp().
3305 * @param op the operator
3306 * @param child1 the first child of the term
3307 * @param child2 the second child of the term
3308 * @param child3 the third child of the term
3311 Term
mkTerm(const Op
& op
,
3314 const Term
& child3
) const;
3317 * Create n-ary term of given kind from a given operator.
3318 * Create operators with mkOp().
3319 * @param op the operator
3320 * @param children the children of the term
3323 Term
mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const;
3326 * Create a tuple term. Terms are automatically converted if sorts are
3328 * @param sorts The sorts of the elements in the tuple
3329 * @param terms The elements in the tuple
3330 * @return the tuple Term
3332 Term
mkTuple(const std::vector
<Sort
>& sorts
,
3333 const std::vector
<Term
>& terms
) const;
3335 /* .................................................................... */
3336 /* Create Operators */
3337 /* .................................................................... */
3340 * Create an operator for a builtin Kind
3341 * The Kind may not be the Kind for an indexed operator
3342 * (e.g. BITVECTOR_EXTRACT)
3343 * Note: in this case, the Op simply wraps the Kind.
3344 * The Kind can be used in mkTerm directly without
3345 * creating an op first.
3346 * @param kind the kind to wrap
3348 Op
mkOp(Kind kind
) const;
3351 * Create operator of kind:
3352 * - DIVISIBLE (to support arbitrary precision integers)
3353 * See enum Kind for a description of the parameters.
3354 * @param kind the kind of the operator
3355 * @param arg the string argument to this operator
3357 Op
mkOp(Kind kind
, const std::string
& arg
) const;
3360 * Create operator of kind:
3362 * - BITVECTOR_REPEAT
3363 * - BITVECTOR_ZERO_EXTEND
3364 * - BITVECTOR_SIGN_EXTEND
3365 * - BITVECTOR_ROTATE_LEFT
3366 * - BITVECTOR_ROTATE_RIGHT
3367 * - INT_TO_BITVECTOR
3368 * - FLOATINGPOINT_TO_UBV
3369 * - FLOATINGPOINT_TO_UBV_TOTAL
3370 * - FLOATINGPOINT_TO_SBV
3371 * - FLOATINGPOINT_TO_SBV_TOTAL
3373 * See enum Kind for a description of the parameters.
3374 * @param kind the kind of the operator
3375 * @param arg the uint32_t argument to this operator
3377 Op
mkOp(Kind kind
, uint32_t arg
) const;
3380 * Create operator of Kind:
3381 * - BITVECTOR_EXTRACT
3382 * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
3383 * - FLOATINGPOINT_TO_FP_FLOATINGPOINT
3384 * - FLOATINGPOINT_TO_FP_REAL
3385 * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
3386 * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
3387 * - FLOATINGPOINT_TO_FP_GENERIC
3388 * See enum Kind for a description of the parameters.
3389 * @param kind the kind of the operator
3390 * @param arg1 the first uint32_t argument to this operator
3391 * @param arg2 the second uint32_t argument to this operator
3393 Op
mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const;
3396 * Create operator of Kind:
3398 * See enum Kind for a description of the parameters.
3399 * @param kind the kind of the operator
3400 * @param args the arguments (indices) of the operator
3402 Op
mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const;
3404 /* .................................................................... */
3405 /* Create Constants */
3406 /* .................................................................... */
3409 * Create a Boolean true constant.
3410 * @return the true constant
3412 Term
mkTrue() const;
3415 * Create a Boolean false constant.
3416 * @return the false constant
3418 Term
mkFalse() const;
3421 * Create a Boolean constant.
3422 * @return the Boolean constant
3423 * @param val the value of the constant
3425 Term
mkBoolean(bool val
) const;
3428 * Create a constant representing the number Pi.
3429 * @return a constant representing Pi
3433 * Create an integer constant from a string.
3434 * @param s the string representation of the constant, may represent an
3435 * integer (e.g., "123").
3436 * @return a constant of sort Integer assuming 's' represents an integer)
3438 Term
mkInteger(const std::string
& s
) const;
3441 * Create an integer constant from a c++ int.
3442 * @param val the value of the constant
3443 * @return a constant of sort Integer
3445 Term
mkInteger(int64_t val
) const;
3448 * Create a real constant from a string.
3449 * @param s the string representation of the constant, may represent an
3450 * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
3451 * @return a constant of sort Real
3453 Term
mkReal(const std::string
& s
) const;
3456 * Create a real constant from an integer.
3457 * @param val the value of the constant
3458 * @return a constant of sort Integer
3460 Term
mkReal(int64_t val
) const;
3463 * Create a real constant from a rational.
3464 * @param num the value of the numerator
3465 * @param den the value of the denominator
3466 * @return a constant of sort Real
3468 Term
mkReal(int64_t num
, int64_t den
) const;
3471 * Create a regular expression all (re.all) term.
3472 * @return the all term
3474 Term
mkRegexpAll() const;
3477 * Create a regular expression allchar (re.allchar) term.
3478 * @return the allchar term
3480 Term
mkRegexpAllchar() const;
3483 * Create a regular expression none (re.none) term.
3484 * @return the none term
3486 Term
mkRegexpNone() const;
3489 * Create a constant representing an empty set of the given sort.
3490 * @param sort the sort of the set elements.
3491 * @return the empty set constant
3493 Term
mkEmptySet(const Sort
& sort
) const;
3496 * Create a constant representing an empty bag of the given sort.
3497 * @param sort the sort of the bag elements.
3498 * @return the empty bag constant
3500 Term
mkEmptyBag(const Sort
& sort
) const;
3503 * Create a separation logic empty term.
3504 * @return the separation logic empty term
3506 Term
mkSepEmp() const;
3509 * Create a separation logic nil term.
3510 * @param sort the sort of the nil term
3511 * @return the separation logic nil term
3513 Term
mkSepNil(const Sort
& sort
) const;
3516 * Create a String constant from a `std::string` which may contain SMT-LIB
3517 * compatible escape sequences like `\u1234` to encode unicode characters.
3518 * @param s the string this constant represents
3519 * @param useEscSequences determines whether escape sequences in `s` should
3520 * be converted to the corresponding unicode character
3521 * @return the String constant
3523 Term
mkString(const std::string
& s
, bool useEscSequences
= false) const;
3526 * Create a String constant from a `std::wstring`.
3527 * This method does not support escape sequences as `std::wstring` already
3528 * supports unicode characters.
3529 * @param s the string this constant represents
3530 * @return the String constant
3532 Term
mkString(const std::wstring
& s
) const;
3535 * Create an empty sequence of the given element sort.
3536 * @param sort The element sort of the sequence.
3537 * @return the empty sequence with given element sort.
3539 Term
mkEmptySequence(const Sort
& sort
) const;
3542 * Create a universe set of the given sort.
3543 * @param sort the sort of the set elements
3544 * @return the universe set constant
3546 Term
mkUniverseSet(const Sort
& sort
) const;
3549 * Create a bit-vector constant of given size and value.
3551 * Note: The given value must fit into a bit-vector of the given size.
3553 * @param size the bit-width of the bit-vector sort
3554 * @param val the value of the constant
3555 * @return the bit-vector constant
3557 Term
mkBitVector(uint32_t size
, uint64_t val
= 0) const;
3560 * Create a bit-vector constant of a given bit-width from a given string of
3563 * Note: The given value must fit into a bit-vector of the given size.
3565 * @param size the bit-width of the constant
3566 * @param s the string representation of the constant
3567 * @param base the base of the string representation (2, 10, or 16)
3568 * @return the bit-vector constant
3570 Term
mkBitVector(uint32_t size
, const std::string
& s
, uint32_t base
) const;
3573 * Create a constant array with the provided constant value stored at every
3575 * @param sort the sort of the constant array (must be an array sort)
3576 * @param val the constant value to store (must match the sort's element sort)
3577 * @return the constant array term
3579 Term
mkConstArray(const Sort
& sort
, const Term
& val
) const;
3582 * Create a positive infinity floating-point constant.
3583 * @param exp Number of bits in the exponent
3584 * @param sig Number of bits in the significand
3585 * @return the floating-point constant
3587 Term
mkPosInf(uint32_t exp
, uint32_t sig
) const;
3590 * Create a negative infinity floating-point constant.
3591 * @param exp Number of bits in the exponent
3592 * @param sig Number of bits in the significand
3593 * @return the floating-point constant
3595 Term
mkNegInf(uint32_t exp
, uint32_t sig
) const;
3598 * Create a not-a-number (NaN) floating-point constant.
3599 * @param exp Number of bits in the exponent
3600 * @param sig Number of bits in the significand
3601 * @return the floating-point constant
3603 Term
mkNaN(uint32_t exp
, uint32_t sig
) const;
3606 * Create a positive zero (+0.0) floating-point constant.
3607 * @param exp Number of bits in the exponent
3608 * @param sig Number of bits in the significand
3609 * @return the floating-point constant
3611 Term
mkPosZero(uint32_t exp
, uint32_t sig
) const;
3614 * Create a negative zero (-0.0) floating-point constant.
3615 * @param exp Number of bits in the exponent
3616 * @param sig Number of bits in the significand
3617 * @return the floating-point constant
3619 Term
mkNegZero(uint32_t exp
, uint32_t sig
) const;
3622 * Create a roundingmode constant.
3623 * @param rm the floating point rounding mode this constant represents
3625 Term
mkRoundingMode(RoundingMode rm
) const;
3628 * Create uninterpreted constant.
3629 * @param sort Sort of the constant
3630 * @param index Index of the constant
3632 Term
mkUninterpretedConst(const Sort
& sort
, int32_t index
) const;
3635 * Create an abstract value constant.
3636 * The given index needs to be a positive integer in base 10.
3637 * @param index Index of the abstract value
3639 Term
mkAbstractValue(const std::string
& index
) const;
3642 * Create an abstract value constant.
3643 * The given index needs to be positive.
3644 * @param index Index of the abstract value
3646 Term
mkAbstractValue(uint64_t index
) const;
3649 * Create a floating-point constant.
3650 * @param exp Size of the exponent
3651 * @param sig Size of the significand
3652 * @param val Value of the floating-point constant as a bit-vector term
3654 Term
mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const;
3657 * Create a cardinality constraint for an uninterpreted sort.
3658 * @param sort the sort the cardinality constraint is for
3659 * @param upperBound the upper bound on the cardinality of the sort
3660 * @return the cardinality constraint
3662 Term
mkCardinalityConstraint(const Sort
& sort
, uint32_t upperBound
) const;
3664 /* .................................................................... */
3665 /* Create Variables */
3666 /* .................................................................... */
3669 * Create (first-order) constant (0-arity function symbol).
3672 * ( declare-const <symbol> <sort> )
3673 * ( declare-fun <symbol> ( ) <sort> )
3676 * @param sort the sort of the constant
3677 * @param symbol the name of the constant
3678 * @return the first-order constant
3680 Term
mkConst(const Sort
& sort
, const std::string
& symbol
) const;
3682 * Create (first-order) constant (0-arity function symbol), with a default
3685 * @param sort the sort of the constant
3686 * @return the first-order constant
3688 Term
mkConst(const Sort
& sort
) const;
3691 * Create a bound variable to be used in a binder (i.e. a quantifier, a
3692 * lambda, or a witness binder).
3693 * @param sort the sort of the variable
3694 * @param symbol the name of the variable
3695 * @return the variable
3697 Term
mkVar(const Sort
& sort
, const std::string
& symbol
= std::string()) const;
3699 /* .................................................................... */
3700 /* Create datatype constructor declarations */
3701 /* .................................................................... */
3703 DatatypeConstructorDecl
mkDatatypeConstructorDecl(const std::string
& name
);
3705 /* .................................................................... */
3706 /* Create datatype declarations */
3707 /* .................................................................... */
3710 * Create a datatype declaration.
3711 * @param name the name of the datatype
3712 * @param isCoDatatype true if a codatatype is to be constructed
3713 * @return the DatatypeDecl
3715 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3716 bool isCoDatatype
= false);
3719 * Create a datatype declaration.
3720 * Create sorts parameter with Solver::mkParamSort().
3721 * @param name the name of the datatype
3722 * @param param the sort parameter
3723 * @param isCoDatatype true if a codatatype is to be constructed
3724 * @return the DatatypeDecl
3726 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3728 bool isCoDatatype
= false);
3731 * Create a datatype declaration.
3732 * Create sorts parameter with Solver::mkParamSort().
3733 * @param name the name of the datatype
3734 * @param params a list of sort parameters
3735 * @param isCoDatatype true if a codatatype is to be constructed
3736 * @return the DatatypeDecl
3738 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3739 const std::vector
<Sort
>& params
,
3740 bool isCoDatatype
= false);
3742 /* .................................................................... */
3743 /* Formula Handling */
3744 /* .................................................................... */
3747 * Simplify a formula without doing "much" work. Does not involve
3748 * the SAT Engine in the simplification, but uses the current
3749 * definitions, assertions, and the current partial model, if one
3750 * has been constructed. It also involves theory normalization.
3751 * @param t the formula to simplify
3752 * @return the simplified formula
3754 Term
simplify(const Term
& t
);
3762 * @param term the formula to assert
3764 void assertFormula(const Term
& term
) const;
3767 * Check satisfiability.
3772 * @return the result of the satisfiability check.
3774 Result
checkSat() const;
3777 * Check satisfiability assuming the given formula.
3780 * ( check-sat-assuming ( <prop_literal> ) )
3782 * @param assumption the formula to assume
3783 * @return the result of the satisfiability check.
3785 Result
checkSatAssuming(const Term
& assumption
) const;
3788 * Check satisfiability assuming the given formulas.
3791 * ( check-sat-assuming ( <prop_literal>+ ) )
3793 * @param assumptions the formulas to assume
3794 * @return the result of the satisfiability check.
3796 Result
checkSatAssuming(const std::vector
<Term
>& assumptions
) const;
3799 * Check entailment of the given formula w.r.t. the current set of assertions.
3800 * @param term the formula to check entailment for
3801 * @return the result of the entailment check.
3803 Result
checkEntailed(const Term
& term
) const;
3806 * Check entailment of the given set of given formulas w.r.t. the current
3807 * set of assertions.
3808 * @param terms the terms to check entailment for
3809 * @return the result of the entailmentcheck.
3811 Result
checkEntailed(const std::vector
<Term
>& terms
) const;
3814 * Create datatype sort.
3817 * ( declare-datatype <symbol> <datatype_decl> )
3819 * @param symbol the name of the datatype sort
3820 * @param ctors the constructor declarations of the datatype sort
3821 * @return the datatype sort
3823 Sort
declareDatatype(const std::string
& symbol
,
3824 const std::vector
<DatatypeConstructorDecl
>& ctors
) const;
3827 * Declare n-ary function symbol.
3830 * ( declare-fun <symbol> ( <sort>* ) <sort> )
3832 * @param symbol the name of the function
3833 * @param sorts the sorts of the parameters to this function
3834 * @param sort the sort of the return value of this function
3835 * @return the function
3837 Term
declareFun(const std::string
& symbol
,
3838 const std::vector
<Sort
>& sorts
,
3839 const Sort
& sort
) const;
3842 * Declare uninterpreted sort.
3845 * ( declare-sort <symbol> <numeral> )
3847 * @param symbol the name of the sort
3848 * @param arity the arity of the sort
3851 Sort
declareSort(const std::string
& symbol
, uint32_t arity
) const;
3854 * Define n-ary function.
3857 * ( define-fun <function_def> )
3859 * @param symbol the name of the function
3860 * @param bound_vars the parameters to this function
3861 * @param sort the sort of the return value of this function
3862 * @param term the function body
3863 * @param global determines whether this definition is global (i.e. persists
3864 * when popping the context)
3865 * @return the function
3867 Term
defineFun(const std::string
& symbol
,
3868 const std::vector
<Term
>& bound_vars
,
3871 bool global
= false) const;
3874 * Define recursive function.
3877 * ( define-fun-rec <function_def> )
3879 * @param symbol the name of the function
3880 * @param bound_vars the parameters to this function
3881 * @param sort the sort of the return value of this function
3882 * @param term the function body
3883 * @param global determines whether this definition is global (i.e. persists
3884 * when popping the context)
3885 * @return the function
3887 Term
defineFunRec(const std::string
& symbol
,
3888 const std::vector
<Term
>& bound_vars
,
3891 bool global
= false) const;
3894 * Define recursive function.
3897 * ( define-fun-rec <function_def> )
3899 * Create parameter 'fun' with mkConst().
3900 * @param fun the sorted function
3901 * @param bound_vars the parameters to this function
3902 * @param term the function body
3903 * @param global determines whether this definition is global (i.e. persists
3904 * when popping the context)
3905 * @return the function
3907 Term
defineFunRec(const Term
& fun
,
3908 const std::vector
<Term
>& bound_vars
,
3910 bool global
= false) const;
3913 * Define recursive functions.
3916 * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3918 * Create elements of parameter 'funs' with mkConst().
3919 * @param funs the sorted functions
3920 * @param bound_vars the list of parameters to the functions
3921 * @param terms the list of function bodies of the functions
3922 * @param global determines whether this definition is global (i.e. persists
3923 * when popping the context)
3924 * @return the function
3926 void defineFunsRec(const std::vector
<Term
>& funs
,
3927 const std::vector
<std::vector
<Term
>>& bound_vars
,
3928 const std::vector
<Term
>& terms
,
3929 bool global
= false) const;
3932 * Echo a given string to the given output stream.
3935 * ( echo <std::string> )
3937 * @param out the output stream
3938 * @param str the string to echo
3940 void echo(std::ostream
& out
, const std::string
& str
) const;
3943 * Get the list of asserted formulas.
3946 * ( get-assertions )
3948 * @return the list of asserted formulas
3950 std::vector
<Term
> getAssertions() const;
3953 * Get info from the solver.
3954 * SMT-LIB: \verbatim( get-info <info_flag> )\endverbatim
3957 std::string
getInfo(const std::string
& flag
) const;
3960 * Get the value of a given option.
3963 * ( get-option <keyword> )
3965 * @param option the option for which the value is queried
3966 * @return a string representation of the option value
3968 std::string
getOption(const std::string
& option
) const;
3971 * Get all option names that can be used with `setOption`, `getOption` and
3973 * @return all option names
3975 std::vector
<std::string
> getOptionNames() const;
3978 * Get some information about the given option. Check the `OptionInfo` class
3979 * for more details on which information is available.
3980 * @return information about the given option
3982 OptionInfo
getOptionInfo(const std::string
& option
) const;
3985 * Get the driver options, which provide access to options that can not be
3986 * communicated properly via getOption() and getOptionInfo().
3987 * @return a DriverOptions object.
3989 DriverOptions
getDriverOptions() const;
3992 * Get the set of unsat ("failed") assumptions.
3995 * ( get-unsat-assumptions )
3997 * Requires to enable option 'produce-unsat-assumptions'.
3998 * @return the set of unsat assumptions.
4000 std::vector
<Term
> getUnsatAssumptions() const;
4003 * Get the unsatisfiable core.
4006 * ( get-unsat-core )
4008 * Requires to enable option 'produce-unsat-cores'.
4009 * @return a set of terms representing the unsatisfiable core
4011 std::vector
<Term
> getUnsatCore() const;
4014 * Get a difficulty estimate for an asserted formula. This method is
4015 * intended to be called immediately after any response to a checkSat.
4017 * @return a map from (a subset of) the input assertions to a real value that
4018 * is an estimate of how difficult each assertion was to solve. Unmentioned
4019 * assertions can be assumed to have zero difficulty.
4021 std::map
<Term
, Term
> getDifficulty() const;
4024 * Get the refutation proof
4029 * Requires to enable option 'produce-proofs'.
4030 * @return a string representing the proof, according to the value of
4031 * proof-format-mode.
4033 std::string
getProof() const;
4036 * Get the value of the given term in the current model.
4039 * ( get-value ( <term> ) )
4041 * @param term the term for which the value is queried
4042 * @return the value of the given term
4044 Term
getValue(const Term
& term
) const;
4047 * Get the values of the given terms in the current model.
4050 * ( get-value ( <term>+ ) )
4052 * @param terms the terms for which the value is queried
4053 * @return the values of the given terms
4055 std::vector
<Term
> getValue(const std::vector
<Term
>& terms
) const;
4058 * Get the domain elements of uninterpreted sort s in the current model. The
4059 * current model interprets s as the finite sort whose domain elements are
4060 * given in the return value of this method.
4062 * @param s The uninterpreted sort in question
4063 * @return the domain elements of s in the current model
4065 std::vector
<Term
> getModelDomainElements(const Sort
& s
) const;
4068 * This returns false if the model value of free constant v was not essential
4069 * for showing the satisfiability of the last call to checkSat using the
4070 * current model. This method will only return false (for any v) if
4071 * the model-cores option has been set.
4073 * @param v The term in question
4074 * @return true if v is a model core symbol
4076 bool isModelCoreSymbol(const Term
& v
) const;
4084 * Requires to enable option 'produce-models'.
4085 * @param sorts The list of uninterpreted sorts that should be printed in the
4087 * @param vars The list of free constants that should be printed in the
4088 * model. A subset of these may be printed based on isModelCoreSymbol.
4089 * @return a string representing the model.
4091 std::string
getModel(const std::vector
<Sort
>& sorts
,
4092 const std::vector
<Term
>& vars
) const;
4095 * Do quantifier elimination.
4100 * Requires a logic that supports quantifier elimination. Currently, the only
4101 * logics supported by quantifier elimination is LRA and LIA.
4102 * @param q a quantified formula of the form:
4103 * Q x1...xn. P( x1...xn, y1...yn )
4104 * where P( x1...xn, y1...yn ) is a quantifier-free formula
4105 * @return a formula ret such that, given the current set of formulas A
4106 * asserted to this solver:
4107 * - ( A ^ q ) and ( A ^ ret ) are equivalent
4108 * - ret is quantifier-free formula containing only free variables in
4111 Term
getQuantifierElimination(const Term
& q
) const;
4114 * Do partial quantifier elimination, which can be used for incrementally
4115 * computing the result of a quantifier elimination.
4118 * ( get-qe-disjunct <q> )
4120 * Requires a logic that supports quantifier elimination. Currently, the only
4121 * logics supported by quantifier elimination is LRA and LIA.
4122 * @param q a quantified formula of the form:
4123 * Q x1...xn. P( x1...xn, y1...yn )
4124 * where P( x1...xn, y1...yn ) is a quantifier-free formula
4125 * @return a formula ret such that, given the current set of formulas A
4126 * asserted to this solver:
4127 * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
4129 * - ret is quantifier-free formula containing only free variables in
4131 * - If Q is exists, let A^Q_n be the formula
4132 * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
4133 * where for each i=1,...n, formula ret^Q_i is the result of calling
4134 * getQuantifierEliminationDisjunct for q with the set of assertions
4135 * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
4136 * A ^ ret^Q_1 ^ ... ^ ret^Q_n
4137 * where ret^Q_i is the same as above. In either case, we have
4138 * that ret^Q_j will eventually be true or false, for some finite j.
4140 Term
getQuantifierEliminationDisjunct(const Term
& q
) const;
4143 * When using separation logic, this sets the location sort and the
4144 * datatype sort to the given ones. This method should be invoked exactly
4145 * once, before any separation logic constraints are provided.
4146 * @param locSort The location sort of the heap
4147 * @param dataSort The data sort of the heap
4149 void declareSepHeap(const Sort
& locSort
, const Sort
& dataSort
) const;
4152 * When using separation logic, obtain the term for the heap.
4153 * @return The term for the heap
4155 Term
getValueSepHeap() const;
4158 * When using separation logic, obtain the term for nil.
4159 * @return The term for nil
4161 Term
getValueSepNil() const;
4164 * Declare a symbolic pool of terms with the given initial value.
4167 * ( declare-pool <symbol> <sort> ( <term>* ) )
4169 * @param symbol The name of the pool
4170 * @param sort The sort of the elements of the pool.
4171 * @param initValue The initial value of the pool
4173 Term
declarePool(const std::string
& symbol
,
4175 const std::vector
<Term
>& initValue
) const;
4177 * Pop (a) level(s) from the assertion stack.
4182 * @param nscopes the number of levels to pop
4184 void pop(uint32_t nscopes
= 1) const;
4187 * Get an interpolant
4190 * ( get-interpol <conj> )
4192 * Requires to enable option 'produce-interpols'.
4193 * @param conj the conjecture term
4194 * @param output a Term I such that A->I and I->B are valid, where A is the
4195 * current set of assertions and B is given in the input by conj.
4196 * @return true if it gets I successfully, false otherwise.
4198 bool getInterpolant(const Term
& conj
, Term
& output
) const;
4201 * Get an interpolant
4204 * ( get-interpol <conj> <g> )
4206 * Requires to enable option 'produce-interpols'.
4207 * @param conj the conjecture term
4208 * @param grammar the grammar for the interpolant I
4209 * @param output a Term I such that A->I and I->B are valid, where A is the
4210 * current set of assertions and B is given in the input by conj.
4211 * @return true if it gets I successfully, false otherwise.
4213 bool getInterpolant(const Term
& conj
, Grammar
& grammar
, Term
& output
) const;
4219 * ( get-abduct <conj> )
4221 * Requires enabling option 'produce-abducts'
4222 * @param conj the conjecture term
4223 * @param output a term C such that A^C is satisfiable, and A^~B^C is
4224 * unsatisfiable, where A is the current set of assertions and B is
4225 * given in the input by conj
4226 * @return true if it gets C successfully, false otherwise
4228 bool getAbduct(const Term
& conj
, Term
& output
) const;
4234 * ( get-abduct <conj> <g> )
4236 * Requires enabling option 'produce-abducts'
4237 * @param conj the conjecture term
4238 * @param grammar the grammar for the abduct C
4239 * @param output a term C such that A^C is satisfiable, and A^~B^C is
4240 * unsatisfiable, where A is the current set of assertions and B is
4241 * given in the input by conj
4242 * @return true if it gets C successfully, false otherwise
4244 bool getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const;
4247 * Block the current model. Can be called only if immediately preceded by a
4248 * SAT or INVALID query.
4253 * Requires enabling 'produce-models' option and setting 'block-models' option
4254 * to a mode other than "none".
4256 void blockModel() const;
4259 * Block the current model values of (at least) the values in terms. Can be
4260 * called only if immediately preceded by a SAT or NOT_ENTAILED query.
4263 * ( block-model-values ( <terms>+ ) )
4265 * Requires enabling 'produce-models' option and setting 'block-models' option
4266 * to a mode other than "none".
4268 void blockModelValues(const std::vector
<Term
>& terms
) const;
4271 * Print all instantiations made by the quantifiers module.
4272 * @param out the output stream
4274 void printInstantiations(std::ostream
& out
) const;
4277 * Push (a) level(s) to the assertion stack.
4280 * ( push <numeral> )
4282 * @param nscopes the number of levels to push
4284 void push(uint32_t nscopes
= 1) const;
4287 * Remove all assertions.
4290 * ( reset-assertions )
4293 void resetAssertions() const;
4299 * ( set-info <attribute> )
4301 * @param keyword the info flag
4302 * @param value the value of the info flag
4304 void setInfo(const std::string
& keyword
, const std::string
& value
) const;
4310 * ( set-logic <symbol> )
4312 * @param logic the logic to set
4314 void setLogic(const std::string
& logic
) const;
4320 * ( set-option <option> )
4322 * @param option the option name
4323 * @param value the option value
4325 void setOption(const std::string
& option
, const std::string
& value
) const;
4328 * If needed, convert this term to a given sort. Note that the sort of the
4329 * term must be convertible into the target sort. Currently only Int to Real
4330 * conversions are supported.
4332 * @param s the target sort
4333 * @return the term wrapped into a sort conversion if needed
4335 Term
ensureTermSort(const Term
& t
, const Sort
& s
) const;
4338 * Append \p symbol to the current list of universal variables.
4341 * ( declare-var <symbol> <sort> )
4343 * @param sort the sort of the universal variable
4344 * @param symbol the name of the universal variable
4345 * @return the universal variable
4347 Term
mkSygusVar(const Sort
& sort
,
4348 const std::string
& symbol
= std::string()) const;
4351 * Create a Sygus grammar. The first non-terminal is treated as the starting
4352 * non-terminal, so the order of non-terminals matters.
4354 * @param boundVars the parameters to corresponding synth-fun/synth-inv
4355 * @param ntSymbols the pre-declaration of the non-terminal symbols
4356 * @return the grammar
4358 Grammar
mkSygusGrammar(const std::vector
<Term
>& boundVars
,
4359 const std::vector
<Term
>& ntSymbols
) const;
4362 * Synthesize n-ary function.
4365 * ( synth-fun <symbol> ( <boundVars>* ) <sort> )
4367 * @param symbol the name of the function
4368 * @param boundVars the parameters to this function
4369 * @param sort the sort of the return value of this function
4370 * @return the function
4372 Term
synthFun(const std::string
& symbol
,
4373 const std::vector
<Term
>& boundVars
,
4374 const Sort
& sort
) const;
4377 * Synthesize n-ary function following specified syntactic constraints.
4380 * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
4382 * @param symbol the name of the function
4383 * @param boundVars the parameters to this function
4384 * @param sort the sort of the return value of this function
4385 * @param grammar the syntactic constraints
4386 * @return the function
4388 Term
synthFun(const std::string
& symbol
,
4389 const std::vector
<Term
>& boundVars
,
4391 Grammar
& grammar
) const;
4394 * Synthesize invariant.
4397 * ( synth-inv <symbol> ( <boundVars>* ) )
4399 * @param symbol the name of the invariant
4400 * @param boundVars the parameters to this invariant
4401 * @return the invariant
4403 Term
synthInv(const std::string
& symbol
,
4404 const std::vector
<Term
>& boundVars
) const;
4407 * Synthesize invariant following specified syntactic constraints.
4410 * ( synth-inv <symbol> ( <boundVars>* ) <g> )
4412 * @param symbol the name of the invariant
4413 * @param boundVars the parameters to this invariant
4414 * @param grammar the syntactic constraints
4415 * @return the invariant
4417 Term
synthInv(const std::string
& symbol
,
4418 const std::vector
<Term
>& boundVars
,
4419 Grammar
& grammar
) const;
4422 * Add a forumla to the set of Sygus constraints.
4425 * ( constraint <term> )
4427 * @param term the formula to add as a constraint
4429 void addSygusConstraint(const Term
& term
) const;
4432 * Add a forumla to the set of Sygus assumptions.
4437 * @param term the formula to add as an assumption
4439 void addSygusAssume(const Term
& term
) const;
4442 * Add a set of Sygus constraints to the current state that correspond to an
4443 * invariant synthesis problem.
4446 * ( inv-constraint <inv> <pre> <trans> <post> )
4448 * @param inv the function-to-synthesize
4449 * @param pre the pre-condition
4450 * @param trans the transition relation
4451 * @param post the post-condition
4453 void addSygusInvConstraint(Term inv
, Term pre
, Term trans
, Term post
) const;
4456 * Try to find a solution for the synthesis conjecture corresponding to the
4457 * current list of functions-to-synthesize, universal variables and
4463 * @return the result of the synthesis conjecture.
4465 Result
checkSynth() const;
4468 * Get the synthesis solution of the given term. This method should be called
4469 * immediately after the solver answers unsat for sygus input.
4470 * @param term the term for which the synthesis solution is queried
4471 * @return the synthesis solution of the given term
4473 Term
getSynthSolution(Term term
) const;
4476 * Get the synthesis solutions of the given terms. This method should be
4477 * called immediately after the solver answers unsat for sygus input.
4478 * @param terms the terms for which the synthesis solutions is queried
4479 * @return the synthesis solutions of the given terms
4481 std::vector
<Term
> getSynthSolutions(const std::vector
<Term
>& terms
) const;
4484 * Returns a snapshot of the current state of the statistic values of this
4485 * solver. The returned object is completely decoupled from the solver and
4486 * will not change when the solver is used again.
4488 Statistics
getStatistics() const;
4491 * Whether the output stream for the given tag is enabled. Tags can be enabled
4492 * with the `output` option (and `-o <tag>` on the command line). Raises an
4493 * exception when an invalid tag is given.
4495 bool isOutputOn(const std::string
& tag
) const;
4498 * Returns an output stream for the given tag. Tags can be enabled with the
4499 * `output` option (and `-o <tag>` on the command line). Raises an exception
4500 * when an invalid tag is given.
4502 std::ostream
& getOutput(const std::string
& tag
) const;
4505 /** @return the node manager of this solver */
4506 NodeManager
* getNodeManager(void) const;
4507 /** Reset the API statistics */
4508 void resetStatistics();
4511 * Print the statistics to the given file descriptor, suitable for usage in
4514 void printStatisticsSafe(int fd
) const;
4516 /** Helper to check for API misuse in mkOp functions. */
4517 void checkMkTerm(Kind kind
, uint32_t nchildren
) const;
4518 /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
4519 template <typename T
>
4520 Term
mkValHelper(const T
& t
) const;
4521 /** Helper for making rational values. */
4522 Term
mkRationalValHelper(const Rational
& r
) const;
4523 /** Helper for mkReal functions that take a string as argument. */
4524 Term
mkRealFromStrHelper(const std::string
& s
) const;
4525 /** Helper for mkBitVector functions that take a string as argument. */
4526 Term
mkBVFromStrHelper(const std::string
& s
, uint32_t base
) const;
4528 * Helper for mkBitVector functions that take a string and a size as
4531 Term
mkBVFromStrHelper(uint32_t size
,
4532 const std::string
& s
,
4533 uint32_t base
) const;
4534 /** Helper for mkBitVector functions that take an integer as argument. */
4535 Term
mkBVFromIntHelper(uint32_t size
, uint64_t val
) const;
4536 /** Helper for functions that create tuple sorts. */
4537 Sort
mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const;
4538 /** Helper for mkTerm functions that create Term from a Kind */
4539 Term
mkTermFromKind(Kind kind
) const;
4540 /** Helper for mkChar functions that take a string as argument. */
4541 Term
mkCharFromStrHelper(const std::string
& s
) const;
4542 /** Get value helper, which accounts for subtyping */
4543 Term
getValueHelper(const Term
& term
) const;
4546 * Helper function that ensures that a given term is of sort real (as opposed
4547 * to being of sort integer).
4548 * @param t a term of sort integer or real
4549 * @return a term of sort real
4551 Term
ensureRealSort(const Term
& t
) const;
4554 * Create n-ary term of given kind. This handles the cases of left/right
4555 * associative operators, chainable operators, and cases when the number of
4556 * children exceeds the maximum arity for the kind.
4557 * @param kind the kind of the term
4558 * @param children the children of the term
4561 Term
mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const;
4564 * Create n-ary term of given kind from a given operator.
4565 * @param op the operator
4566 * @param children the children of the term
4569 Term
mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const;
4572 * Create a vector of datatype sorts, using unresolved sorts.
4573 * @param dtypedecls the datatype declarations from which the sort is created
4574 * @param unresolvedSorts the list of unresolved sorts
4575 * @return the datatype sorts
4577 std::vector
<Sort
> mkDatatypeSortsInternal(
4578 const std::vector
<DatatypeDecl
>& dtypedecls
,
4579 const std::set
<Sort
>& unresolvedSorts
) const;
4582 * Synthesize n-ary function following specified syntactic constraints.
4585 * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
4587 * @param symbol the name of the function
4588 * @param boundVars the parameters to this function
4589 * @param sort the sort of the return value of this function
4590 * @param isInv determines whether this is synth-fun or synth-inv
4591 * @param grammar the syntactic constraints
4592 * @return the function
4594 Term
synthFunHelper(const std::string
& symbol
,
4595 const std::vector
<Term
>& boundVars
,
4598 Grammar
* grammar
= nullptr) const;
4600 /** Check whether string s is a valid decimal integer. */
4601 bool isValidInteger(const std::string
& s
) const;
4603 /** Increment the term stats counter. */
4604 void increment_term_stats(Kind kind
) const;
4605 /** Increment the vars stats (if 'is_var') or consts stats counter. */
4606 void increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const;
4608 /** Keep a copy of the original option settings (for resets). */
4609 std::unique_ptr
<Options
> d_originalOptions
;
4610 /** The node manager of this solver. */
4611 NodeManager
* d_nodeMgr
;
4612 /** The statistics collected on the Api level. */
4613 std::unique_ptr
<APIStatistics
> d_stats
;
4614 /** The SMT engine of this solver. */
4615 std::unique_ptr
<SolverEngine
> d_slv
;
4616 /** The random number generator of this solver. */
4617 std::unique_ptr
<Random
> d_rng
;
4620 } // namespace cvc5::api