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
26 #include <unordered_map>
27 #include <unordered_set>
30 #include "api/cpp/cvc5_kind.h"
35 template <bool ref_count
>
37 typedef NodeTemplate
<true> Node
;
42 class DTypeConstructor
;
50 class StatisticsRegistry
;
58 /* -------------------------------------------------------------------------- */
60 /* -------------------------------------------------------------------------- */
63 * Base class for all API exceptions.
64 * If thrown, all API objects may be in an unsafe state.
66 class CVC5_EXPORT CVC5ApiException
: public std::exception
70 * Construct with message from a string.
71 * @param str The error message.
73 CVC5ApiException(const std::string
& str
) : d_msg(str
) {}
75 * Construct with message from a string stream.
76 * @param stream The error message.
78 CVC5ApiException(const std::stringstream
& stream
) : d_msg(stream
.str()) {}
80 * Retrieve the message from this exception.
81 * @return The error message.
83 const std::string
& getMessage() const { return d_msg
; }
85 * Retrieve the message as a C-style array.
86 * @return The error message.
88 const char* what() const noexcept override
{ return d_msg
.c_str(); }
91 /** The stored error message. */
96 * A recoverable API exception.
97 * If thrown, API objects can still be used.
99 class CVC5_EXPORT CVC5ApiRecoverableException
: public CVC5ApiException
103 * Construct with message from a string.
104 * @param str The error message.
106 CVC5ApiRecoverableException(const std::string
& str
) : CVC5ApiException(str
) {}
108 * Construct with message from a string stream.
109 * @param stream The error message.
111 CVC5ApiRecoverableException(const std::stringstream
& stream
)
112 : CVC5ApiException(stream
.str())
117 /* -------------------------------------------------------------------------- */
119 /* -------------------------------------------------------------------------- */
122 * Encapsulation of a three-valued solver result, with explanations.
124 class CVC5_EXPORT Result
129 enum UnknownExplanation
147 * Return true if Result is empty, i.e., a nullary Result, and not an actual
148 * result returned from a checkSat() (and friends) query.
153 * Return true if query was a satisfiable checkSat() or checkSatAssuming()
159 * Return true if query was an unsatisfiable checkSat() or
160 * checkSatAssuming() query.
162 bool isUnsat() const;
165 * Return true if query was a checkSat() or checkSatAssuming() query and
166 * cvc5 was not able to determine (un)satisfiability.
168 bool isSatUnknown() const;
171 * Return true if corresponding query was an entailed checkEntailed() query.
173 bool isEntailed() const;
176 * Return true if corresponding query was a checkEntailed() query that is
179 bool isNotEntailed() const;
182 * Return true if query was a checkEntailed() () query and cvc5 was not able
183 * to determine if it is entailed.
185 bool isEntailmentUnknown() const;
188 * Operator overloading for equality of two results.
189 * @param r the result to compare to for equality
190 * @return true if the results are equal
192 bool operator==(const Result
& r
) const;
195 * Operator overloading for disequality of two results.
196 * @param r the result to compare to for disequality
197 * @return true if the results are disequal
199 bool operator!=(const Result
& r
) const;
202 * @return an explanation for an unknown query result.
204 UnknownExplanation
getUnknownExplanation() const;
207 * @return a string representation of this result.
209 std::string
toString() const;
214 * @param r the internal result that is to be wrapped by this result
217 Result(const cvc5::Result
& r
);
220 * The interal result wrapped by this result.
221 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::Result is
224 std::shared_ptr
<cvc5::Result
> d_result
;
228 * Serialize a Result to given stream.
229 * @param out the output stream
230 * @param r the result to be serialized to the given output stream
231 * @return the output stream
233 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
) CVC5_EXPORT
;
236 * Serialize an UnknownExplanation to given stream.
237 * @param out the output stream
238 * @param e the explanation to be serialized to the given output stream
239 * @return the output stream
241 std::ostream
& operator<<(std::ostream
& out
,
242 enum Result::UnknownExplanation e
) CVC5_EXPORT
;
244 /* -------------------------------------------------------------------------- */
246 /* -------------------------------------------------------------------------- */
251 * The sort of a cvc5 term.
253 class CVC5_EXPORT Sort
255 friend class cvc5::Command
;
256 friend class DatatypeConstructor
;
257 friend class DatatypeConstructorDecl
;
258 friend class DatatypeSelector
;
259 friend class DatatypeDecl
;
262 friend class Grammar
;
263 friend struct std::hash
<Sort
>;
278 * Comparison for structural equality.
279 * @param s the sort to compare to
280 * @return true if the sorts are equal
282 bool operator==(const Sort
& s
) const;
285 * Comparison for structural disequality.
286 * @param s the sort to compare to
287 * @return true if the sorts are not equal
289 bool operator!=(const Sort
& s
) const;
292 * Comparison for ordering on sorts.
293 * @param s the sort to compare to
294 * @return true if this sort is less than s
296 bool operator<(const Sort
& s
) const;
299 * Comparison for ordering on sorts.
300 * @param s the sort to compare to
301 * @return true if this sort is greater than s
303 bool operator>(const Sort
& s
) const;
306 * Comparison for ordering on sorts.
307 * @param s the sort to compare to
308 * @return true if this sort is less than or equal to s
310 bool operator<=(const Sort
& s
) const;
313 * Comparison for ordering on sorts.
314 * @param s the sort to compare to
315 * @return true if this sort is greater than or equal to s
317 bool operator>=(const Sort
& s
) const;
320 * @return true if this Sort is a null sort.
325 * Is this a Boolean sort?
326 * @return true if the sort is a Boolean sort
328 bool isBoolean() const;
331 * Is this a integer sort?
332 * @return true if the sort is a integer sort
334 bool isInteger() const;
337 * Is this a real sort?
338 * @return true if the sort is a real sort
343 * Is this a string sort?
344 * @return true if the sort is the string sort
346 bool isString() const;
349 * Is this a regexp sort?
350 * @return true if the sort is the regexp sort
352 bool isRegExp() const;
355 * Is this a rounding mode sort?
356 * @return true if the sort is the rounding mode sort
358 bool isRoundingMode() const;
361 * Is this a bit-vector sort?
362 * @return true if the sort is a bit-vector sort
364 bool isBitVector() const;
367 * Is this a floating-point sort?
368 * @return true if the sort is a floating-point sort
370 bool isFloatingPoint() const;
373 * Is this a datatype sort?
374 * @return true if the sort is a datatype sort
376 bool isDatatype() const;
379 * Is this a parametric datatype sort?
380 * @return true if the sort is a parametric datatype sort
382 bool isParametricDatatype() const;
385 * Is this a constructor sort?
386 * @return true if the sort is a constructor sort
388 bool isConstructor() const;
391 * Is this a selector sort?
392 * @return true if the sort is a selector sort
394 bool isSelector() const;
397 * Is this a tester sort?
398 * @return true if the sort is a tester sort
400 bool isTester() const;
402 * Is this a datatype updater sort?
403 * @return true if the sort is a datatype updater sort
405 bool isUpdater() const;
407 * Is this a function sort?
408 * @return true if the sort is a function sort
410 bool isFunction() const;
413 * Is this a predicate sort?
414 * That is, is this a function sort mapping to Boolean? All predicate
415 * sorts are also function sorts.
416 * @return true if the sort is a predicate sort
418 bool isPredicate() const;
421 * Is this a tuple sort?
422 * @return true if the sort is a tuple sort
424 bool isTuple() const;
427 * Is this a record sort?
428 * @return true if the sort is a record sort
430 bool isRecord() const;
433 * Is this an array sort?
434 * @return true if the sort is a array sort
436 bool isArray() const;
439 * Is this a Set sort?
440 * @return true if the sort is a Set sort
445 * Is this a Bag sort?
446 * @return true if the sort is a Bag sort
451 * Is this a Sequence sort?
452 * @return true if the sort is a Sequence sort
454 bool isSequence() const;
457 * Is this a sort kind?
458 * @return true if this is a sort kind
460 bool isUninterpretedSort() const;
463 * Is this a sort constructor kind?
464 * @return true if this is a sort constructor kind
466 bool isSortConstructor() const;
469 * Is this a first-class sort?
470 * First-class sorts are sorts for which:
471 * (1) we handle equalities between terms of that type, and
472 * (2) they are allowed to be parameters of parametric sorts (e.g. index or
473 * element sorts of arrays).
475 * Examples of sorts that are not first-class include sort constructor sorts
476 * and regular expression sorts.
478 * @return true if this is a first-class sort
480 bool isFirstClass() const;
483 * Is this a function-LIKE sort?
485 * Anything function-like except arrays (e.g., datatype selectors) is
486 * considered a function here. Function-like terms can not be the argument
487 * or return value for any term that is function-like.
488 * This is mainly to avoid higher order.
490 * Note that arrays are explicitly not considered function-like here.
492 * @return true if this is a function-like sort
494 bool isFunctionLike() const;
497 * Is this sort a subsort of the given sort?
498 * @return true if this sort is a subsort of s
500 bool isSubsortOf(const Sort
& s
) const;
503 * Is this sort comparable to the given sort (i.e., do they share
504 * a common ancestor in the subsort tree)?
505 * @return true if this sort is comparable to s
507 bool isComparableTo(const Sort
& s
) const;
510 * @return the underlying datatype of a datatype sort
512 Datatype
getDatatype() const;
515 * Instantiate a parameterized datatype/sort sort.
516 * Create sorts parameter with Solver::mkParamSort().
517 * @param params the list of sort parameters to instantiate with
519 Sort
instantiate(const std::vector
<Sort
>& params
) const;
522 * Substitution of Sorts.
523 * @param sort the subsort to be substituted within this sort.
524 * @param replacement the sort replacing the substituted subsort.
526 Sort
substitute(const Sort
& sort
, const Sort
& replacement
) const;
529 * Simultaneous substitution of Sorts.
530 * @param sorts the subsorts to be substituted within this sort.
531 * @param replacements the sort replacing the substituted subsorts.
533 Sort
substitute(const std::vector
<Sort
>& sorts
,
534 const std::vector
<Sort
>& replacements
) const;
537 * Output a string representation of this sort to a given stream.
538 * @param out the output stream
540 void toStream(std::ostream
& out
) const;
543 * @return a string representation of this sort
545 std::string
toString() const;
547 /* Constructor sort ------------------------------------------------------- */
550 * @return the arity of a constructor sort
552 size_t getConstructorArity() const;
555 * @return the domain sorts of a constructor sort
557 std::vector
<Sort
> getConstructorDomainSorts() const;
560 * @return the codomain sort of a constructor sort
562 Sort
getConstructorCodomainSort() const;
564 /* Selector sort ------------------------------------------------------- */
567 * @return the domain sort of a selector sort
569 Sort
getSelectorDomainSort() const;
572 * @return the codomain sort of a selector sort
574 Sort
getSelectorCodomainSort() const;
576 /* Tester sort ------------------------------------------------------- */
579 * @return the domain sort of a tester sort
581 Sort
getTesterDomainSort() const;
584 * @return the codomain sort of a tester sort, which is the Boolean sort
586 Sort
getTesterCodomainSort() const;
588 /* Function sort ------------------------------------------------------- */
591 * @return the arity of a function sort
593 size_t getFunctionArity() const;
596 * @return the domain sorts of a function sort
598 std::vector
<Sort
> getFunctionDomainSorts() const;
601 * @return the codomain sort of a function sort
603 Sort
getFunctionCodomainSort() const;
605 /* Array sort ---------------------------------------------------------- */
608 * @return the array index sort of an array sort
610 Sort
getArrayIndexSort() const;
613 * @return the array element sort of an array element sort
615 Sort
getArrayElementSort() const;
617 /* Set sort ------------------------------------------------------------ */
620 * @return the element sort of a set sort
622 Sort
getSetElementSort() const;
624 /* Bag sort ------------------------------------------------------------ */
627 * @return the element sort of a bag sort
629 Sort
getBagElementSort() const;
631 /* Sequence sort ------------------------------------------------------- */
634 * @return the element sort of a sequence sort
636 Sort
getSequenceElementSort() const;
638 /* Uninterpreted sort -------------------------------------------------- */
641 * @return the name of an uninterpreted sort
643 std::string
getUninterpretedSortName() const;
646 * @return true if an uninterpreted sort is parameterezied
648 bool isUninterpretedSortParameterized() const;
651 * @return the parameter sorts of an uninterpreted sort
653 std::vector
<Sort
> getUninterpretedSortParamSorts() const;
655 /* Sort constructor sort ----------------------------------------------- */
658 * @return the name of a sort constructor sort
660 std::string
getSortConstructorName() const;
663 * @return the arity of a sort constructor sort
665 size_t getSortConstructorArity() const;
667 /* Bit-vector sort ----------------------------------------------------- */
670 * @return the bit-width of the bit-vector sort
672 uint32_t getBVSize() const;
674 /* Floating-point sort ------------------------------------------------- */
677 * @return the bit-width of the exponent of the floating-point sort
679 uint32_t getFPExponentSize() const;
682 * @return the width of the significand of the floating-point sort
684 uint32_t getFPSignificandSize() const;
686 /* Datatype sort ------------------------------------------------------- */
689 * @return the parameter sorts of a datatype sort
691 std::vector
<Sort
> getDatatypeParamSorts() const;
694 * @return the arity of a datatype sort
696 size_t getDatatypeArity() const;
698 /* Tuple sort ---------------------------------------------------------- */
701 * @return the length of a tuple sort
703 size_t getTupleLength() const;
706 * @return the element sorts of a tuple sort
708 std::vector
<Sort
> getTupleSorts() const;
711 /** @return the internal wrapped TypeNode of this sort. */
712 const cvc5::TypeNode
& getTypeNode(void) const;
714 /** Helper to convert a set of Sorts to internal TypeNodes. */
715 std::set
<TypeNode
> static sortSetToTypeNodes(const std::set
<Sort
>& sorts
);
716 /** Helper to convert a vector of Sorts to internal TypeNodes. */
717 std::vector
<TypeNode
> static sortVectorToTypeNodes(
718 const std::vector
<Sort
>& sorts
);
719 /** Helper to convert a vector of internal TypeNodes to Sorts. */
720 std::vector
<Sort
> static typeNodeVectorToSorts(
721 const Solver
* slv
, const std::vector
<TypeNode
>& types
);
725 * @param slv the associated solver object
726 * @param t the internal type that is to be wrapped by this sort
729 Sort(const Solver
* slv
, const cvc5::TypeNode
& t
);
732 * Helper for isNull checks. This prevents calling an API function with
733 * CVC5_API_CHECK_NOT_NULL
735 bool isNullHelper() const;
738 * The associated solver object.
740 const Solver
* d_solver
;
743 * The interal type wrapped by this sort.
744 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
745 * to memory allocation (cvc5::Type is already ref counted, so this
746 * could be a unique_ptr instead).
748 std::shared_ptr
<cvc5::TypeNode
> d_type
;
752 * Serialize a sort to given stream.
753 * @param out the output stream
754 * @param s the sort to be serialized to the given output stream
755 * @return the output stream
757 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
) CVC5_EXPORT
;
765 * Hash function for Sorts.
768 struct CVC5_EXPORT hash
<cvc5::api::Sort
>
770 size_t operator()(const cvc5::api::Sort
& s
) const;
775 namespace cvc5::api
{
777 /* -------------------------------------------------------------------------- */
779 /* -------------------------------------------------------------------------- */
783 * An operator is a term that represents certain operators, instantiated
784 * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
790 friend struct std::hash
<Op
>;
804 * Syntactic equality operator.
805 * Return true if both operators are syntactically identical.
806 * Both operators must belong to the same solver object.
807 * @param t the operator to compare to for equality
808 * @return true if the operators are equal
810 bool operator==(const Op
& t
) const;
813 * Syntactic disequality operator.
814 * Return true if both operators differ syntactically.
815 * Both terms must belong to the same solver object.
816 * @param t the operator to compare to for disequality
817 * @return true if operators are disequal
819 bool operator!=(const Op
& t
) const;
822 * @return the kind of this operator
824 Kind
getKind() const;
827 * @return true if this operator is a null term
832 * @return true iff this operator is indexed
834 bool isIndexed() const;
837 * @return the number of indices of this op
839 size_t getNumIndices() const;
842 * Get the indices used to create this Op.
843 * Supports the following template arguments:
847 * - pair<uint32_t, uint32_t>
848 * Check the Op Kind with getKind() to determine which argument to use.
849 * @return the indices used to create this Op
851 template <typename T
>
852 T
getIndices() const;
855 * @return a string representation of this operator
857 std::string
toString() const;
861 * Constructor for a single kind (non-indexed operator).
862 * @param slv the associated solver object
863 * @param k the kind of this Op
865 Op(const Solver
* slv
, const Kind k
);
869 * @param slv the associated solver object
870 * @param k the kind of this Op
871 * @param n the internal node that is to be wrapped by this term
874 Op(const Solver
* slv
, const Kind k
, const cvc5::Node
& n
);
877 * Helper for isNull checks. This prevents calling an API function with
878 * CVC5_API_CHECK_NOT_NULL
880 bool isNullHelper() const;
883 * Note: An indexed operator has a non-null internal node, d_node
884 * Note 2: We use a helper method to avoid having API functions call
885 * other API functions (we need to call this internally)
886 * @return true iff this Op is indexed
888 bool isIndexedHelper() const;
891 * The associated solver object.
893 const Solver
* d_solver
;
895 /** The kind of this operator. */
899 * The internal node wrapped by this operator.
900 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
901 * to memory allocation (cvc5::Node is already ref counted, so this
902 * could be a unique_ptr instead).
904 std::shared_ptr
<cvc5::Node
> d_node
;
908 * Serialize an operator to given stream.
909 * @param out the output stream
910 * @param t the operator to be serialized to the given output stream
911 * @return the output stream
913 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
) CVC5_EXPORT
;
915 } // namespace cvc5::api
919 * Hash function for Ops.
922 struct CVC5_EXPORT hash
<cvc5::api::Op
>
924 size_t operator()(const cvc5::api::Op
& t
) const;
928 namespace cvc5::api
{
929 /* -------------------------------------------------------------------------- */
931 /* -------------------------------------------------------------------------- */
936 class CVC5_EXPORT Term
938 friend class cvc5::Command
;
939 friend class Datatype
;
940 friend class DatatypeConstructor
;
941 friend class DatatypeSelector
;
943 friend class Grammar
;
944 friend struct std::hash
<Term
>;
958 * Syntactic equality operator.
959 * Return true if both terms are syntactically identical.
960 * Both terms must belong to the same solver object.
961 * @param t the term to compare to for equality
962 * @return true if the terms are equal
964 bool operator==(const Term
& t
) const;
967 * Syntactic disequality operator.
968 * Return true if both terms differ syntactically.
969 * Both terms must belong to the same solver object.
970 * @param t the term to compare to for disequality
971 * @return true if terms are disequal
973 bool operator!=(const Term
& t
) const;
976 * Comparison for ordering on terms.
977 * @param t the term to compare to
978 * @return true if this term is less than t
980 bool operator<(const Term
& t
) const;
983 * Comparison for ordering on terms.
984 * @param t the term to compare to
985 * @return true if this term is greater than t
987 bool operator>(const Term
& t
) const;
990 * Comparison for ordering on terms.
991 * @param t the term to compare to
992 * @return true if this term is less than or equal to t
994 bool operator<=(const Term
& t
) const;
997 * Comparison for ordering on terms.
998 * @param t the term to compare to
999 * @return true if this term is greater than or equal to t
1001 bool operator>=(const Term
& t
) const;
1003 /** @return the number of children of this term */
1004 size_t getNumChildren() const;
1007 * Get the child term at a given index.
1008 * @param index the index of the child term to return
1009 * @return the child term with the given index
1011 Term
operator[](size_t index
) const;
1014 * @return the id of this term
1016 uint64_t getId() const;
1019 * @return the kind of this term
1021 Kind
getKind() const;
1024 * @return the sort of this term
1026 Sort
getSort() const;
1029 * @return the result of replacing 'term' by 'replacement' in this term
1031 Term
substitute(const Term
& term
, const Term
& replacement
) const;
1034 * @return the result of simulatenously replacing 'terms' by 'replacements'
1037 Term
substitute(const std::vector
<Term
>& terms
,
1038 const std::vector
<Term
>& replacements
) const;
1041 * @return true iff this term has an operator
1046 * @return the Op used to create this term
1047 * Note: This is safe to call when hasOp() returns true.
1052 * @return true if this Term is a null term
1054 bool isNull() const;
1057 * Return the base (element stored at all indices) of a constant array
1058 * throws an exception if the kind is not CONST_ARRAY
1059 * @return the base value
1061 Term
getConstArrayBase() const;
1064 * Return the elements of a constant sequence
1065 * throws an exception if the kind is not CONST_SEQUENCE
1066 * @return the elements of the constant sequence.
1068 std::vector
<Term
> getConstSequenceElements() const;
1072 * @return the Boolean negation of this term
1074 Term
notTerm() const;
1078 * @param t a Boolean term
1079 * @return the conjunction of this term and the given term
1081 Term
andTerm(const Term
& t
) const;
1085 * @param t a Boolean term
1086 * @return the disjunction of this term and the given term
1088 Term
orTerm(const Term
& t
) const;
1091 * Boolean exclusive or.
1092 * @param t a Boolean term
1093 * @return the exclusive disjunction of this term and the given term
1095 Term
xorTerm(const Term
& t
) const;
1099 * @param t a Boolean term
1100 * @return the Boolean equivalence of this term and the given term
1102 Term
eqTerm(const Term
& t
) const;
1105 * Boolean implication.
1106 * @param t a Boolean term
1107 * @return the implication of this term and the given term
1109 Term
impTerm(const Term
& t
) const;
1112 * If-then-else with this term as the Boolean condition.
1113 * @param then_t the 'then' term
1114 * @param else_t the 'else' term
1115 * @return the if-then-else term with this term as the Boolean condition
1117 Term
iteTerm(const Term
& then_t
, const Term
& else_t
) const;
1120 * @return a string representation of this term
1122 std::string
toString() const;
1125 * Iterator for the children of a Term.
1126 * Note: This treats uninterpreted functions as Term just like any other term
1127 * for example, the term f(x, y) will have Kind APPLY_UF and three
1128 * children: f, x, and y
1130 class const_iterator
: public std::iterator
<std::input_iterator_tag
, Term
>
1142 * @param slv the associated solver object
1143 * @param e a shared pointer to the node that we're iterating over
1144 * @param p the position of the iterator (e.g. which child it's on)
1146 const_iterator(const Solver
* slv
,
1147 const std::shared_ptr
<cvc5::Node
>& e
,
1153 const_iterator(const const_iterator
& it
);
1156 * Assignment operator.
1157 * @param it the iterator to assign to
1158 * @return the reference to the iterator after assignment
1160 const_iterator
& operator=(const const_iterator
& it
);
1163 * Equality operator.
1164 * @param it the iterator to compare to for equality
1165 * @return true if the iterators are equal
1167 bool operator==(const const_iterator
& it
) const;
1170 * Disequality operator.
1171 * @param it the iterator to compare to for disequality
1172 * @return true if the iterators are disequal
1174 bool operator!=(const const_iterator
& it
) const;
1177 * Increment operator (prefix).
1178 * @return a reference to the iterator after incrementing by one
1180 const_iterator
& operator++();
1183 * Increment operator (postfix).
1184 * @return a reference to the iterator after incrementing by one
1186 const_iterator
operator++(int);
1189 * Dereference operator.
1190 * @return the term this iterator points to
1192 Term
operator*() const;
1196 * The associated solver object.
1198 const Solver
* d_solver
;
1199 /** The original node to be iterated over. */
1200 std::shared_ptr
<cvc5::Node
> d_origNode
;
1201 /** Keeps track of the iteration position. */
1206 * @return an iterator to the first child of this Term
1208 const_iterator
begin() const;
1211 * @return an iterator to one-off-the-last child of this Term
1213 const_iterator
end() const;
1216 * @return true if the term is an integer that fits within std::int32_t.
1218 bool isInt32() const;
1220 * @return the stored integer as a std::int32_t.
1221 * Note: Asserts isInt32().
1223 std::int32_t getInt32() const;
1225 * @return true if the term is an integer that fits within std::uint32_t.
1227 bool isUInt32() const;
1229 * @return the stored integer as a std::uint32_t.
1230 * Note: Asserts isUInt32().
1232 std::uint32_t getUInt32() const;
1234 * @return true if the term is an integer that fits within std::int64_t.
1236 bool isInt64() const;
1238 * @return the stored integer as a std::int64_t.
1239 * Note: Asserts isInt64().
1241 std::int64_t getInt64() const;
1243 * @return true if the term is an integer that fits within std::uint64_t.
1245 bool isUInt64() const;
1247 * @return the stored integer as a std::uint64_t.
1248 * Note: Asserts isUInt64().
1250 std::uint64_t getUInt64() const;
1252 * @return true if the term is an integer.
1254 bool isInteger() const;
1256 * @return the stored integer in (decimal) string representation.
1257 * Note: Asserts isInteger().
1259 std::string
getInteger() const;
1262 * @return true if the term is a string constant.
1264 bool isString() const;
1266 * @return the stored string constant.
1268 * Note: This method is not to be confused with toString() which returns the
1269 * term in some string representation, whatever data it may hold.
1270 * Asserts isString().
1272 std::wstring
getString() const;
1276 * The associated solver object.
1278 const Solver
* d_solver
;
1281 /** Helper to convert a vector of Terms to internal Nodes. */
1282 std::vector
<Node
> static termVectorToNodes(const std::vector
<Term
>& terms
);
1286 * @param slv the associated solver object
1287 * @param n the internal node that is to be wrapped by this term
1290 Term(const Solver
* slv
, const cvc5::Node
& n
);
1292 /** @return the internal wrapped Node of this term. */
1293 const cvc5::Node
& getNode(void) const;
1296 * Helper for isNull checks. This prevents calling an API function with
1297 * CVC5_API_CHECK_NOT_NULL
1299 bool isNullHelper() const;
1302 * Helper function that returns the kind of the term, which takes into
1303 * account special cases of the conversion for internal to external kinds.
1304 * @return the kind of this term
1306 Kind
getKindHelper() const;
1309 * @return true if the current term is a constant integer that is casted into
1310 * real using the operator CAST_TO_REAL, and returns false otherwise
1312 bool isCastedReal() const;
1314 * The internal node wrapped by this term.
1315 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
1316 * to memory allocation (cvc5::Node is already ref counted, so this
1317 * could be a unique_ptr instead).
1319 std::shared_ptr
<cvc5::Node
> d_node
;
1323 * Serialize a term to given stream.
1324 * @param out the output stream
1325 * @param t the term to be serialized to the given output stream
1326 * @return the output stream
1328 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
) CVC5_EXPORT
;
1331 * Serialize a vector of terms to given stream.
1332 * @param out the output stream
1333 * @param vector the vector of terms to be serialized to the given stream
1334 * @return the output stream
1336 std::ostream
& operator<<(std::ostream
& out
,
1337 const std::vector
<Term
>& vector
) CVC5_EXPORT
;
1340 * Serialize a set of terms to the given stream.
1341 * @param out the output stream
1342 * @param set the set of terms to be serialized to the given stream
1343 * @return the output stream
1345 std::ostream
& operator<<(std::ostream
& out
,
1346 const std::set
<Term
>& set
) CVC5_EXPORT
;
1349 * Serialize an unordered_set of terms to the given stream.
1351 * @param out the output stream
1352 * @param unordered_set the set of terms to be serialized to the given stream
1353 * @return the output stream
1355 std::ostream
& operator<<(std::ostream
& out
,
1356 const std::unordered_set
<Term
>& unordered_set
)
1360 * Serialize a map of terms to the given stream.
1362 * @param out the output stream
1363 * @param map the map of terms to be serialized to the given stream
1364 * @return the output stream
1366 template <typename V
>
1367 std::ostream
& operator<<(std::ostream
& out
,
1368 const std::map
<Term
, V
>& map
) CVC5_EXPORT
;
1371 * Serialize an unordered_map of terms to the given stream.
1373 * @param out the output stream
1374 * @param unordered_map the map of terms to be serialized to the given stream
1375 * @return the output stream
1377 template <typename V
>
1378 std::ostream
& operator<<(std::ostream
& out
,
1379 const std::unordered_map
<Term
, V
>& unordered_map
)
1382 } // namespace cvc5::api
1386 * Hash function for Terms.
1389 struct CVC5_EXPORT hash
<cvc5::api::Term
>
1391 size_t operator()(const cvc5::api::Term
& t
) const;
1395 namespace cvc5::api
{
1397 /* -------------------------------------------------------------------------- */
1399 /* -------------------------------------------------------------------------- */
1401 class DatatypeConstructorIterator
;
1402 class DatatypeIterator
;
1405 * A cvc5 datatype constructor declaration.
1407 class CVC5_EXPORT DatatypeConstructorDecl
1409 friend class DatatypeDecl
;
1410 friend class Solver
;
1414 DatatypeConstructorDecl();
1419 ~DatatypeConstructorDecl();
1422 * Add datatype selector declaration.
1423 * @param name the name of the datatype selector declaration to add
1424 * @param sort the range sort of the datatype selector declaration to add
1426 void addSelector(const std::string
& name
, const Sort
& sort
);
1428 * Add datatype selector declaration whose range type is the datatype itself.
1429 * @param name the name of the datatype selector declaration to add
1431 void addSelectorSelf(const std::string
& name
);
1434 * @return true if this DatatypeConstructorDecl is a null declaration.
1436 bool isNull() const;
1439 * @return a string representation of this datatype constructor declaration
1441 std::string
toString() const;
1446 * @param slv the associated solver object
1447 * @param name the name of the datatype constructor
1448 * @return the DatatypeConstructorDecl
1450 DatatypeConstructorDecl(const Solver
* slv
, const std::string
& name
);
1453 * Helper for isNull checks. This prevents calling an API function with
1454 * CVC5_API_CHECK_NOT_NULL
1456 bool isNullHelper() const;
1459 * The associated solver object.
1461 const Solver
* d_solver
;
1464 * The internal (intermediate) datatype constructor wrapped by this
1465 * datatype constructor declaration.
1466 * Note: This is a shared_ptr rather than a unique_ptr since
1467 * cvc5::DTypeConstructor is not ref counted.
1469 std::shared_ptr
<cvc5::DTypeConstructor
> d_ctor
;
1475 * A cvc5 datatype declaration.
1477 class CVC5_EXPORT DatatypeDecl
1479 friend class DatatypeConstructorArg
;
1480 friend class Solver
;
1481 friend class Grammar
;
1493 * Add datatype constructor declaration.
1494 * @param ctor the datatype constructor declaration to add
1496 void addConstructor(const DatatypeConstructorDecl
& ctor
);
1498 /** Get the number of constructors (so far) for this Datatype declaration. */
1499 size_t getNumConstructors() const;
1501 /** Is this Datatype declaration parametric? */
1502 bool isParametric() const;
1505 * @return true if this DatatypeDecl is a null object
1507 bool isNull() const;
1510 * @return a string representation of this datatype declaration
1512 std::string
toString() const;
1514 /** @return the name of this datatype declaration. */
1515 std::string
getName() const;
1520 * @param slv the associated solver object
1521 * @param name the name of the datatype
1522 * @param isCoDatatype true if a codatatype is to be constructed
1523 * @return the DatatypeDecl
1525 DatatypeDecl(const Solver
* slv
,
1526 const std::string
& name
,
1527 bool isCoDatatype
= false);
1530 * Constructor for parameterized datatype declaration.
1531 * Create sorts parameter with Solver::mkParamSort().
1532 * @param slv the associated solver object
1533 * @param name the name of the datatype
1534 * @param param the sort parameter
1535 * @param isCoDatatype true if a codatatype is to be constructed
1537 DatatypeDecl(const Solver
* slv
,
1538 const std::string
& name
,
1540 bool isCoDatatype
= false);
1543 * Constructor for parameterized datatype declaration.
1544 * Create sorts parameter with Solver::mkParamSort().
1545 * @param slv the associated solver object
1546 * @param name the name of the datatype
1547 * @param params a list of sort parameters
1548 * @param isCoDatatype true if a codatatype is to be constructed
1550 DatatypeDecl(const Solver
* slv
,
1551 const std::string
& name
,
1552 const std::vector
<Sort
>& params
,
1553 bool isCoDatatype
= false);
1555 /** @return the internal wrapped Dtype of this datatype declaration. */
1556 cvc5::DType
& getDatatype(void) const;
1559 * Helper for isNull checks. This prevents calling an API function with
1560 * CVC5_API_CHECK_NOT_NULL
1562 bool isNullHelper() const;
1565 * The associated solver object.
1567 const Solver
* d_solver
;
1570 * The internal (intermediate) datatype wrapped by this datatype
1572 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1575 std::shared_ptr
<cvc5::DType
> d_dtype
;
1579 * A cvc5 datatype selector.
1581 class CVC5_EXPORT DatatypeSelector
1583 friend class Datatype
;
1584 friend class DatatypeConstructor
;
1585 friend class Solver
;
1596 ~DatatypeSelector();
1598 /** @return the name of this Datatype selector. */
1599 std::string
getName() const;
1602 * Get the selector operator of this datatype selector.
1603 * @return the selector term
1605 Term
getSelectorTerm() const;
1608 * Get the upater operator of this datatype selector.
1609 * @return the updater term
1611 Term
getUpdaterTerm() const;
1613 /** @return the range sort of this argument. */
1614 Sort
getRangeSort() const;
1617 * @return true if this DatatypeSelector is a null object
1619 bool isNull() const;
1622 * @return a string representation of this datatype selector
1624 std::string
toString() const;
1629 * @param slv the associated solver object
1630 * @param stor the internal datatype selector to be wrapped
1631 * @return the DatatypeSelector
1633 DatatypeSelector(const Solver
* slv
, const cvc5::DTypeSelector
& stor
);
1636 * Helper for isNull checks. This prevents calling an API function with
1637 * CVC5_API_CHECK_NOT_NULL
1639 bool isNullHelper() const;
1642 * The associated solver object.
1644 const Solver
* d_solver
;
1647 * The internal datatype selector wrapped by this datatype selector.
1648 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1651 std::shared_ptr
<cvc5::DTypeSelector
> d_stor
;
1655 * A cvc5 datatype constructor.
1657 class CVC5_EXPORT DatatypeConstructor
1659 friend class Datatype
;
1660 friend class Solver
;
1666 DatatypeConstructor();
1671 ~DatatypeConstructor();
1673 /** @return the name of this Datatype constructor. */
1674 std::string
getName() const;
1677 * Get the constructor operator of this datatype constructor.
1678 * @return the constructor term
1680 Term
getConstructorTerm() const;
1683 * Get the constructor operator of this datatype constructor whose return
1684 * type is retSort. This method is intended to be used on constructors of
1685 * parametric datatypes and can be seen as returning the constructor
1686 * term that has been explicitly cast to the given sort.
1688 * This method is required for constructors of parametric datatypes whose
1689 * return type cannot be determined by type inference. For example, given:
1690 * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
1691 * The type of nil terms need to be provided by the user. In SMT version 2.6,
1692 * this is done via the syntax for qualified identifiers:
1693 * (as nil (List Int))
1694 * This method is equivalent of applying the above, where this
1695 * DatatypeConstructor is the one corresponding to nil, and retSort is
1698 * Furthermore note that the returned constructor term t is an operator,
1699 * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
1700 * (nullary) application of nil.
1702 * @param retSort the desired return sort of the constructor
1703 * @return the constructor term
1705 Term
getSpecializedConstructorTerm(const Sort
& retSort
) const;
1708 * Get the tester operator of this datatype constructor.
1709 * @return the tester operator
1711 Term
getTesterTerm() const;
1714 * @return the number of selectors (so far) of this Datatype constructor.
1716 size_t getNumSelectors() const;
1718 /** @return the i^th DatatypeSelector. */
1719 DatatypeSelector
operator[](size_t index
) const;
1721 * Get the datatype selector with the given name.
1722 * This is a linear search through the selectors, so in case of
1723 * multiple, similarly-named selectors, the first is returned.
1724 * @param name the name of the datatype selector
1725 * @return the first datatype selector with the given name
1727 DatatypeSelector
operator[](const std::string
& name
) const;
1728 DatatypeSelector
getSelector(const std::string
& name
) const;
1731 * Get the term representation of the datatype selector with the given name.
1732 * This is a linear search through the arguments, so in case of multiple,
1733 * similarly-named arguments, the selector for the first is returned.
1734 * @param name the name of the datatype selector
1735 * @return a term representing the datatype selector with the given name
1737 Term
getSelectorTerm(const std::string
& name
) const;
1740 * @return true if this DatatypeConstructor is a null object
1742 bool isNull() const;
1745 * @return a string representation of this datatype constructor
1747 std::string
toString() const;
1750 * Iterator for the selectors of a datatype constructor.
1752 class const_iterator
1753 : public std::iterator
<std::input_iterator_tag
, DatatypeConstructor
>
1755 friend class DatatypeConstructor
; // to access constructor
1758 /** Nullary constructor (required for Cython). */
1762 * Assignment operator.
1763 * @param it the iterator to assign to
1764 * @return the reference to the iterator after assignment
1766 const_iterator
& operator=(const const_iterator
& it
);
1769 * Equality operator.
1770 * @param it the iterator to compare to for equality
1771 * @return true if the iterators are equal
1773 bool operator==(const const_iterator
& it
) const;
1776 * Disequality operator.
1777 * @param it the iterator to compare to for disequality
1778 * @return true if the iterators are disequal
1780 bool operator!=(const const_iterator
& it
) const;
1783 * Increment operator (prefix).
1784 * @return a reference to the iterator after incrementing by one
1786 const_iterator
& operator++();
1789 * Increment operator (postfix).
1790 * @return a reference to the iterator after incrementing by one
1792 const_iterator
operator++(int);
1795 * Dereference operator.
1796 * @return a reference to the selector this iterator points to
1798 const DatatypeSelector
& operator*() const;
1801 * Dereference operator.
1802 * @return a pointer to the selector this iterator points to
1804 const DatatypeSelector
* operator->() const;
1809 * @param slv the associated Solver object
1810 * @param ctor the internal datatype constructor to iterate over
1811 * @param begin true if this is a begin() iterator
1813 const_iterator(const Solver
* slv
,
1814 const cvc5::DTypeConstructor
& ctor
,
1818 * The associated solver object.
1820 const Solver
* d_solver
;
1823 * A pointer to the list of selectors of the internal datatype
1824 * constructor to iterate over.
1825 * This pointer is maintained for operators == and != only.
1827 const void* d_int_stors
;
1829 /** The list of datatype selector (wrappers) to iterate over. */
1830 std::vector
<DatatypeSelector
> d_stors
;
1832 /** The current index of the iterator. */
1837 * @return an iterator to the first selector of this constructor
1839 const_iterator
begin() const;
1842 * @return an iterator to one-off-the-last selector of this constructor
1844 const_iterator
end() const;
1849 * @param slv the associated solver instance
1850 * @param ctor the internal datatype constructor to be wrapped
1851 * @return the DatatypeConstructor
1853 DatatypeConstructor(const Solver
* slv
, const cvc5::DTypeConstructor
& ctor
);
1856 * Return selector for name.
1857 * @param name The name of selector to find
1858 * @return the selector object for the name
1860 DatatypeSelector
getSelectorForName(const std::string
& name
) const;
1863 * Helper for isNull checks. This prevents calling an API function with
1864 * CVC5_API_CHECK_NOT_NULL
1866 bool isNullHelper() const;
1869 * The associated solver object.
1871 const Solver
* d_solver
;
1874 * The internal datatype constructor wrapped by this datatype constructor.
1875 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
1878 std::shared_ptr
<cvc5::DTypeConstructor
> d_ctor
;
1884 class CVC5_EXPORT Datatype
1886 friend class Solver
;
1899 * Get the datatype constructor at a given index.
1900 * @param idx the index of the datatype constructor to return
1901 * @return the datatype constructor with the given index
1903 DatatypeConstructor
operator[](size_t idx
) const;
1906 * Get the datatype constructor with the given name.
1907 * This is a linear search through the constructors, so in case of multiple,
1908 * similarly-named constructors, the first is returned.
1909 * @param name the name of the datatype constructor
1910 * @return the datatype constructor with the given name
1912 DatatypeConstructor
operator[](const std::string
& name
) const;
1913 DatatypeConstructor
getConstructor(const std::string
& name
) const;
1916 * Get a term representing the datatype constructor with the given name.
1917 * This is a linear search through the constructors, so in case of multiple,
1918 * similarly-named constructors, the
1919 * first is returned.
1921 Term
getConstructorTerm(const std::string
& name
) const;
1924 * Get the datatype constructor with the given name.
1925 * This is a linear search through the constructors and their selectors, so
1926 * in case of multiple, similarly-named selectors, the first is returned.
1927 * @param name the name of the datatype selector
1928 * @return the datatype selector with the given name
1930 DatatypeSelector
getSelector(const std::string
& name
) const;
1932 /** @return the name of this Datatype. */
1933 std::string
getName() const;
1935 /** @return the number of constructors for this Datatype. */
1936 size_t getNumConstructors() const;
1938 /** @return true if this datatype is parametric */
1939 bool isParametric() const;
1941 /** @return true if this datatype corresponds to a co-datatype */
1942 bool isCodatatype() const;
1944 /** @return true if this datatype corresponds to a tuple */
1945 bool isTuple() const;
1947 /** @return true if this datatype corresponds to a record */
1948 bool isRecord() const;
1950 /** @return true if this datatype is finite */
1951 bool isFinite() const;
1954 * Is this datatype well-founded? If this datatype is not a codatatype,
1955 * this returns false if there are no values of this datatype that are of
1958 * @return true if this datatype is well-founded
1960 bool isWellFounded() const;
1963 * Does this datatype have nested recursion? This method returns false if a
1964 * value of this datatype includes a subterm of its type that is nested
1965 * beneath a non-datatype type constructor. For example, a datatype
1966 * T containing a constructor having a selector with range type (Set T) has
1969 * @return true if this datatype has nested recursion
1971 bool hasNestedRecursion() const;
1974 * @return true if this Datatype is a null object
1976 bool isNull() const;
1979 * @return a string representation of this datatype
1981 std::string
toString() const;
1984 * Iterator for the constructors of a datatype.
1986 class const_iterator
: public std::iterator
<std::input_iterator_tag
, Datatype
>
1988 friend class Datatype
; // to access constructor
1991 /** Nullary constructor (required for Cython). */
1995 * Assignment operator.
1996 * @param it the iterator to assign to
1997 * @return the reference to the iterator after assignment
1999 const_iterator
& operator=(const const_iterator
& it
);
2002 * Equality operator.
2003 * @param it the iterator to compare to for equality
2004 * @return true if the iterators are equal
2006 bool operator==(const const_iterator
& it
) const;
2009 * Disequality operator.
2010 * @param it the iterator to compare to for disequality
2011 * @return true if the iterators are disequal
2013 bool operator!=(const const_iterator
& it
) const;
2016 * Increment operator (prefix).
2017 * @return a reference to the iterator after incrementing by one
2019 const_iterator
& operator++();
2022 * Increment operator (postfix).
2023 * @return a reference to the iterator after incrementing by one
2025 const_iterator
operator++(int);
2028 * Dereference operator.
2029 * @return a reference to the constructor this iterator points to
2031 const DatatypeConstructor
& operator*() const;
2034 * Dereference operator.
2035 * @return a pointer to the constructor this iterator points to
2037 const DatatypeConstructor
* operator->() const;
2042 * @param slv the associated Solver object
2043 * @param dtype the internal datatype to iterate over
2044 * @param begin true if this is a begin() iterator
2046 const_iterator(const Solver
* slv
, const cvc5::DType
& dtype
, bool begin
);
2049 * The associated solver object.
2051 const Solver
* d_solver
;
2054 * A pointer to the list of constructors of the internal datatype
2056 * This pointer is maintained for operators == and != only.
2058 const void* d_int_ctors
;
2060 /** The list of datatype constructor (wrappers) to iterate over. */
2061 std::vector
<DatatypeConstructor
> d_ctors
;
2063 /** The current index of the iterator. */
2068 * @return an iterator to the first constructor of this datatype
2070 const_iterator
begin() const;
2073 * @return an iterator to one-off-the-last constructor of this datatype
2075 const_iterator
end() const;
2080 * @param slv the associated solver instance
2081 * @param dtype the internal datatype to be wrapped
2082 * @return the Datatype
2084 Datatype(const Solver
* slv
, const cvc5::DType
& dtype
);
2087 * Return constructor for name.
2088 * @param name The name of constructor to find
2089 * @return the constructor object for the name
2091 DatatypeConstructor
getConstructorForName(const std::string
& name
) const;
2094 * Return selector for name.
2095 * @param name The name of selector to find
2096 * @return the selector object for the name
2098 DatatypeSelector
getSelectorForName(const std::string
& name
) const;
2101 * Helper for isNull checks. This prevents calling an API function with
2102 * CVC5_API_CHECK_NOT_NULL
2104 bool isNullHelper() const;
2107 * The associated solver object.
2109 const Solver
* d_solver
;
2112 * The internal datatype wrapped by this datatype.
2113 * Note: This is a shared_ptr rather than a unique_ptr since cvc5::DType is
2116 std::shared_ptr
<cvc5::DType
> d_dtype
;
2120 * Serialize a datatype declaration to given stream.
2121 * @param out the output stream
2122 * @param dtdecl the datatype declaration to be serialized to the given stream
2123 * @return the output stream
2125 std::ostream
& operator<<(std::ostream
& out
,
2126 const DatatypeDecl
& dtdecl
) CVC5_EXPORT
;
2129 * Serialize a datatype constructor declaration to given stream.
2130 * @param out the output stream
2131 * @param ctordecl the datatype constructor declaration to be serialized
2132 * @return the output stream
2134 std::ostream
& operator<<(std::ostream
& out
,
2135 const DatatypeConstructorDecl
& ctordecl
) CVC5_EXPORT
;
2138 * Serialize a vector of datatype constructor declarations to given stream.
2139 * @param out the output stream
2140 * @param vector the vector of datatype constructor declarations to be
2141 * serialized to the given stream
2142 * @return the output stream
2144 std::ostream
& operator<<(std::ostream
& out
,
2145 const std::vector
<DatatypeConstructorDecl
>& vector
)
2149 * Serialize a datatype to given stream.
2150 * @param out the output stream
2151 * @param dtype the datatype to be serialized to given stream
2152 * @return the output stream
2154 std::ostream
& operator<<(std::ostream
& out
, const Datatype
& dtype
) CVC5_EXPORT
;
2157 * Serialize a datatype constructor to given stream.
2158 * @param out the output stream
2159 * @param ctor the datatype constructor to be serialized to given stream
2160 * @return the output stream
2162 std::ostream
& operator<<(std::ostream
& out
,
2163 const DatatypeConstructor
& ctor
) CVC5_EXPORT
;
2166 * Serialize a datatype selector to given stream.
2167 * @param out the output stream
2168 * @param stor the datatype selector to be serialized to given stream
2169 * @return the output stream
2171 std::ostream
& operator<<(std::ostream
& out
,
2172 const DatatypeSelector
& stor
) CVC5_EXPORT
;
2174 /* -------------------------------------------------------------------------- */
2176 /* -------------------------------------------------------------------------- */
2181 class CVC5_EXPORT Grammar
2183 friend class cvc5::Command
;
2184 friend class Solver
;
2188 * Add \p rule to the set of rules corresponding to \p ntSymbol.
2189 * @param ntSymbol the non-terminal to which the rule is added
2190 * @param rule the rule to add
2192 void addRule(const Term
& ntSymbol
, const Term
& rule
);
2195 * Add \p rules to the set of rules corresponding to \p ntSymbol.
2196 * @param ntSymbol the non-terminal to which the rules are added
2197 * @param rules the rules to add
2199 void addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
);
2202 * Allow \p ntSymbol to be an arbitrary constant.
2203 * @param ntSymbol the non-terminal allowed to be any constant
2205 void addAnyConstant(const Term
& ntSymbol
);
2208 * Allow \p ntSymbol to be any input variable to corresponding
2209 * synth-fun/synth-inv with the same sort as \p ntSymbol.
2210 * @param ntSymbol the non-terminal allowed to be any input constant
2212 void addAnyVariable(const Term
& ntSymbol
);
2215 * @return a string representation of this grammar.
2217 std::string
toString() const;
2220 * Nullary constructor. Needed for the Cython API.
2227 * @param slv the solver that created this grammar
2228 * @param sygusVars the input variables to synth-fun/synth-var
2229 * @param ntSymbols the non-terminals of this grammar
2231 Grammar(const Solver
* slv
,
2232 const std::vector
<Term
>& sygusVars
,
2233 const std::vector
<Term
>& ntSymbols
);
2236 * @return the resolved datatype of the Start symbol of the grammar
2241 * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
2243 * \p ntsToUnres contains a mapping from non-terminal symbols to the
2244 * unresolved sorts they correspond to. This map indicates how the argument
2245 * <term> should be interpreted (instances of symbols from the domain of
2246 * \p ntsToUnres correspond to constructor arguments).
2248 * The sygus operator that is actually added to <dt> corresponds to replacing
2249 * each occurrence of non-terminal symbols from the domain of \p ntsToUnres
2250 * with bound variables via purifySygusGTerm, and binding these variables
2253 * @param dt the non-terminal's datatype to which a constructor is added
2254 * @param term the sygus operator of the constructor
2255 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2257 void addSygusConstructorTerm(
2260 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const;
2263 * Purify SyGuS grammar term.
2265 * This returns a term where all occurrences of non-terminal symbols (those
2266 * in the domain of \p ntsToUnres) are replaced by fresh variables. For
2267 * each variable replaced in this way, we add the fresh variable it is
2268 * replaced with to \p args, and the unresolved sorts corresponding to the
2269 * non-terminal symbol to \p cargs (constructor args). In other words,
2270 * \p args contains the free variables in the term returned by this method
2271 * (which should be bound by a lambda), and \p cargs contains the sorts of
2272 * the arguments of the sygus constructor.
2274 * @param term the term to purify
2275 * @param args the free variables in the term returned by this method
2276 * @param cargs the sorts of the arguments of the sygus constructor
2277 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2278 * @return the purfied term
2280 Term
purifySygusGTerm(const Term
& term
,
2281 std::vector
<Term
>& args
,
2282 std::vector
<Sort
>& cargs
,
2283 const std::unordered_map
<Term
, Sort
>& ntsToUnres
) const;
2286 * This adds constructors to \p dt for sygus variables in \p d_sygusVars
2287 * whose sort is argument \p sort. This method should be called when the
2288 * sygus grammar term (Variable sort) is encountered.
2290 * @param dt the non-terminal's datatype to which the constructors are added
2291 * @param sort the sort of the sygus variables to add
2293 void addSygusConstructorVariables(DatatypeDecl
& dt
, const Sort
& sort
) const;
2296 * Check if \p rule contains variables that are neither parameters of
2297 * the corresponding synthFun/synthInv nor non-terminals.
2298 * @param rule the non-terminal allowed to be any constant
2299 * @return true if \p rule contains free variables and false otherwise
2301 bool containsFreeVariables(const Term
& rule
) const;
2303 /** The solver that created this grammar. */
2304 const Solver
* d_solver
;
2305 /** Input variables to the corresponding function/invariant to synthesize.*/
2306 std::vector
<Term
> d_sygusVars
;
2307 /** The non-terminal symbols of this grammar. */
2308 std::vector
<Term
> d_ntSyms
;
2309 /** The mapping from non-terminal symbols to their production terms. */
2310 std::unordered_map
<Term
, std::vector
<Term
>> d_ntsToTerms
;
2311 /** The set of non-terminals that can be arbitrary constants. */
2312 std::unordered_set
<Term
> d_allowConst
;
2313 /** The set of non-terminals that can be sygus variables. */
2314 std::unordered_set
<Term
> d_allowVars
;
2315 /** Did we call resolve() before? */
2320 * Serialize a grammar to given stream.
2321 * @param out the output stream
2322 * @param g the grammar to be serialized to the given output stream
2323 * @return the output stream
2325 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& g
) CVC5_EXPORT
;
2327 /* -------------------------------------------------------------------------- */
2328 /* Rounding Mode for Floating-Points */
2329 /* -------------------------------------------------------------------------- */
2332 * Rounding modes for floating-point numbers.
2334 * For many floating-point operations, infinitely precise results may not be
2335 * representable with the number of available bits. Thus, the results are
2336 * rounded in a certain way to one of the representable floating-point numbers.
2338 * \verbatim embed:rst:leading-asterisk
2339 * These rounding modes directly follow the SMT-LIB theory for floating-point
2340 * arithmetic, which in turn is based on IEEE Standard 754 :cite:`IEEE754`.
2341 * The rounding modes are specified in Sections 4.3.1 and 4.3.2 of the IEEE
2345 enum CVC5_EXPORT RoundingMode
2348 * Round to the nearest even number.
2349 * If the two nearest floating-point numbers bracketing an unrepresentable
2350 * infinitely precise result are equally near, the one with an even least
2351 * significant digit will be delivered.
2353 ROUND_NEAREST_TIES_TO_EVEN
,
2355 * Round towards positive infinity (+oo).
2356 * The result shall be the format’s floating-point number (possibly +oo)
2357 * closest to and no less than the infinitely precise result.
2359 ROUND_TOWARD_POSITIVE
,
2361 * Round towards negative infinity (-oo).
2362 * The result shall be the format’s floating-point number (possibly -oo)
2363 * closest to and no less than the infinitely precise result.
2365 ROUND_TOWARD_NEGATIVE
,
2367 * Round towards zero.
2368 * The result shall be the format’s floating-point number closest to and no
2369 * greater in magnitude than the infinitely precise result.
2373 * Round to the nearest number away from zero.
2374 * If the two nearest floating-point numbers bracketing an unrepresentable
2375 * infinitely precise result are equally near, the one with larger magnitude
2378 ROUND_NEAREST_TIES_TO_AWAY
,
2381 } // namespace cvc5::api
2386 * Hash function for RoundingModes.
2389 struct CVC5_EXPORT hash
<cvc5::api::RoundingMode
>
2391 size_t operator()(cvc5::api::RoundingMode rm
) const;
2394 namespace cvc5::api
{
2396 /* -------------------------------------------------------------------------- */
2398 /* -------------------------------------------------------------------------- */
2401 * Represents a snapshot of a single statistic value.
2402 * A value can be of type `int64_t`, `double`, `std::string` or a histogram
2403 * (`std::map<std::string, uint64_t>`).
2404 * The value type can be queried (using `isInt()`, `isDouble()`, etc.) and
2405 * the stored value can be accessed (using `getInt()`, `getDouble()`, etc.).
2406 * It is possible to query whether this statistic is an expert statistic by
2407 * `isExpert()` and whether its value is the default value by `isDefault()`.
2409 class CVC5_EXPORT Stat
2414 friend class Statistics
;
2415 friend std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
);
2416 /** Representation of a histogram: maps names to frequencies. */
2417 using HistogramData
= std::map
<std::string
, uint64_t>;
2418 /** Can only be obtained from a `Statistics` object. */
2420 /** Copy constructor */
2421 Stat(const Stat
& s
);
2424 /** Copy assignment */
2425 Stat
& operator=(const Stat
& s
);
2428 * Is this value intended for experts only?
2429 * @return Whether this is an expert statistic.
2431 bool isExpert() const;
2433 * Does this value hold the default value?
2434 * @return Whether this is a defaulted statistic.
2436 bool isDefault() const;
2439 * Is this value an integer?
2440 * @return Whether the value is an integer.
2444 * Return the integer value.
2445 * @return The integer value.
2447 int64_t getInt() const;
2449 * Is this value a double?
2450 * @return Whether the value is a double.
2452 bool isDouble() const;
2454 * Return the double value.
2455 * @return The double value.
2457 double getDouble() const;
2459 * Is this value a string?
2460 * @return Whether the value is a string.
2462 bool isString() const;
2464 * Return the string value.
2465 * @return The string value.
2467 const std::string
& getString() const;
2469 * Is this value a histogram?
2470 * @return Whether the value is a histogram.
2472 bool isHistogram() const;
2474 * Return the histogram value.
2475 * @return The histogram value.
2477 const HistogramData
& getHistogram() const;
2480 Stat(bool expert
, bool def
, StatData
&& sd
);
2481 /** Whether this statistic is only meant for experts */
2483 /** Whether this statistic has the default value */
2485 std::unique_ptr
<StatData
> d_data
;
2489 * Print a `Stat` object to an ``std::ostream``.
2491 std::ostream
& operator<<(std::ostream
& os
, const Stat
& sv
) CVC5_EXPORT
;
2494 * Represents a snapshot of the solver statistics.
2495 * Once obtained, an instance of this class is independent of the `Solver`
2496 * object: it will not change when the solvers internal statistics do, it
2497 * will not be invalidated if the solver is destroyed.
2498 * Iterating on this class (via `begin()` and `end()`) shows only public
2499 * statistics that have been changed. By passing appropriate flags to
2500 * `begin()`, statistics that are expert, defaulted, or both, can be
2501 * included as well. A single statistic value is represented as `Stat`.
2503 class CVC5_EXPORT Statistics
2506 friend class Solver
;
2507 /** How the statistics are stored internally. */
2508 using BaseType
= std::map
<std::string
, Stat
>;
2510 /** Custom iterator to hide certain statistics from regular iteration */
2514 friend class Statistics
;
2515 BaseType::const_reference
operator*() const;
2516 BaseType::const_pointer
operator->() const;
2517 iterator
& operator++();
2518 iterator
operator++(int);
2519 iterator
& operator--();
2520 iterator
operator--(int);
2521 bool operator==(const iterator
& rhs
) const;
2522 bool operator!=(const iterator
& rhs
) const;
2525 iterator(BaseType::const_iterator it
,
2526 const BaseType
& base
,
2529 bool isVisible() const;
2530 BaseType::const_iterator d_it
;
2531 const BaseType
* d_base
;
2532 bool d_showExpert
= false;
2533 bool d_showDefault
= false;
2537 * Retrieve the statistic with the given name.
2538 * Asserts that a statistic with the given name actually exists and throws
2539 * a `CVC4ApiRecoverableException` if it does not.
2540 * @param name Name of the statistic.
2541 * @return The statistic with the given name.
2543 const Stat
& get(const std::string
& name
);
2545 * Begin iteration over the statistics values.
2546 * By default, only entries that are public (non-expert) and have been set
2547 * are visible while the others are skipped.
2548 * @param expert If set to true, expert statistics are shown as well.
2549 * @param defaulted If set to true, defaulted statistics are shown as well.
2551 iterator
begin(bool expert
= false, bool defaulted
= false) const;
2552 /** End iteration */
2553 iterator
end() const;
2556 Statistics() = default;
2557 Statistics(const StatisticsRegistry
& reg
);
2558 /** Internal data */
2561 std::ostream
& operator<<(std::ostream
& out
,
2562 const Statistics
& stats
) CVC5_EXPORT
;
2564 /* -------------------------------------------------------------------------- */
2566 /* -------------------------------------------------------------------------- */
2571 class CVC5_EXPORT Solver
2573 friend class Datatype
;
2574 friend class DatatypeDecl
;
2575 friend class DatatypeConstructor
;
2576 friend class DatatypeConstructorDecl
;
2577 friend class DatatypeSelector
;
2578 friend class Grammar
;
2580 friend class cvc5::Command
;
2585 /* .................................................................... */
2586 /* Constructors/Destructors */
2587 /* .................................................................... */
2591 * @param opts an optional pointer to a solver options object
2592 * @return the Solver
2594 Solver(Options
* opts
= nullptr);
2602 * Disallow copy/assignment.
2604 Solver(const Solver
&) = delete;
2605 Solver
& operator=(const Solver
&) = delete;
2607 /* .................................................................... */
2608 /* Solver Configuration */
2609 /* .................................................................... */
2611 bool supportsFloatingPoint() const;
2613 /* .................................................................... */
2614 /* Sorts Handling */
2615 /* .................................................................... */
2620 Sort
getNullSort() const;
2623 * @return sort Boolean
2625 Sort
getBooleanSort() const;
2628 * @return sort Integer (in cvc5, Integer is a subtype of Real)
2630 Sort
getIntegerSort() const;
2635 Sort
getRealSort() const;
2638 * @return sort RegExp
2640 Sort
getRegExpSort() const;
2643 * @return sort RoundingMode
2645 Sort
getRoundingModeSort() const;
2648 * @return sort String
2650 Sort
getStringSort() const;
2653 * Create an array sort.
2654 * @param indexSort the array index sort
2655 * @param elemSort the array element sort
2656 * @return the array sort
2658 Sort
mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const;
2661 * Create a bit-vector sort.
2662 * @param size the bit-width of the bit-vector sort
2663 * @return the bit-vector sort
2665 Sort
mkBitVectorSort(uint32_t size
) const;
2668 * Create a floating-point sort.
2669 * @param exp the bit-width of the exponent of the floating-point sort.
2670 * @param sig the bit-width of the significand of the floating-point sort.
2672 Sort
mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const;
2675 * Create a datatype sort.
2676 * @param dtypedecl the datatype declaration from which the sort is created
2677 * @return the datatype sort
2679 Sort
mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const;
2682 * Create a vector of datatype sorts. The names of the datatype declarations
2685 * @param dtypedecls the datatype declarations from which the sort is created
2686 * @return the datatype sorts
2688 std::vector
<Sort
> mkDatatypeSorts(
2689 const std::vector
<DatatypeDecl
>& dtypedecls
) const;
2692 * Create a vector of datatype sorts using unresolved sorts. The names of
2693 * the datatype declarations in dtypedecls must be distinct.
2695 * This method is called when the DatatypeDecl objects dtypedecls have been
2696 * built using "unresolved" sorts.
2698 * We associate each sort in unresolvedSorts with exacly one datatype from
2699 * dtypedecls. In particular, it must have the same name as exactly one
2700 * datatype declaration in dtypedecls.
2702 * When constructing datatypes, unresolved sorts are replaced by the datatype
2703 * sort constructed for the datatype declaration it is associated with.
2705 * @param dtypedecls the datatype declarations from which the sort is created
2706 * @param unresolvedSorts the list of unresolved sorts
2707 * @return the datatype sorts
2709 std::vector
<Sort
> mkDatatypeSorts(
2710 const std::vector
<DatatypeDecl
>& dtypedecls
,
2711 const std::set
<Sort
>& unresolvedSorts
) const;
2714 * Create function sort.
2715 * @param domain the sort of the fuction argument
2716 * @param codomain the sort of the function return value
2717 * @return the function sort
2719 Sort
mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const;
2722 * Create function sort.
2723 * @param sorts the sort of the function arguments
2724 * @param codomain the sort of the function return value
2725 * @return the function sort
2727 Sort
mkFunctionSort(const std::vector
<Sort
>& sorts
,
2728 const Sort
& codomain
) const;
2731 * Create a sort parameter.
2732 * @param symbol the name of the sort
2733 * @return the sort parameter
2735 Sort
mkParamSort(const std::string
& symbol
) const;
2738 * Create a predicate sort.
2739 * @param sorts the list of sorts of the predicate
2740 * @return the predicate sort
2742 Sort
mkPredicateSort(const std::vector
<Sort
>& sorts
) const;
2745 * Create a record sort
2746 * @param fields the list of fields of the record
2747 * @return the record sort
2750 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const;
2753 * Create a set sort.
2754 * @param elemSort the sort of the set elements
2755 * @return the set sort
2757 Sort
mkSetSort(const Sort
& elemSort
) const;
2760 * Create a bag sort.
2761 * @param elemSort the sort of the bag elements
2762 * @return the bag sort
2764 Sort
mkBagSort(const Sort
& elemSort
) const;
2767 * Create a sequence sort.
2768 * @param elemSort the sort of the sequence elements
2769 * @return the sequence sort
2771 Sort
mkSequenceSort(const Sort
& elemSort
) const;
2774 * Create an uninterpreted sort.
2775 * @param symbol the name of the sort
2776 * @return the uninterpreted sort
2778 Sort
mkUninterpretedSort(const std::string
& symbol
) const;
2781 * Create a sort constructor sort.
2782 * @param symbol the symbol of the sort
2783 * @param arity the arity of the sort
2784 * @return the sort constructor sort
2786 Sort
mkSortConstructorSort(const std::string
& symbol
, size_t arity
) const;
2789 * Create a tuple sort.
2790 * @param sorts of the elements of the tuple
2791 * @return the tuple sort
2793 Sort
mkTupleSort(const std::vector
<Sort
>& sorts
) const;
2795 /* .................................................................... */
2797 /* .................................................................... */
2800 * Create 0-ary term of given kind.
2801 * @param kind the kind of the term
2804 Term
mkTerm(Kind kind
) const;
2807 * Create a unary term of given kind.
2808 * @param kind the kind of the term
2809 * @param child the child of the term
2812 Term
mkTerm(Kind kind
, const Term
& child
) const;
2815 * Create binary term of given kind.
2816 * @param kind the kind of the term
2817 * @param child1 the first child of the term
2818 * @param child2 the second child of the term
2821 Term
mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const;
2824 * Create ternary term of given kind.
2825 * @param kind the kind of the term
2826 * @param child1 the first child of the term
2827 * @param child2 the second child of the term
2828 * @param child3 the third child of the term
2831 Term
mkTerm(Kind kind
,
2834 const Term
& child3
) const;
2837 * Create n-ary term of given kind.
2838 * @param kind the kind of the term
2839 * @param children the children of the term
2842 Term
mkTerm(Kind kind
, const std::vector
<Term
>& children
) const;
2845 * Create nullary term of given kind from a given operator.
2846 * Create operators with mkOp().
2847 * @param op the operator
2850 Term
mkTerm(const Op
& op
) const;
2853 * Create unary term of given kind from a given operator.
2854 * Create operators with mkOp().
2855 * @param op the operator
2856 * @param child the child of the term
2859 Term
mkTerm(const Op
& op
, const Term
& child
) const;
2862 * Create binary term of given kind from a given operator.
2863 * Create operators with mkOp().
2864 * @param op the operator
2865 * @param child1 the first child of the term
2866 * @param child2 the second child of the term
2869 Term
mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const;
2872 * Create ternary term of given kind from a given operator.
2873 * Create operators with mkOp().
2874 * @param op the operator
2875 * @param child1 the first child of the term
2876 * @param child2 the second child of the term
2877 * @param child3 the third child of the term
2880 Term
mkTerm(const Op
& op
,
2883 const Term
& child3
) const;
2886 * Create n-ary term of given kind from a given operator.
2887 * Create operators with mkOp().
2888 * @param op the operator
2889 * @param children the children of the term
2892 Term
mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const;
2895 * Create a tuple term. Terms are automatically converted if sorts are
2897 * @param sorts The sorts of the elements in the tuple
2898 * @param terms The elements in the tuple
2899 * @return the tuple Term
2901 Term
mkTuple(const std::vector
<Sort
>& sorts
,
2902 const std::vector
<Term
>& terms
) const;
2904 /* .................................................................... */
2905 /* Create Operators */
2906 /* .................................................................... */
2909 * Create an operator for a builtin Kind
2910 * The Kind may not be the Kind for an indexed operator
2911 * (e.g. BITVECTOR_EXTRACT)
2912 * Note: in this case, the Op simply wraps the Kind.
2913 * The Kind can be used in mkTerm directly without
2914 * creating an op first.
2915 * @param kind the kind to wrap
2917 Op
mkOp(Kind kind
) const;
2920 * Create operator of kind:
2921 * - DIVISIBLE (to support arbitrary precision integers)
2922 * See enum Kind for a description of the parameters.
2923 * @param kind the kind of the operator
2924 * @param arg the string argument to this operator
2926 Op
mkOp(Kind kind
, const std::string
& arg
) const;
2929 * Create operator of kind:
2931 * - BITVECTOR_REPEAT
2932 * - BITVECTOR_ZERO_EXTEND
2933 * - BITVECTOR_SIGN_EXTEND
2934 * - BITVECTOR_ROTATE_LEFT
2935 * - BITVECTOR_ROTATE_RIGHT
2936 * - INT_TO_BITVECTOR
2937 * - FLOATINGPOINT_TO_UBV
2938 * - FLOATINGPOINT_TO_UBV_TOTAL
2939 * - FLOATINGPOINT_TO_SBV
2940 * - FLOATINGPOINT_TO_SBV_TOTAL
2942 * See enum Kind for a description of the parameters.
2943 * @param kind the kind of the operator
2944 * @param arg the uint32_t argument to this operator
2946 Op
mkOp(Kind kind
, uint32_t arg
) const;
2949 * Create operator of Kind:
2950 * - BITVECTOR_EXTRACT
2951 * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
2952 * - FLOATINGPOINT_TO_FP_FLOATINGPOINT
2953 * - FLOATINGPOINT_TO_FP_REAL
2954 * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
2955 * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
2956 * - FLOATINGPOINT_TO_FP_GENERIC
2957 * See enum Kind for a description of the parameters.
2958 * @param kind the kind of the operator
2959 * @param arg1 the first uint32_t argument to this operator
2960 * @param arg2 the second uint32_t argument to this operator
2962 Op
mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const;
2965 * Create operator of Kind:
2967 * See enum Kind for a description of the parameters.
2968 * @param kind the kind of the operator
2969 * @param args the arguments (indices) of the operator
2971 Op
mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const;
2973 /* .................................................................... */
2974 /* Create Constants */
2975 /* .................................................................... */
2978 * Create a Boolean true constant.
2979 * @return the true constant
2981 Term
mkTrue() const;
2984 * Create a Boolean false constant.
2985 * @return the false constant
2987 Term
mkFalse() const;
2990 * Create a Boolean constant.
2991 * @return the Boolean constant
2992 * @param val the value of the constant
2994 Term
mkBoolean(bool val
) const;
2997 * Create a constant representing the number Pi.
2998 * @return a constant representing Pi
3002 * Create an integer constant from a string.
3003 * @param s the string representation of the constant, may represent an
3004 * integer (e.g., "123").
3005 * @return a constant of sort Integer assuming 's' represents an integer)
3007 Term
mkInteger(const std::string
& s
) const;
3010 * Create an integer constant from a c++ int.
3011 * @param val the value of the constant
3012 * @return a constant of sort Integer
3014 Term
mkInteger(int64_t val
) const;
3017 * Create a real constant from a string.
3018 * @param s the string representation of the constant, may represent an
3019 * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
3020 * @return a constant of sort Real
3022 Term
mkReal(const std::string
& s
) const;
3025 * Create a real constant from an integer.
3026 * @param val the value of the constant
3027 * @return a constant of sort Integer
3029 Term
mkReal(int64_t val
) const;
3032 * Create a real constant from a rational.
3033 * @param num the value of the numerator
3034 * @param den the value of the denominator
3035 * @return a constant of sort Real
3037 Term
mkReal(int64_t num
, int64_t den
) const;
3040 * Create a regular expression empty term.
3041 * @return the empty term
3043 Term
mkRegexpEmpty() const;
3046 * Create a regular expression sigma term.
3047 * @return the sigma term
3049 Term
mkRegexpSigma() const;
3052 * Create a constant representing an empty set of the given sort.
3053 * @param sort the sort of the set elements.
3054 * @return the empty set constant
3056 Term
mkEmptySet(const Sort
& sort
) const;
3059 * Create a constant representing an empty bag of the given sort.
3060 * @param sort the sort of the bag elements.
3061 * @return the empty bag constant
3063 Term
mkEmptyBag(const Sort
& sort
) const;
3066 * Create a separation logic nil term.
3067 * @param sort the sort of the nil term
3068 * @return the separation logic nil term
3070 Term
mkSepNil(const Sort
& sort
) const;
3073 * Create a String constant.
3074 * @param s the string this constant represents
3075 * @param useEscSequences determines whether escape sequences in \p s should
3076 * be converted to the corresponding character
3077 * @return the String constant
3079 Term
mkString(const std::string
& s
, bool useEscSequences
= false) const;
3082 * Create a String constant.
3083 * @param c the character this constant represents
3084 * @return the String constant
3086 Term
mkString(const unsigned char c
) const;
3089 * Create a String constant.
3090 * @param s a list of unsigned (unicode) values this constant represents as
3092 * @return the String constant
3094 Term
mkString(const std::vector
<uint32_t>& s
) const;
3097 * Create a character constant from a given string.
3098 * @param s the string denoting the code point of the character (in base 16)
3099 * @return the character constant
3101 Term
mkChar(const std::string
& s
) const;
3104 * Create an empty sequence of the given element sort.
3105 * @param sort The element sort of the sequence.
3106 * @return the empty sequence with given element sort.
3108 Term
mkEmptySequence(const Sort
& sort
) const;
3111 * Create a universe set of the given sort.
3112 * @param sort the sort of the set elements
3113 * @return the universe set constant
3115 Term
mkUniverseSet(const Sort
& sort
) const;
3118 * Create a bit-vector constant of given size and value.
3119 * @param size the bit-width of the bit-vector sort
3120 * @param val the value of the constant
3121 * @return the bit-vector constant
3123 Term
mkBitVector(uint32_t size
, uint64_t val
= 0) const;
3126 * Create a bit-vector constant from a given string of base 2, 10 or 16.
3128 * The size of resulting bit-vector is
3129 * - base 2: the size of the binary string
3130 * - base 10: the min. size required to represent the decimal as a bit-vector
3131 * - base 16: the max. size required to represent the hexadecimal as a
3132 * bit-vector (4 * size of the given value string)
3134 * @param s the string representation of the constant
3135 * @param base the base of the string representation (2, 10, or 16)
3136 * @return the bit-vector constant
3138 Term
mkBitVector(const std::string
& s
, uint32_t base
= 2) const;
3141 * Create a bit-vector constant of a given bit-width from a given string of
3143 * @param size the bit-width of the constant
3144 * @param s the string representation of the constant
3145 * @param base the base of the string representation (2, 10, or 16)
3146 * @return the bit-vector constant
3148 Term
mkBitVector(uint32_t size
, const std::string
& s
, uint32_t base
) const;
3151 * Create a constant array with the provided constant value stored at every
3153 * @param sort the sort of the constant array (must be an array sort)
3154 * @param val the constant value to store (must match the sort's element sort)
3155 * @return the constant array term
3157 Term
mkConstArray(const Sort
& sort
, const Term
& val
) const;
3160 * Create a positive infinity floating-point constant. Requires cvc5 to be
3161 * compiled with SymFPU support.
3162 * @param exp Number of bits in the exponent
3163 * @param sig Number of bits in the significand
3164 * @return the floating-point constant
3166 Term
mkPosInf(uint32_t exp
, uint32_t sig
) const;
3169 * Create a negative infinity floating-point constant. Requires cvc5 to be
3170 * compiled with SymFPU support.
3171 * @param exp Number of bits in the exponent
3172 * @param sig Number of bits in the significand
3173 * @return the floating-point constant
3175 Term
mkNegInf(uint32_t exp
, uint32_t sig
) const;
3178 * Create a not-a-number (NaN) floating-point constant. Requires cvc5 to be
3179 * compiled with SymFPU support.
3180 * @param exp Number of bits in the exponent
3181 * @param sig Number of bits in the significand
3182 * @return the floating-point constant
3184 Term
mkNaN(uint32_t exp
, uint32_t sig
) const;
3187 * Create a positive zero (+0.0) floating-point constant. Requires cvc5 to be
3188 * compiled with SymFPU support.
3189 * @param exp Number of bits in the exponent
3190 * @param sig Number of bits in the significand
3191 * @return the floating-point constant
3193 Term
mkPosZero(uint32_t exp
, uint32_t sig
) const;
3196 * Create a negative zero (-0.0) floating-point constant. Requires cvc5 to be
3197 * compiled with SymFPU support.
3198 * @param exp Number of bits in the exponent
3199 * @param sig Number of bits in the significand
3200 * @return the floating-point constant
3202 Term
mkNegZero(uint32_t exp
, uint32_t sig
) const;
3205 * Create a roundingmode constant.
3206 * @param rm the floating point rounding mode this constant represents
3208 Term
mkRoundingMode(RoundingMode rm
) const;
3211 * Create uninterpreted constant.
3212 * @param sort Sort of the constant
3213 * @param index Index of the constant
3215 Term
mkUninterpretedConst(const Sort
& sort
, int32_t index
) const;
3218 * Create an abstract value constant.
3219 * @param index Index of the abstract value
3221 Term
mkAbstractValue(const std::string
& index
) const;
3224 * Create an abstract value constant.
3225 * @param index Index of the abstract value
3227 Term
mkAbstractValue(uint64_t index
) const;
3230 * Create a floating-point constant (requires cvc5 to be compiled with symFPU
3232 * @param exp Size of the exponent
3233 * @param sig Size of the significand
3234 * @param val Value of the floating-point constant as a bit-vector term
3236 Term
mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const;
3238 /* .................................................................... */
3239 /* Create Variables */
3240 /* .................................................................... */
3243 * Create (first-order) constant (0-arity function symbol).
3246 * ( declare-const <symbol> <sort> )
3247 * ( declare-fun <symbol> ( ) <sort> )
3250 * @param sort the sort of the constant
3251 * @param symbol the name of the constant
3252 * @return the first-order constant
3254 Term
mkConst(const Sort
& sort
, const std::string
& symbol
) const;
3256 * Create (first-order) constant (0-arity function symbol), with a default
3259 * @param sort the sort of the constant
3260 * @return the first-order constant
3262 Term
mkConst(const Sort
& sort
) const;
3265 * Create a bound variable to be used in a binder (i.e. a quantifier, a
3266 * lambda, or a witness binder).
3267 * @param sort the sort of the variable
3268 * @param symbol the name of the variable
3269 * @return the variable
3271 Term
mkVar(const Sort
& sort
, const std::string
& symbol
= std::string()) const;
3273 /* .................................................................... */
3274 /* Create datatype constructor declarations */
3275 /* .................................................................... */
3277 DatatypeConstructorDecl
mkDatatypeConstructorDecl(const std::string
& name
);
3279 /* .................................................................... */
3280 /* Create datatype declarations */
3281 /* .................................................................... */
3284 * Create a datatype declaration.
3285 * @param name the name of the datatype
3286 * @param isCoDatatype true if a codatatype is to be constructed
3287 * @return the DatatypeDecl
3289 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3290 bool isCoDatatype
= false);
3293 * Create a datatype declaration.
3294 * Create sorts parameter with Solver::mkParamSort().
3295 * @param name the name of the datatype
3296 * @param param the sort parameter
3297 * @param isCoDatatype true if a codatatype is to be constructed
3298 * @return the DatatypeDecl
3300 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3302 bool isCoDatatype
= false);
3305 * Create a datatype declaration.
3306 * Create sorts parameter with Solver::mkParamSort().
3307 * @param name the name of the datatype
3308 * @param params a list of sort parameters
3309 * @param isCoDatatype true if a codatatype is to be constructed
3310 * @return the DatatypeDecl
3312 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3313 const std::vector
<Sort
>& params
,
3314 bool isCoDatatype
= false);
3316 /* .................................................................... */
3317 /* Formula Handling */
3318 /* .................................................................... */
3321 * Simplify a formula without doing "much" work. Does not involve
3322 * the SAT Engine in the simplification, but uses the current
3323 * definitions, assertions, and the current partial model, if one
3324 * has been constructed. It also involves theory normalization.
3325 * @param t the formula to simplify
3326 * @return the simplified formula
3328 Term
simplify(const Term
& t
);
3336 * @param term the formula to assert
3338 void assertFormula(const Term
& term
) const;
3341 * Check satisfiability.
3346 * @return the result of the satisfiability check.
3348 Result
checkSat() const;
3351 * Check satisfiability assuming the given formula.
3354 * ( check-sat-assuming ( <prop_literal> ) )
3356 * @param assumption the formula to assume
3357 * @return the result of the satisfiability check.
3359 Result
checkSatAssuming(const Term
& assumption
) const;
3362 * Check satisfiability assuming the given formulas.
3365 * ( check-sat-assuming ( <prop_literal>+ ) )
3367 * @param assumptions the formulas to assume
3368 * @return the result of the satisfiability check.
3370 Result
checkSatAssuming(const std::vector
<Term
>& assumptions
) const;
3373 * Check entailment of the given formula w.r.t. the current set of assertions.
3374 * @param term the formula to check entailment for
3375 * @return the result of the entailment check.
3377 Result
checkEntailed(const Term
& term
) const;
3380 * Check entailment of the given set of given formulas w.r.t. the current
3381 * set of assertions.
3382 * @param terms the terms to check entailment for
3383 * @return the result of the entailmentcheck.
3385 Result
checkEntailed(const std::vector
<Term
>& terms
) const;
3388 * Create datatype sort.
3391 * ( declare-datatype <symbol> <datatype_decl> )
3393 * @param symbol the name of the datatype sort
3394 * @param ctors the constructor declarations of the datatype sort
3395 * @return the datatype sort
3397 Sort
declareDatatype(const std::string
& symbol
,
3398 const std::vector
<DatatypeConstructorDecl
>& ctors
) const;
3401 * Declare n-ary function symbol.
3404 * ( declare-fun <symbol> ( <sort>* ) <sort> )
3406 * @param symbol the name of the function
3407 * @param sorts the sorts of the parameters to this function
3408 * @param sort the sort of the return value of this function
3409 * @return the function
3411 Term
declareFun(const std::string
& symbol
,
3412 const std::vector
<Sort
>& sorts
,
3413 const Sort
& sort
) const;
3416 * Declare uninterpreted sort.
3419 * ( declare-sort <symbol> <numeral> )
3421 * @param symbol the name of the sort
3422 * @param arity the arity of the sort
3425 Sort
declareSort(const std::string
& symbol
, uint32_t arity
) const;
3428 * Define n-ary function.
3431 * ( define-fun <function_def> )
3433 * @param symbol the name of the function
3434 * @param bound_vars the parameters to this function
3435 * @param sort the sort of the return value of this function
3436 * @param term the function body
3437 * @param global determines whether this definition is global (i.e. persists
3438 * when popping the context)
3439 * @return the function
3441 Term
defineFun(const std::string
& symbol
,
3442 const std::vector
<Term
>& bound_vars
,
3445 bool global
= false) const;
3447 * Define n-ary function.
3450 * ( define-fun <function_def> )
3452 * Create parameter 'fun' with mkConst().
3453 * @param fun the sorted function
3454 * @param bound_vars the parameters to this function
3455 * @param term the function body
3456 * @param global determines whether this definition is global (i.e. persists
3457 * when popping the context)
3458 * @return the function
3460 Term
defineFun(const Term
& fun
,
3461 const std::vector
<Term
>& bound_vars
,
3463 bool global
= false) const;
3466 * Define recursive function.
3469 * ( define-fun-rec <function_def> )
3471 * @param symbol the name of the function
3472 * @param bound_vars the parameters to this function
3473 * @param sort the sort of the return value of this function
3474 * @param term the function body
3475 * @param global determines whether this definition is global (i.e. persists
3476 * when popping the context)
3477 * @return the function
3479 Term
defineFunRec(const std::string
& symbol
,
3480 const std::vector
<Term
>& bound_vars
,
3483 bool global
= false) const;
3486 * Define recursive function.
3489 * ( define-fun-rec <function_def> )
3491 * Create parameter 'fun' with mkConst().
3492 * @param fun the sorted function
3493 * @param bound_vars the parameters to this function
3494 * @param term the function body
3495 * @param global determines whether this definition is global (i.e. persists
3496 * when popping the context)
3497 * @return the function
3499 Term
defineFunRec(const Term
& fun
,
3500 const std::vector
<Term
>& bound_vars
,
3502 bool global
= false) const;
3505 * Define recursive functions.
3508 * ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3510 * Create elements of parameter 'funs' with mkConst().
3511 * @param funs the sorted functions
3512 * @param bound_vars the list of parameters to the functions
3513 * @param terms the list of function bodies of the functions
3514 * @param global determines whether this definition is global (i.e. persists
3515 * when popping the context)
3516 * @return the function
3518 void defineFunsRec(const std::vector
<Term
>& funs
,
3519 const std::vector
<std::vector
<Term
>>& bound_vars
,
3520 const std::vector
<Term
>& terms
,
3521 bool global
= false) const;
3524 * Echo a given string to the given output stream.
3527 * ( echo <std::string> )
3529 * @param out the output stream
3530 * @param str the string to echo
3532 void echo(std::ostream
& out
, const std::string
& str
) const;
3535 * Get the list of asserted formulas.
3538 * ( get-assertions )
3540 * @return the list of asserted formulas
3542 std::vector
<Term
> getAssertions() const;
3545 * Get info from the solver.
3546 * SMT-LIB: \verbatim( get-info <info_flag> )\verbatim
3549 std::string
getInfo(const std::string
& flag
) const;
3552 * Get the value of a given option.
3555 * ( get-option <keyword> )
3557 * @param option the option for which the value is queried
3558 * @return a string representation of the option value
3560 std::string
getOption(const std::string
& option
) const;
3563 * Get the set of unsat ("failed") assumptions.
3566 * ( get-unsat-assumptions )
3568 * Requires to enable option 'produce-unsat-assumptions'.
3569 * @return the set of unsat assumptions.
3571 std::vector
<Term
> getUnsatAssumptions() const;
3574 * Get the unsatisfiable core.
3577 * ( get-unsat-core )
3579 * Requires to enable option 'produce-unsat-cores'.
3580 * @return a set of terms representing the unsatisfiable core
3582 std::vector
<Term
> getUnsatCore() const;
3585 * Get the value of the given term.
3588 * ( get-value ( <term> ) )
3590 * @param term the term for which the value is queried
3591 * @return the value of the given term
3593 Term
getValue(const Term
& term
) const;
3595 * Get the values of the given terms.
3598 * ( get-value ( <term>+ ) )
3600 * @param terms the terms for which the value is queried
3601 * @return the values of the given terms
3603 std::vector
<Term
> getValue(const std::vector
<Term
>& terms
) const;
3606 * Do quantifier elimination.
3611 * Requires a logic that supports quantifier elimination. Currently, the only
3612 * logics supported by quantifier elimination is LRA and LIA.
3613 * @param q a quantified formula of the form:
3614 * Q x1...xn. P( x1...xn, y1...yn )
3615 * where P( x1...xn, y1...yn ) is a quantifier-free formula
3616 * @return a formula ret such that, given the current set of formulas A
3617 * asserted to this solver:
3618 * - ( A ^ q ) and ( A ^ ret ) are equivalent
3619 * - ret is quantifier-free formula containing only free variables in
3622 Term
getQuantifierElimination(const Term
& q
) const;
3625 * Do partial quantifier elimination, which can be used for incrementally
3626 * computing the result of a quantifier elimination.
3629 * ( get-qe-disjunct <q> )
3631 * Requires a logic that supports quantifier elimination. Currently, the only
3632 * logics supported by quantifier elimination is LRA and LIA.
3633 * @param q a quantified formula of the form:
3634 * Q x1...xn. P( x1...xn, y1...yn )
3635 * where P( x1...xn, y1...yn ) is a quantifier-free formula
3636 * @return a formula ret such that, given the current set of formulas A
3637 * asserted to this solver:
3638 * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
3640 * - ret is quantifier-free formula containing only free variables in
3642 * - If Q is exists, let A^Q_n be the formula
3643 * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
3644 * where for each i=1,...n, formula ret^Q_i is the result of calling
3645 * getQuantifierEliminationDisjunct for q with the set of assertions
3646 * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
3647 * A ^ ret^Q_1 ^ ... ^ ret^Q_n
3648 * where ret^Q_i is the same as above. In either case, we have
3649 * that ret^Q_j will eventually be true or false, for some finite j.
3651 Term
getQuantifierEliminationDisjunct(const Term
& q
) const;
3654 * When using separation logic, this sets the location sort and the
3655 * datatype sort to the given ones. This method should be invoked exactly
3656 * once, before any separation logic constraints are provided.
3657 * @param locSort The location sort of the heap
3658 * @param dataSort The data sort of the heap
3660 void declareSeparationHeap(const Sort
& locSort
, const Sort
& dataSort
) const;
3663 * When using separation logic, obtain the term for the heap.
3664 * @return The term for the heap
3666 Term
getSeparationHeap() const;
3669 * When using separation logic, obtain the term for nil.
3670 * @return The term for nil
3672 Term
getSeparationNilTerm() const;
3675 * Declare a symbolic pool of terms with the given initial value.
3678 * ( declare-pool <symbol> <sort> ( <term>* ) )
3680 * @param symbol The name of the pool
3681 * @param sort The sort of the elements of the pool.
3682 * @param initValue The initial value of the pool
3684 Term
declarePool(const std::string
& symbol
,
3686 const std::vector
<Term
>& initValue
) const;
3688 * Pop (a) level(s) from the assertion stack.
3693 * @param nscopes the number of levels to pop
3695 void pop(uint32_t nscopes
= 1) const;
3698 * Get an interpolant
3701 * ( get-interpol <conj> )
3703 * Requires to enable option 'produce-interpols'.
3704 * @param conj the conjecture term
3705 * @param output a Term I such that A->I and I->B are valid, where A is the
3706 * current set of assertions and B is given in the input by conj.
3707 * @return true if it gets I successfully, false otherwise.
3709 bool getInterpolant(const Term
& conj
, Term
& output
) const;
3712 * Get an interpolant
3715 * ( get-interpol <conj> <g> )
3717 * Requires to enable option 'produce-interpols'.
3718 * @param conj the conjecture term
3719 * @param grammar the grammar for the interpolant I
3720 * @param output a Term I such that A->I and I->B are valid, where A is the
3721 * current set of assertions and B is given in the input by conj.
3722 * @return true if it gets I successfully, false otherwise.
3724 bool getInterpolant(const Term
& conj
, Grammar
& grammar
, Term
& output
) const;
3730 * ( get-abduct <conj> )
3732 * Requires enabling option 'produce-abducts'
3733 * @param conj the conjecture term
3734 * @param output a term C such that A^C is satisfiable, and A^~B^C is
3735 * unsatisfiable, where A is the current set of assertions and B is
3736 * given in the input by conj
3737 * @return true if it gets C successfully, false otherwise
3739 bool getAbduct(const Term
& conj
, Term
& output
) const;
3745 * ( get-abduct <conj> <g> )
3747 * Requires enabling option 'produce-abducts'
3748 * @param conj the conjecture term
3749 * @param grammar the grammar for the abduct C
3750 * @param output a term C such that A^C is satisfiable, and A^~B^C is
3751 * unsatisfiable, where A is the current set of assertions and B is
3752 * given in the input by conj
3753 * @return true if it gets C successfully, false otherwise
3755 bool getAbduct(const Term
& conj
, Grammar
& grammar
, Term
& output
) const;
3758 * Block the current model. Can be called only if immediately preceded by a
3759 * SAT or INVALID query.
3764 * Requires enabling 'produce-models' option and setting 'block-models' option
3765 * to a mode other than "none".
3767 void blockModel() const;
3770 * Block the current model values of (at least) the values in terms. Can be
3771 * called only if immediately preceded by a SAT or NOT_ENTAILED query.
3774 * ( block-model-values ( <terms>+ ) )
3776 * Requires enabling 'produce-models' option and setting 'block-models' option
3777 * to a mode other than "none".
3779 void blockModelValues(const std::vector
<Term
>& terms
) const;
3782 * Print all instantiations made by the quantifiers module.
3783 * @param out the output stream
3785 void printInstantiations(std::ostream
& out
) const;
3788 * Push (a) level(s) to the assertion stack.
3791 * ( push <numeral> )
3793 * @param nscopes the number of levels to push
3795 void push(uint32_t nscopes
= 1) const;
3798 * Remove all assertions.
3801 * ( reset-assertions )
3804 void resetAssertions() const;
3810 * ( set-info <attribute> )
3812 * @param keyword the info flag
3813 * @param value the value of the info flag
3815 void setInfo(const std::string
& keyword
, const std::string
& value
) const;
3821 * ( set-logic <symbol> )
3823 * @param logic the logic to set
3825 void setLogic(const std::string
& logic
) const;
3831 * ( set-option <option> )
3833 * @param option the option name
3834 * @param value the option value
3836 void setOption(const std::string
& option
, const std::string
& value
) const;
3839 * If needed, convert this term to a given sort. Note that the sort of the
3840 * term must be convertible into the target sort. Currently only Int to Real
3841 * conversions are supported.
3843 * @param s the target sort
3844 * @return the term wrapped into a sort conversion if needed
3846 Term
ensureTermSort(const Term
& t
, const Sort
& s
) const;
3849 * Append \p symbol to the current list of universal variables.
3852 * ( declare-var <symbol> <sort> )
3854 * @param sort the sort of the universal variable
3855 * @param symbol the name of the universal variable
3856 * @return the universal variable
3858 Term
mkSygusVar(const Sort
& sort
,
3859 const std::string
& symbol
= std::string()) const;
3862 * Create a Sygus grammar. The first non-terminal is treated as the starting
3863 * non-terminal, so the order of non-terminals matters.
3865 * @param boundVars the parameters to corresponding synth-fun/synth-inv
3866 * @param ntSymbols the pre-declaration of the non-terminal symbols
3867 * @return the grammar
3869 Grammar
mkSygusGrammar(const std::vector
<Term
>& boundVars
,
3870 const std::vector
<Term
>& ntSymbols
) const;
3873 * Synthesize n-ary function.
3876 * ( synth-fun <symbol> ( <boundVars>* ) <sort> )
3878 * @param symbol the name of the function
3879 * @param boundVars the parameters to this function
3880 * @param sort the sort of the return value of this function
3881 * @return the function
3883 Term
synthFun(const std::string
& symbol
,
3884 const std::vector
<Term
>& boundVars
,
3885 const Sort
& sort
) const;
3888 * Synthesize n-ary function following specified syntactic constraints.
3891 * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
3893 * @param symbol the name of the function
3894 * @param boundVars the parameters to this function
3895 * @param sort the sort of the return value of this function
3896 * @param grammar the syntactic constraints
3897 * @return the function
3899 Term
synthFun(const std::string
& symbol
,
3900 const std::vector
<Term
>& boundVars
,
3902 Grammar
& grammar
) const;
3905 * Synthesize invariant.
3908 * ( synth-inv <symbol> ( <boundVars>* ) )
3910 * @param symbol the name of the invariant
3911 * @param boundVars the parameters to this invariant
3912 * @return the invariant
3914 Term
synthInv(const std::string
& symbol
,
3915 const std::vector
<Term
>& boundVars
) const;
3918 * Synthesize invariant following specified syntactic constraints.
3921 * ( synth-inv <symbol> ( <boundVars>* ) <g> )
3923 * @param symbol the name of the invariant
3924 * @param boundVars the parameters to this invariant
3925 * @param grammar the syntactic constraints
3926 * @return the invariant
3928 Term
synthInv(const std::string
& symbol
,
3929 const std::vector
<Term
>& boundVars
,
3930 Grammar
& grammar
) const;
3933 * Add a forumla to the set of Sygus constraints.
3936 * ( constraint <term> )
3938 * @param term the formula to add as a constraint
3940 void addSygusConstraint(const Term
& term
) const;
3943 * Add a set of Sygus constraints to the current state that correspond to an
3944 * invariant synthesis problem.
3947 * ( inv-constraint <inv> <pre> <trans> <post> )
3949 * @param inv the function-to-synthesize
3950 * @param pre the pre-condition
3951 * @param trans the transition relation
3952 * @param post the post-condition
3954 void addSygusInvConstraint(Term inv
, Term pre
, Term trans
, Term post
) const;
3957 * Try to find a solution for the synthesis conjecture corresponding to the
3958 * current list of functions-to-synthesize, universal variables and
3964 * @return the result of the synthesis conjecture.
3966 Result
checkSynth() const;
3969 * Get the synthesis solution of the given term. This method should be called
3970 * immediately after the solver answers unsat for sygus input.
3971 * @param term the term for which the synthesis solution is queried
3972 * @return the synthesis solution of the given term
3974 Term
getSynthSolution(Term term
) const;
3977 * Get the synthesis solutions of the given terms. This method should be
3978 * called immediately after the solver answers unsat for sygus input.
3979 * @param terms the terms for which the synthesis solutions is queried
3980 * @return the synthesis solutions of the given terms
3982 std::vector
<Term
> getSynthSolutions(const std::vector
<Term
>& terms
) const;
3985 * Print solution for synthesis conjecture to the given output stream.
3986 * @param out the output stream
3988 void printSynthSolution(std::ostream
& out
) const;
3990 // !!! This is only temporarily available until the parser is fully migrated
3991 // to the new API. !!!
3992 SmtEngine
* getSmtEngine(void) const;
3994 // !!! This is only temporarily available until options are refactored at
3995 // the driver level. !!!
3996 Options
& getOptions(void);
3999 * Returns a snapshot of the current state of the statistic values of this
4000 * solver. The returned object is completely decoupled from the solver and
4001 * will not change when the solver is used again.
4003 Statistics
getStatistics() const;
4006 /** @return the node manager of this solver */
4007 NodeManager
* getNodeManager(void) const;
4008 /** Reset the API statistics */
4009 void resetStatistics();
4011 /** Helper to check for API misuse in mkOp functions. */
4012 void checkMkTerm(Kind kind
, uint32_t nchildren
) const;
4013 /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
4014 template <typename T
>
4015 Term
mkValHelper(T t
) const;
4016 /** Helper for mkReal functions that take a string as argument. */
4017 Term
mkRealFromStrHelper(const std::string
& s
) const;
4018 /** Helper for mkBitVector functions that take a string as argument. */
4019 Term
mkBVFromStrHelper(const std::string
& s
, uint32_t base
) const;
4021 * Helper for mkBitVector functions that take a string and a size as
4024 Term
mkBVFromStrHelper(uint32_t size
,
4025 const std::string
& s
,
4026 uint32_t base
) const;
4027 /** Helper for mkBitVector functions that take an integer as argument. */
4028 Term
mkBVFromIntHelper(uint32_t size
, uint64_t val
) const;
4029 /** Helper for functions that create tuple sorts. */
4030 Sort
mkTupleSortHelper(const std::vector
<Sort
>& sorts
) const;
4031 /** Helper for mkTerm functions that create Term from a Kind */
4032 Term
mkTermFromKind(Kind kind
) const;
4033 /** Helper for mkChar functions that take a string as argument. */
4034 Term
mkCharFromStrHelper(const std::string
& s
) const;
4035 /** Get value helper, which accounts for subtyping */
4036 Term
getValueHelper(const Term
& term
) const;
4039 * Helper function that ensures that a given term is of sort real (as opposed
4040 * to being of sort integer).
4041 * @param t a term of sort integer or real
4042 * @return a term of sort real
4044 Term
ensureRealSort(const Term
& t
) const;
4047 * Create n-ary term of given kind. This handles the cases of left/right
4048 * associative operators, chainable operators, and cases when the number of
4049 * children exceeds the maximum arity for the kind.
4050 * @param kind the kind of the term
4051 * @param children the children of the term
4054 Term
mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const;
4057 * Create n-ary term of given kind from a given operator.
4058 * @param op the operator
4059 * @param children the children of the term
4062 Term
mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const;
4065 * Create a vector of datatype sorts, using unresolved sorts.
4066 * @param dtypedecls the datatype declarations from which the sort is created
4067 * @param unresolvedSorts the list of unresolved sorts
4068 * @return the datatype sorts
4070 std::vector
<Sort
> mkDatatypeSortsInternal(
4071 const std::vector
<DatatypeDecl
>& dtypedecls
,
4072 const std::set
<Sort
>& unresolvedSorts
) const;
4075 * Synthesize n-ary function following specified syntactic constraints.
4078 * ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
4080 * @param symbol the name of the function
4081 * @param boundVars the parameters to this function
4082 * @param sort the sort of the return value of this function
4083 * @param isInv determines whether this is synth-fun or synth-inv
4084 * @param grammar the syntactic constraints
4085 * @return the function
4087 Term
synthFunHelper(const std::string
& symbol
,
4088 const std::vector
<Term
>& boundVars
,
4091 Grammar
* grammar
= nullptr) const;
4093 /** Check whether string s is a valid decimal integer. */
4094 bool isValidInteger(const std::string
& s
) const;
4096 /** Increment the term stats counter. */
4097 void increment_term_stats(Kind kind
) const;
4098 /** Increment the vars stats (if 'is_var') or consts stats counter. */
4099 void increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const;
4101 /** Keep a copy of the original option settings (for resets). */
4102 std::unique_ptr
<Options
> d_originalOptions
;
4103 /** The node manager of this solver. */
4104 std::unique_ptr
<NodeManager
> d_nodeMgr
;
4105 /** The statistics collected on the Api level. */
4106 std::unique_ptr
<APIStatistics
> d_stats
;
4107 /** The SMT engine of this solver. */
4108 std::unique_ptr
<SmtEngine
> d_smtEngine
;
4109 /** The random number generator of this solver. */
4110 std::unique_ptr
<Random
> d_rng
;
4113 } // namespace cvc5::api