1 /********************* */
4 ** Top contributors (to current version):
5 ** Aina Niemetz, Andrew Reynolds, Abdalrhman Mohamed
6 ** This file is part of the CVC4 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.\endverbatim
12 ** \brief The CVC4 C++ API.
17 #include "cvc4_public.h"
19 #ifndef CVC4__API__CVC4CPP_H
20 #define CVC4__API__CVC4CPP_H
22 #include "api/cvc4cppkind.h"
29 #include <unordered_map>
30 #include <unordered_set>
35 template <bool ref_count
>
37 typedef NodeTemplate
<true> Node
;
40 class BlockModelValuesCommand
;
41 class CheckSatCommand
;
42 class CheckSatAssumingCommand
;
43 class DatatypeDeclarationCommand
;
44 class DeclareFunctionCommand
;
45 class DeclareHeapCommand
;
46 class DeclareSortCommand
;
47 class DeclareSygusVarCommand
;
48 class DefineFunctionCommand
;
49 class DefineFunctionRecCommand
;
50 class DefineSortCommand
;
52 class DTypeConstructor
;
54 class GetAbductCommand
;
55 class GetInterpolCommand
;
56 class GetModelCommand
;
57 class GetQuantifierEliminationCommand
;
58 class GetUnsatCoreCommand
;
59 class GetValueCommand
;
61 class SetUserAttributeCommand
;
62 class SimplifyCommand
;
64 class SygusConstraintCommand
;
65 class SygusInvConstraintCommand
;
66 class SynthFunCommand
;
79 /* -------------------------------------------------------------------------- */
81 /* -------------------------------------------------------------------------- */
83 class CVC4_PUBLIC CVC4ApiException
: public std::exception
86 CVC4ApiException(const std::string
& str
) : d_msg(str
) {}
87 CVC4ApiException(const std::stringstream
& stream
) : d_msg(stream
.str()) {}
88 std::string
getMessage() const { return d_msg
; }
89 const char* what() const noexcept override
{ return d_msg
.c_str(); }
95 class CVC4_PUBLIC CVC4ApiRecoverableException
: public CVC4ApiException
98 CVC4ApiRecoverableException(const std::string
& str
) : CVC4ApiException(str
) {}
99 CVC4ApiRecoverableException(const std::stringstream
& stream
)
100 : CVC4ApiException(stream
.str())
105 /* -------------------------------------------------------------------------- */
107 /* -------------------------------------------------------------------------- */
110 * Encapsulation of a three-valued solver result, with explanations.
112 class CVC4_PUBLIC Result
117 enum UnknownExplanation
135 * Return true if Result is empty, i.e., a nullary Result, and not an actual
136 * result returned from a checkSat() (and friends) query.
141 * Return true if query was a satisfiable checkSat() or checkSatAssuming()
147 * Return true if query was an unsatisfiable checkSat() or
148 * checkSatAssuming() query.
150 bool isUnsat() const;
153 * Return true if query was a checkSat() or checkSatAssuming() query and
154 * CVC4 was not able to determine (un)satisfiability.
156 bool isSatUnknown() const;
159 * Return true if corresponding query was an entailed checkEntailed() query.
161 bool isEntailed() const;
164 * Return true if corresponding query was a checkEntailed() query that is
167 bool isNotEntailed() const;
170 * Return true if query was a checkEntailed() () query and CVC4 was not able
171 * to determine if it is entailed.
173 bool isEntailmentUnknown() const;
176 * Operator overloading for equality of two results.
177 * @param r the result to compare to for equality
178 * @return true if the results are equal
180 bool operator==(const Result
& r
) const;
183 * Operator overloading for disequality of two results.
184 * @param r the result to compare to for disequality
185 * @return true if the results are disequal
187 bool operator!=(const Result
& r
) const;
190 * @return an explanation for an unknown query result.
192 UnknownExplanation
getUnknownExplanation() const;
195 * @return a string representation of this result.
197 std::string
toString() const;
202 * @param r the internal result that is to be wrapped by this result
205 Result(const CVC4::Result
& r
);
208 * The interal result wrapped by this result.
209 * Note: This is a shared_ptr rather than a unique_ptr since CVC4::Result is
212 std::shared_ptr
<CVC4::Result
> d_result
;
216 * Serialize a Result to given stream.
217 * @param out the output stream
218 * @param r the result to be serialized to the given output stream
219 * @return the output stream
221 std::ostream
& operator<<(std::ostream
& out
, const Result
& r
) CVC4_PUBLIC
;
224 * Serialize an UnknownExplanation to given stream.
225 * @param out the output stream
226 * @param r the explanation to be serialized to the given output stream
227 * @return the output stream
229 std::ostream
& operator<<(std::ostream
& out
,
230 enum Result::UnknownExplanation e
) CVC4_PUBLIC
;
232 /* -------------------------------------------------------------------------- */
234 /* -------------------------------------------------------------------------- */
239 * The sort of a CVC4 term.
241 class CVC4_PUBLIC Sort
243 friend class CVC4::DatatypeDeclarationCommand
;
244 friend class CVC4::DeclareFunctionCommand
;
245 friend class CVC4::DeclareHeapCommand
;
246 friend class CVC4::DeclareSortCommand
;
247 friend class CVC4::DeclareSygusVarCommand
;
248 friend class CVC4::DefineSortCommand
;
249 friend class CVC4::GetAbductCommand
;
250 friend class CVC4::GetInterpolCommand
;
251 friend class CVC4::GetModelCommand
;
252 friend class CVC4::SynthFunCommand
;
253 friend class DatatypeConstructor
;
254 friend class DatatypeConstructorDecl
;
255 friend class DatatypeSelector
;
256 friend class DatatypeDecl
;
259 friend class Grammar
;
260 friend struct SortHashFunction
;
275 * Comparison for structural equality.
276 * @param s the sort to compare to
277 * @return true if the sorts are equal
279 bool operator==(const Sort
& s
) const;
282 * Comparison for structural disequality.
283 * @param s the sort to compare to
284 * @return true if the sorts are not equal
286 bool operator!=(const Sort
& s
) const;
289 * Comparison for ordering on sorts.
290 * @param s the sort to compare to
291 * @return true if this sort is less than s
293 bool operator<(const Sort
& s
) const;
296 * Comparison for ordering on sorts.
297 * @param s the sort to compare to
298 * @return true if this sort is greater than s
300 bool operator>(const Sort
& s
) const;
303 * Comparison for ordering on sorts.
304 * @param s the sort to compare to
305 * @return true if this sort is less than or equal to s
307 bool operator<=(const Sort
& s
) const;
310 * Comparison for ordering on sorts.
311 * @param s the sort to compare to
312 * @return true if this sort is greater than or equal to s
314 bool operator>=(const Sort
& s
) const;
317 * @return true if this Sort is a null sort.
322 * Is this a Boolean sort?
323 * @return true if the sort is a Boolean sort
325 bool isBoolean() const;
328 * Is this a integer sort?
329 * @return true if the sort is a integer sort
331 bool isInteger() const;
334 * Is this a real sort?
335 * @return true if the sort is a real sort
340 * Is this a string sort?
341 * @return true if the sort is the string sort
343 bool isString() const;
346 * Is this a regexp sort?
347 * @return true if the sort is the regexp sort
349 bool isRegExp() const;
352 * Is this a rounding mode sort?
353 * @return true if the sort is the rounding mode sort
355 bool isRoundingMode() const;
358 * Is this a bit-vector sort?
359 * @return true if the sort is a bit-vector sort
361 bool isBitVector() const;
364 * Is this a floating-point sort?
365 * @return true if the sort is a floating-point sort
367 bool isFloatingPoint() const;
370 * Is this a datatype sort?
371 * @return true if the sort is a datatype sort
373 bool isDatatype() const;
376 * Is this a parametric datatype sort?
377 * @return true if the sort is a parametric datatype sort
379 bool isParametricDatatype() const;
382 * Is this a constructor sort?
383 * @return true if the sort is a constructor sort
385 bool isConstructor() const;
388 * Is this a selector sort?
389 * @return true if the sort is a selector sort
391 bool isSelector() const;
394 * Is this a tester sort?
395 * @return true if the sort is a tester sort
397 bool isTester() const;
399 * Is this a function sort?
400 * @return true if the sort is a function sort
402 bool isFunction() const;
405 * Is this a predicate sort?
406 * That is, is this a function sort mapping to Boolean? All predicate
407 * sorts are also function sorts.
408 * @return true if the sort is a predicate sort
410 bool isPredicate() const;
413 * Is this a tuple sort?
414 * @return true if the sort is a tuple sort
416 bool isTuple() const;
419 * Is this a record sort?
420 * @return true if the sort is a record sort
422 bool isRecord() const;
425 * Is this an array sort?
426 * @return true if the sort is a array sort
428 bool isArray() const;
431 * Is this a Set sort?
432 * @return true if the sort is a Set sort
437 * Is this a Bag sort?
438 * @return true if the sort is a Bag sort
443 * Is this a Sequence sort?
444 * @return true if the sort is a Sequence sort
446 bool isSequence() const;
449 * Is this a sort kind?
450 * @return true if this is a sort kind
452 bool isUninterpretedSort() const;
455 * Is this a sort constructor kind?
456 * @return true if this is a sort constructor kind
458 bool isSortConstructor() const;
461 * Is this a first-class sort?
462 * First-class sorts are sorts for which:
463 * (1) we handle equalities between terms of that type, and
464 * (2) they are allowed to be parameters of parametric sorts (e.g. index or
465 * element sorts of arrays).
467 * Examples of sorts that are not first-class include sort constructor sorts
468 * and regular expression sorts.
470 * @return true if this is a first-class sort
472 bool isFirstClass() const;
475 * Is this a function-LIKE sort?
477 * Anything function-like except arrays (e.g., datatype selectors) is
478 * considered a function here. Function-like terms can not be the argument
479 * or return value for any term that is function-like.
480 * This is mainly to avoid higher order.
482 * Note that arrays are explicitly not considered function-like here.
484 * @return true if this is a function-like sort
486 bool isFunctionLike() const;
489 * Is this sort a subsort of the given sort?
490 * @return true if this sort is a subsort of s
492 bool isSubsortOf(const Sort
& s
) const;
495 * Is this sort comparable to the given sort (i.e., do they share
496 * a common ancestor in the subsort tree)?
497 * @return true if this sort is comparable to s
499 bool isComparableTo(const Sort
& s
) const;
502 * @return the underlying datatype of a datatype sort
504 Datatype
getDatatype() const;
507 * Instantiate a parameterized datatype/sort sort.
508 * Create sorts parameter with Solver::mkParamSort().
509 * @param params the list of sort parameters to instantiate with
511 Sort
instantiate(const std::vector
<Sort
>& params
) const;
514 * Substitution of Sorts.
515 * @param sort the subsort to be substituted within this sort.
516 * @param replacement the sort replacing the substituted subsort.
518 Sort
substitute(const Sort
& sort
, const Sort
& replacement
) const;
521 * Simultaneous substitution of Sorts.
522 * @param sorts the subsorts to be substituted within this sort.
523 * @param replacements the sort replacing the substituted subsorts.
525 Sort
substitute(const std::vector
<Sort
>& sorts
,
526 const std::vector
<Sort
>& replacements
) const;
529 * Output a string representation of this sort to a given stream.
530 * @param out the output stream
532 void toStream(std::ostream
& out
) const;
535 * @return a string representation of this sort
537 std::string
toString() const;
539 /* Constructor sort ------------------------------------------------------- */
542 * @return the arity of a constructor sort
544 size_t getConstructorArity() const;
547 * @return the domain sorts of a constructor sort
549 std::vector
<Sort
> getConstructorDomainSorts() const;
552 * @return the codomain sort of a constructor sort
554 Sort
getConstructorCodomainSort() const;
556 /* Selector sort ------------------------------------------------------- */
559 * @return the domain sort of a selector sort
561 Sort
getSelectorDomainSort() const;
564 * @return the codomain sort of a selector sort
566 Sort
getSelectorCodomainSort() const;
568 /* Tester sort ------------------------------------------------------- */
571 * @return the domain sort of a tester sort
573 Sort
getTesterDomainSort() const;
576 * @return the codomain sort of a tester sort, which is the Boolean sort
578 Sort
getTesterCodomainSort() const;
580 /* Function sort ------------------------------------------------------- */
583 * @return the arity of a function sort
585 size_t getFunctionArity() const;
588 * @return the domain sorts of a function sort
590 std::vector
<Sort
> getFunctionDomainSorts() const;
593 * @return the codomain sort of a function sort
595 Sort
getFunctionCodomainSort() const;
597 /* Array sort ---------------------------------------------------------- */
600 * @return the array index sort of an array sort
602 Sort
getArrayIndexSort() const;
605 * @return the array element sort of an array element sort
607 Sort
getArrayElementSort() const;
609 /* Set sort ------------------------------------------------------------ */
612 * @return the element sort of a set sort
614 Sort
getSetElementSort() const;
616 /* Bag sort ------------------------------------------------------------ */
619 * @return the element sort of a bag sort
621 Sort
getBagElementSort() const;
623 /* Sequence sort ------------------------------------------------------- */
626 * @return the element sort of a sequence sort
628 Sort
getSequenceElementSort() const;
630 /* Uninterpreted sort -------------------------------------------------- */
633 * @return the name of an uninterpreted sort
635 std::string
getUninterpretedSortName() const;
638 * @return true if an uninterpreted sort is parameterezied
640 bool isUninterpretedSortParameterized() const;
643 * @return the parameter sorts of an uninterpreted sort
645 std::vector
<Sort
> getUninterpretedSortParamSorts() const;
647 /* Sort constructor sort ----------------------------------------------- */
650 * @return the name of a sort constructor sort
652 std::string
getSortConstructorName() const;
655 * @return the arity of a sort constructor sort
657 size_t getSortConstructorArity() const;
659 /* Bit-vector sort ----------------------------------------------------- */
662 * @return the bit-width of the bit-vector sort
664 uint32_t getBVSize() const;
666 /* Floating-point sort ------------------------------------------------- */
669 * @return the bit-width of the exponent of the floating-point sort
671 uint32_t getFPExponentSize() const;
674 * @return the width of the significand of the floating-point sort
676 uint32_t getFPSignificandSize() const;
678 /* Datatype sort ------------------------------------------------------- */
681 * @return the parameter sorts of a datatype sort
683 std::vector
<Sort
> getDatatypeParamSorts() const;
686 * @return the arity of a datatype sort
688 size_t getDatatypeArity() const;
690 /* Tuple sort ---------------------------------------------------------- */
693 * @return the length of a tuple sort
695 size_t getTupleLength() const;
698 * @return the element sorts of a tuple sort
700 std::vector
<Sort
> getTupleSorts() const;
703 /** @return the internal wrapped TypeNode of this sort. */
704 const CVC4::TypeNode
& getTypeNode(void) const;
706 /** Helper to convert a set of Sorts to internal TypeNodes. */
707 std::set
<TypeNode
> static sortSetToTypeNodes(const std::set
<Sort
>& sorts
);
708 /** Helper to convert a vector of Sorts to internal TypeNodes. */
709 std::vector
<TypeNode
> static sortVectorToTypeNodes(
710 const std::vector
<Sort
>& sorts
);
711 /** Helper to convert a vector of internal TypeNodes to Sorts. */
712 std::vector
<Sort
> static typeNodeVectorToSorts(
713 const Solver
* slv
, const std::vector
<TypeNode
>& types
);
717 * @param slv the associated solver object
718 * @param t the internal type that is to be wrapped by this sort
721 Sort(const Solver
* slv
, const CVC4::Type
& t
);
722 Sort(const Solver
* slv
, const CVC4::TypeNode
& t
);
725 * Helper for isNull checks. This prevents calling an API function with
726 * CVC4_API_CHECK_NOT_NULL
728 bool isNullHelper() const;
731 * The associated solver object.
733 const Solver
* d_solver
;
736 * The interal type wrapped by this sort.
737 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
738 * to memory allocation (CVC4::Type is already ref counted, so this
739 * could be a unique_ptr instead).
741 std::shared_ptr
<CVC4::TypeNode
> d_type
;
745 * Serialize a sort to given stream.
746 * @param out the output stream
747 * @param s the sort to be serialized to the given output stream
748 * @return the output stream
750 std::ostream
& operator<<(std::ostream
& out
, const Sort
& s
) CVC4_PUBLIC
;
753 * Hash function for Sorts.
755 struct CVC4_PUBLIC SortHashFunction
757 size_t operator()(const Sort
& s
) const;
760 /* -------------------------------------------------------------------------- */
762 /* -------------------------------------------------------------------------- */
766 * An operator is a term that represents certain operators, instantiated
767 * with its required parameters, e.g., a term of kind BITVECTOR_EXTRACT.
773 friend struct OpHashFunction
;
787 * Syntactic equality operator.
788 * Return true if both operators are syntactically identical.
789 * Both operators must belong to the same solver object.
790 * @param t the operator to compare to for equality
791 * @return true if the operators are equal
793 bool operator==(const Op
& t
) const;
796 * Syntactic disequality operator.
797 * Return true if both operators differ syntactically.
798 * Both terms must belong to the same solver object.
799 * @param t the operator to compare to for disequality
800 * @return true if operators are disequal
802 bool operator!=(const Op
& t
) const;
805 * @return the kind of this operator
807 Kind
getKind() const;
810 * @return true if this operator is a null term
815 * @return true iff this operator is indexed
817 bool isIndexed() const;
820 * Get the indices used to create this Op.
821 * Supports the following template arguments:
825 * - pair<uint32_t, uint32_t>
826 * Check the Op Kind with getKind() to determine which argument to use.
827 * @return the indices used to create this Op
829 template <typename T
>
830 T
getIndices() const;
833 * @return a string representation of this operator
835 std::string
toString() const;
839 * Constructor for a single kind (non-indexed operator).
840 * @param slv the associated solver object
841 * @param k the kind of this Op
843 Op(const Solver
* slv
, const Kind k
);
847 * @param slv the associated solver object
848 * @param k the kind of this Op
849 * @param n the internal node that is to be wrapped by this term
852 Op(const Solver
* slv
, const Kind k
, const CVC4::Node
& n
);
855 * Helper for isNull checks. This prevents calling an API function with
856 * CVC4_API_CHECK_NOT_NULL
858 bool isNullHelper() const;
861 * Note: An indexed operator has a non-null internal node, d_node
862 * Note 2: We use a helper method to avoid having API functions call
863 * other API functions (we need to call this internally)
864 * @return true iff this Op is indexed
866 bool isIndexedHelper() const;
869 * The associated solver object.
871 const Solver
* d_solver
;
873 /** The kind of this operator. */
877 * The internal node wrapped by this operator.
878 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
879 * to memory allocation (CVC4::Node is already ref counted, so this
880 * could be a unique_ptr instead).
882 std::shared_ptr
<CVC4::Node
> d_node
;
885 /* -------------------------------------------------------------------------- */
887 /* -------------------------------------------------------------------------- */
892 class CVC4_PUBLIC Term
894 friend class CVC4::AssertCommand
;
895 friend class CVC4::BlockModelValuesCommand
;
896 friend class CVC4::CheckSatCommand
;
897 friend class CVC4::CheckSatAssumingCommand
;
898 friend class CVC4::DeclareSygusVarCommand
;
899 friend class CVC4::DefineFunctionCommand
;
900 friend class CVC4::DefineFunctionRecCommand
;
901 friend class CVC4::GetAbductCommand
;
902 friend class CVC4::GetInterpolCommand
;
903 friend class CVC4::GetModelCommand
;
904 friend class CVC4::GetQuantifierEliminationCommand
;
905 friend class CVC4::GetUnsatCoreCommand
;
906 friend class CVC4::GetValueCommand
;
907 friend class CVC4::SetUserAttributeCommand
;
908 friend class CVC4::SimplifyCommand
;
909 friend class CVC4::SygusConstraintCommand
;
910 friend class CVC4::SygusInvConstraintCommand
;
911 friend class CVC4::SynthFunCommand
;
912 friend class CVC4::QueryCommand
;
913 friend class Datatype
;
914 friend class DatatypeConstructor
;
915 friend class DatatypeSelector
;
917 friend class Grammar
;
918 friend struct TermHashFunction
;
932 * Syntactic equality operator.
933 * Return true if both terms are syntactically identical.
934 * Both terms must belong to the same solver object.
935 * @param t the term to compare to for equality
936 * @return true if the terms are equal
938 bool operator==(const Term
& t
) const;
941 * Syntactic disequality operator.
942 * Return true if both terms differ syntactically.
943 * Both terms must belong to the same solver object.
944 * @param t the term to compare to for disequality
945 * @return true if terms are disequal
947 bool operator!=(const Term
& t
) const;
950 * Comparison for ordering on terms.
951 * @param t the term to compare to
952 * @return true if this term is less than t
954 bool operator<(const Term
& t
) const;
957 * Comparison for ordering on terms.
958 * @param t the term to compare to
959 * @return true if this term is greater than t
961 bool operator>(const Term
& t
) const;
964 * Comparison for ordering on terms.
965 * @param t the term to compare to
966 * @return true if this term is less than or equal to t
968 bool operator<=(const Term
& t
) const;
971 * Comparison for ordering on terms.
972 * @param t the term to compare to
973 * @return true if this term is greater than or equal to t
975 bool operator>=(const Term
& t
) const;
977 /** @return the number of children of this term */
978 size_t getNumChildren() const;
981 * Get the child term at a given index.
982 * @param index the index of the child term to return
983 * @return the child term with the given index
985 Term
operator[](size_t index
) const;
988 * @return the id of this term
990 uint64_t getId() const;
993 * @return the kind of this term
995 Kind
getKind() const;
998 * @return the sort of this term
1000 Sort
getSort() const;
1003 * @return the result of replacing "e" by "replacement" in this term
1005 Term
substitute(const Term
& e
, const Term
& replacement
) const;
1008 * @return the result of simulatenously replacing "es" by "replacements" in
1011 Term
substitute(const std::vector
<Term
>& es
,
1012 const std::vector
<Term
>& replacements
) const;
1015 * @return true iff this term has an operator
1020 * @return the Op used to create this term
1021 * Note: This is safe to call when hasOp() returns true.
1026 * @return true if this Term is a null term
1028 bool isNull() const;
1031 * Return the base (element stored at all indices) of a constant array
1032 * throws an exception if the kind is not CONST_ARRAY
1033 * @return the base value
1035 Term
getConstArrayBase() const;
1038 * Return the elements of a constant sequence
1039 * throws an exception if the kind is not CONST_SEQUENCE
1040 * @return the elements of the constant sequence.
1042 std::vector
<Term
> getConstSequenceElements() const;
1046 * @return the Boolean negation of this term
1048 Term
notTerm() const;
1052 * @param t a Boolean term
1053 * @return the conjunction of this term and the given term
1055 Term
andTerm(const Term
& t
) const;
1059 * @param t a Boolean term
1060 * @return the disjunction of this term and the given term
1062 Term
orTerm(const Term
& t
) const;
1065 * Boolean exclusive or.
1066 * @param t a Boolean term
1067 * @return the exclusive disjunction of this term and the given term
1069 Term
xorTerm(const Term
& t
) const;
1073 * @param t a Boolean term
1074 * @return the Boolean equivalence of this term and the given term
1076 Term
eqTerm(const Term
& t
) const;
1079 * Boolean implication.
1080 * @param t a Boolean term
1081 * @return the implication of this term and the given term
1083 Term
impTerm(const Term
& t
) const;
1086 * If-then-else with this term as the Boolean condition.
1087 * @param then_t the 'then' term
1088 * @param else_t the 'else' term
1089 * @return the if-then-else term with this term as the Boolean condition
1091 Term
iteTerm(const Term
& then_t
, const Term
& else_t
) const;
1094 * @return a string representation of this term
1096 std::string
toString() const;
1099 * Iterator for the children of a Term.
1100 * Note: This treats uninterpreted functions as Term just like any other term
1101 * for example, the term f(x, y) will have Kind APPLY_UF and three
1102 * children: f, x, and y
1104 class const_iterator
: public std::iterator
<std::input_iterator_tag
, Term
>
1116 * @param slv the associated solver object
1117 * @param e a shared pointer to the node that we're iterating over
1118 * @param p the position of the iterator (e.g. which child it's on)
1120 const_iterator(const Solver
* slv
,
1121 const std::shared_ptr
<CVC4::Node
>& e
,
1127 const_iterator(const const_iterator
& it
);
1130 * Assignment operator.
1131 * @param it the iterator to assign to
1132 * @return the reference to the iterator after assignment
1134 const_iterator
& operator=(const const_iterator
& it
);
1137 * Equality operator.
1138 * @param it the iterator to compare to for equality
1139 * @return true if the iterators are equal
1141 bool operator==(const const_iterator
& it
) const;
1144 * Disequality operator.
1145 * @param it the iterator to compare to for disequality
1146 * @return true if the iterators are disequal
1148 bool operator!=(const const_iterator
& it
) const;
1151 * Increment operator (prefix).
1152 * @return a reference to the iterator after incrementing by one
1154 const_iterator
& operator++();
1157 * Increment operator (postfix).
1158 * @return a reference to the iterator after incrementing by one
1160 const_iterator
operator++(int);
1163 * Dereference operator.
1164 * @return the term this iterator points to
1166 Term
operator*() const;
1170 * The associated solver object.
1172 const Solver
* d_solver
;
1173 /** The original node to be iterated over. */
1174 std::shared_ptr
<CVC4::Node
> d_origNode
;
1175 /** Keeps track of the iteration position. */
1180 * @return an iterator to the first child of this Term
1182 const_iterator
begin() const;
1185 * @return an iterator to one-off-the-last child of this Term
1187 const_iterator
end() const;
1190 * @return true if the term is an integer that fits within std::int32_t.
1192 bool isInt32() const;
1194 * @return the stored integer as a std::int32_t.
1195 * Note: Asserts isInt32().
1197 std::int32_t getInt32() const;
1199 * @return true if the term is an integer that fits within std::uint32_t.
1201 bool isUInt32() const;
1203 * @return the stored integer as a std::uint32_t.
1204 * Note: Asserts isUInt32().
1206 std::uint32_t getUInt32() const;
1208 * @return true if the term is an integer that fits within std::int64_t.
1210 bool isInt64() const;
1212 * @return the stored integer as a std::int64_t.
1213 * Note: Asserts isInt64().
1215 std::int64_t getInt64() const;
1217 * @return true if the term is an integer that fits within std::uint64_t.
1219 bool isUInt64() const;
1221 * @return the stored integer as a std::uint64_t.
1222 * Note: Asserts isUInt64().
1224 std::uint64_t getUInt64() const;
1226 * @return true if the term is an integer.
1228 bool isInteger() const;
1230 * @return the stored integer in (decimal) string representation.
1231 * Note: Asserts isInteger().
1233 std::string
getInteger() const;
1236 * @return true if the term is a string constant.
1238 bool isString() const;
1240 * @return the stored string constant.
1242 * Note: This method is not to be confused with toString() which returns the
1243 * term in some string representation, whatever data it may hold.
1244 * Asserts isString().
1246 std::wstring
getString() const;
1250 * The associated solver object.
1252 const Solver
* d_solver
;
1255 /** Helper to convert a vector of Terms to internal Nodes. */
1256 std::vector
<Node
> static termVectorToNodes(const std::vector
<Term
>& terms
);
1260 * @param slv the associated solver object
1261 * @param n the internal node that is to be wrapped by this term
1264 Term(const Solver
* slv
, const CVC4::Node
& n
);
1266 /** @return the internal wrapped Node of this term. */
1267 const CVC4::Node
& getNode(void) const;
1270 * Helper for isNull checks. This prevents calling an API function with
1271 * CVC4_API_CHECK_NOT_NULL
1273 bool isNullHelper() const;
1276 * Helper function that returns the kind of the term, which takes into
1277 * account special cases of the conversion for internal to external kinds.
1278 * @return the kind of this term
1280 Kind
getKindHelper() const;
1283 * @return true if the current term is a constant integer that is casted into
1284 * real using the operator CAST_TO_REAL, and returns false otherwise
1286 bool isCastedReal() const;
1288 * The internal node wrapped by this term.
1289 * Note: This is a shared_ptr rather than a unique_ptr to avoid overhead due
1290 * to memory allocation (CVC4::Node is already ref counted, so this
1291 * could be a unique_ptr instead).
1293 std::shared_ptr
<CVC4::Node
> d_node
;
1297 * Hash function for Terms.
1299 struct CVC4_PUBLIC TermHashFunction
1301 size_t operator()(const Term
& t
) const;
1305 * Serialize a term to given stream.
1306 * @param out the output stream
1307 * @param t the term to be serialized to the given output stream
1308 * @return the output stream
1310 std::ostream
& operator<<(std::ostream
& out
, const Term
& t
) CVC4_PUBLIC
;
1313 * Serialize a vector of terms to given stream.
1314 * @param out the output stream
1315 * @param vector the vector of terms to be serialized to the given stream
1316 * @return the output stream
1318 std::ostream
& operator<<(std::ostream
& out
,
1319 const std::vector
<Term
>& vector
) CVC4_PUBLIC
;
1322 * Serialize a set of terms to the given stream.
1323 * @param out the output stream
1324 * @param set the set of terms to be serialized to the given stream
1325 * @return the output stream
1327 std::ostream
& operator<<(std::ostream
& out
,
1328 const std::set
<Term
>& set
) CVC4_PUBLIC
;
1331 * Serialize an unordered_set of terms to the given stream.
1333 * @param out the output stream
1334 * @param unordered_set the set of terms to be serialized to the given stream
1335 * @return the output stream
1337 std::ostream
& operator<<(std::ostream
& out
,
1338 const std::unordered_set
<Term
, TermHashFunction
>&
1339 unordered_set
) CVC4_PUBLIC
;
1342 * Serialize a map of terms to the given stream.
1344 * @param out the output stream
1345 * @param map the map of terms to be serialized to the given stream
1346 * @return the output stream
1348 template <typename V
>
1349 std::ostream
& operator<<(std::ostream
& out
,
1350 const std::map
<Term
, V
>& map
) CVC4_PUBLIC
;
1353 * Serialize an unordered_map of terms to the given stream.
1355 * @param out the output stream
1356 * @param unordered_map the map of terms to be serialized to the given stream
1357 * @return the output stream
1359 template <typename V
>
1360 std::ostream
& operator<<(std::ostream
& out
,
1361 const std::unordered_map
<Term
, V
, TermHashFunction
>&
1362 unordered_map
) CVC4_PUBLIC
;
1365 * Serialize an operator to given stream.
1366 * @param out the output stream
1367 * @param t the operator to be serialized to the given output stream
1368 * @return the output stream
1370 std::ostream
& operator<<(std::ostream
& out
, const Op
& t
) CVC4_PUBLIC
;
1373 * Hash function for Ops.
1375 struct CVC4_PUBLIC OpHashFunction
1377 size_t operator()(const Op
& t
) const;
1380 /* -------------------------------------------------------------------------- */
1382 /* -------------------------------------------------------------------------- */
1384 class DatatypeConstructorIterator
;
1385 class DatatypeIterator
;
1388 * A CVC4 datatype constructor declaration.
1390 class CVC4_PUBLIC DatatypeConstructorDecl
1392 friend class DatatypeDecl
;
1393 friend class Solver
;
1397 DatatypeConstructorDecl();
1402 ~DatatypeConstructorDecl();
1405 * Add datatype selector declaration.
1406 * @param name the name of the datatype selector declaration to add
1407 * @param sort the range sort of the datatype selector declaration to add
1409 void addSelector(const std::string
& name
, const Sort
& sort
);
1411 * Add datatype selector declaration whose range type is the datatype itself.
1412 * @param name the name of the datatype selector declaration to add
1414 void addSelectorSelf(const std::string
& name
);
1417 * @return a string representation of this datatype constructor declaration
1419 std::string
toString() const;
1424 * @param slv the associated solver object
1425 * @param name the name of the datatype constructor
1426 * @return the DatatypeConstructorDecl
1428 DatatypeConstructorDecl(const Solver
* slv
, const std::string
& name
);
1431 * The associated solver object.
1433 const Solver
* d_solver
;
1436 * The internal (intermediate) datatype constructor wrapped by this
1437 * datatype constructor declaration.
1438 * Note: This is a shared_ptr rather than a unique_ptr since
1439 * CVC4::DTypeConstructor is not ref counted.
1441 std::shared_ptr
<CVC4::DTypeConstructor
> d_ctor
;
1447 * A CVC4 datatype declaration.
1449 class CVC4_PUBLIC DatatypeDecl
1451 friend class DatatypeConstructorArg
;
1452 friend class Solver
;
1453 friend class Grammar
;
1465 * Add datatype constructor declaration.
1466 * @param ctor the datatype constructor declaration to add
1468 void addConstructor(const DatatypeConstructorDecl
& ctor
);
1470 /** Get the number of constructors (so far) for this Datatype declaration. */
1471 size_t getNumConstructors() const;
1473 /** Is this Datatype declaration parametric? */
1474 bool isParametric() const;
1477 * @return true if this DatatypeDecl is a null object
1479 bool isNull() const;
1482 * @return a string representation of this datatype declaration
1484 std::string
toString() const;
1486 /** @return the name of this datatype declaration. */
1487 std::string
getName() const;
1492 * @param slv the associated solver object
1493 * @param name the name of the datatype
1494 * @param isCoDatatype true if a codatatype is to be constructed
1495 * @return the DatatypeDecl
1497 DatatypeDecl(const Solver
* slv
,
1498 const std::string
& name
,
1499 bool isCoDatatype
= false);
1502 * Constructor for parameterized datatype declaration.
1503 * Create sorts parameter with Solver::mkParamSort().
1504 * @param slv the associated solver object
1505 * @param name the name of the datatype
1506 * @param param the sort parameter
1507 * @param isCoDatatype true if a codatatype is to be constructed
1509 DatatypeDecl(const Solver
* slv
,
1510 const std::string
& name
,
1512 bool isCoDatatype
= false);
1515 * Constructor for parameterized datatype declaration.
1516 * Create sorts parameter with Solver::mkParamSort().
1517 * @param slv the associated solver object
1518 * @param name the name of the datatype
1519 * @param params a list of sort parameters
1520 * @param isCoDatatype true if a codatatype is to be constructed
1522 DatatypeDecl(const Solver
* slv
,
1523 const std::string
& name
,
1524 const std::vector
<Sort
>& params
,
1525 bool isCoDatatype
= false);
1527 /** @return the internal wrapped Dtype of this datatype declaration. */
1528 CVC4::DType
& getDatatype(void) const;
1531 * Helper for isNull checks. This prevents calling an API function with
1532 * CVC4_API_CHECK_NOT_NULL
1534 bool isNullHelper() const;
1537 * The associated solver object.
1539 const Solver
* d_solver
;
1542 * The internal (intermediate) datatype wrapped by this datatype
1544 * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1547 std::shared_ptr
<CVC4::DType
> d_dtype
;
1551 * A CVC4 datatype selector.
1553 class CVC4_PUBLIC DatatypeSelector
1555 friend class DatatypeConstructor
;
1556 friend class Solver
;
1567 ~DatatypeSelector();
1569 /** @return the name of this Datatype selector. */
1570 std::string
getName() const;
1573 * Get the selector operator of this datatype selector.
1574 * @return the selector term
1576 Term
getSelectorTerm() const;
1578 /** @return the range sort of this argument. */
1579 Sort
getRangeSort() const;
1582 * @return a string representation of this datatype selector
1584 std::string
toString() const;
1589 * @param slv the associated solver object
1590 * @param stor the internal datatype selector to be wrapped
1591 * @return the DatatypeSelector
1593 DatatypeSelector(const Solver
* slv
, const CVC4::DTypeSelector
& stor
);
1596 * The associated solver object.
1598 const Solver
* d_solver
;
1601 * The internal datatype selector wrapped by this datatype selector.
1602 * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1605 std::shared_ptr
<CVC4::DTypeSelector
> d_stor
;
1609 * A CVC4 datatype constructor.
1611 class CVC4_PUBLIC DatatypeConstructor
1613 friend class Datatype
;
1614 friend class Solver
;
1620 DatatypeConstructor();
1625 ~DatatypeConstructor();
1627 /** @return the name of this Datatype constructor. */
1628 std::string
getName() const;
1631 * Get the constructor operator of this datatype constructor.
1632 * @return the constructor term
1634 Term
getConstructorTerm() const;
1637 * Get the constructor operator of this datatype constructor whose return
1638 * type is retSort. This method is intended to be used on constructors of
1639 * parametric datatypes and can be seen as returning the constructor
1640 * term that has been explicitly cast to the given sort.
1642 * This method is required for constructors of parametric datatypes whose
1643 * return type cannot be determined by type inference. For example, given:
1644 * (declare-datatype List (par (T) ((nil) (cons (head T) (tail (List T))))))
1645 * The type of nil terms need to be provided by the user. In SMT version 2.6,
1646 * this is done via the syntax for qualified identifiers:
1647 * (as nil (List Int))
1648 * This method is equivalent of applying the above, where this
1649 * DatatypeConstructor is the one corresponding to nil, and retSort is
1652 * Furthermore note that the returned constructor term t is an operator,
1653 * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
1654 * (nullary) application of nil.
1656 * @param retSort the desired return sort of the constructor
1657 * @return the constructor term
1659 Term
getSpecializedConstructorTerm(const Sort
& retSort
) const;
1662 * Get the tester operator of this datatype constructor.
1663 * @return the tester operator
1665 Term
getTesterTerm() const;
1668 * @return the number of selectors (so far) of this Datatype constructor.
1670 size_t getNumSelectors() const;
1672 /** @return the i^th DatatypeSelector. */
1673 DatatypeSelector
operator[](size_t index
) const;
1675 * Get the datatype selector with the given name.
1676 * This is a linear search through the selectors, so in case of
1677 * multiple, similarly-named selectors, the first is returned.
1678 * @param name the name of the datatype selector
1679 * @return the first datatype selector with the given name
1681 DatatypeSelector
operator[](const std::string
& name
) const;
1682 DatatypeSelector
getSelector(const std::string
& name
) const;
1685 * Get the term representation of the datatype selector with the given name.
1686 * This is a linear search through the arguments, so in case of multiple,
1687 * similarly-named arguments, the selector for the first is returned.
1688 * @param name the name of the datatype selector
1689 * @return a term representing the datatype selector with the given name
1691 Term
getSelectorTerm(const std::string
& name
) const;
1694 * @return a string representation of this datatype constructor
1696 std::string
toString() const;
1699 * Iterator for the selectors of a datatype constructor.
1701 class const_iterator
1702 : public std::iterator
<std::input_iterator_tag
, DatatypeConstructor
>
1704 friend class DatatypeConstructor
; // to access constructor
1707 /** Nullary constructor (required for Cython). */
1711 * Assignment operator.
1712 * @param it the iterator to assign to
1713 * @return the reference to the iterator after assignment
1715 const_iterator
& operator=(const const_iterator
& it
);
1718 * Equality operator.
1719 * @param it the iterator to compare to for equality
1720 * @return true if the iterators are equal
1722 bool operator==(const const_iterator
& it
) const;
1725 * Disequality operator.
1726 * @param it the iterator to compare to for disequality
1727 * @return true if the iterators are disequal
1729 bool operator!=(const const_iterator
& it
) const;
1732 * Increment operator (prefix).
1733 * @return a reference to the iterator after incrementing by one
1735 const_iterator
& operator++();
1738 * Increment operator (postfix).
1739 * @return a reference to the iterator after incrementing by one
1741 const_iterator
operator++(int);
1744 * Dereference operator.
1745 * @return a reference to the selector this iterator points to
1747 const DatatypeSelector
& operator*() const;
1750 * Dereference operator.
1751 * @return a pointer to the selector this iterator points to
1753 const DatatypeSelector
* operator->() const;
1758 * @param slv the associated Solver object
1759 * @param ctor the internal datatype constructor to iterate over
1760 * @param true if this is a begin() iterator
1762 const_iterator(const Solver
* slv
,
1763 const CVC4::DTypeConstructor
& ctor
,
1767 * The associated solver object.
1769 const Solver
* d_solver
;
1772 * A pointer to the list of selectors of the internal datatype
1773 * constructor to iterate over.
1774 * This pointer is maintained for operators == and != only.
1776 const void* d_int_stors
;
1778 /** The list of datatype selector (wrappers) to iterate over. */
1779 std::vector
<DatatypeSelector
> d_stors
;
1781 /** The current index of the iterator. */
1786 * @return an iterator to the first selector of this constructor
1788 const_iterator
begin() const;
1791 * @return an iterator to one-off-the-last selector of this constructor
1793 const_iterator
end() const;
1798 * @param ctor the internal datatype constructor to be wrapped
1799 * @return the DatatypeConstructor
1801 DatatypeConstructor(const Solver
* slv
, const CVC4::DTypeConstructor
& ctor
);
1804 * Return selector for name.
1805 * @param name The name of selector to find
1806 * @return the selector object for the name
1808 DatatypeSelector
getSelectorForName(const std::string
& name
) const;
1811 * The associated solver object.
1813 const Solver
* d_solver
;
1816 * The internal datatype constructor wrapped by this datatype constructor.
1817 * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
1820 std::shared_ptr
<CVC4::DTypeConstructor
> d_ctor
;
1826 class CVC4_PUBLIC Datatype
1828 friend class Solver
;
1841 * Get the datatype constructor at a given index.
1842 * @param idx the index of the datatype constructor to return
1843 * @return the datatype constructor with the given index
1845 DatatypeConstructor
operator[](size_t idx
) const;
1848 * Get the datatype constructor with the given name.
1849 * This is a linear search through the constructors, so in case of multiple,
1850 * similarly-named constructors, the first is returned.
1851 * @param name the name of the datatype constructor
1852 * @return the datatype constructor with the given name
1854 DatatypeConstructor
operator[](const std::string
& name
) const;
1855 DatatypeConstructor
getConstructor(const std::string
& name
) const;
1858 * Get a term representing the datatype constructor with the given name.
1859 * This is a linear search through the constructors, so in case of multiple,
1860 * similarly-named constructors, the
1861 * first is returned.
1863 Term
getConstructorTerm(const std::string
& name
) const;
1865 /** @return the name of this Datatype. */
1866 std::string
getName() const;
1868 /** @return the number of constructors for this Datatype. */
1869 size_t getNumConstructors() const;
1871 /** @return true if this datatype is parametric */
1872 bool isParametric() const;
1874 /** @return true if this datatype corresponds to a co-datatype */
1875 bool isCodatatype() const;
1877 /** @return true if this datatype corresponds to a tuple */
1878 bool isTuple() const;
1880 /** @return true if this datatype corresponds to a record */
1881 bool isRecord() const;
1883 /** @return true if this datatype is finite */
1884 bool isFinite() const;
1887 * Is this datatype well-founded? If this datatype is not a codatatype,
1888 * this returns false if there are no values of this datatype that are of
1891 * @return true if this datatype is well-founded
1893 bool isWellFounded() const;
1896 * Does this datatype have nested recursion? This method returns false if a
1897 * value of this datatype includes a subterm of its type that is nested
1898 * beneath a non-datatype type constructor. For example, a datatype
1899 * T containing a constructor having a selector with range type (Set T) has
1902 * @return true if this datatype has nested recursion
1904 bool hasNestedRecursion() const;
1907 * @return a string representation of this datatype
1909 std::string
toString() const;
1912 * Iterator for the constructors of a datatype.
1914 class const_iterator
: public std::iterator
<std::input_iterator_tag
, Datatype
>
1916 friend class Datatype
; // to access constructor
1919 /** Nullary constructor (required for Cython). */
1923 * Assignment operator.
1924 * @param it the iterator to assign to
1925 * @return the reference to the iterator after assignment
1927 const_iterator
& operator=(const const_iterator
& it
);
1930 * Equality operator.
1931 * @param it the iterator to compare to for equality
1932 * @return true if the iterators are equal
1934 bool operator==(const const_iterator
& it
) const;
1937 * Disequality operator.
1938 * @param it the iterator to compare to for disequality
1939 * @return true if the iterators are disequal
1941 bool operator!=(const const_iterator
& it
) const;
1944 * Increment operator (prefix).
1945 * @return a reference to the iterator after incrementing by one
1947 const_iterator
& operator++();
1950 * Increment operator (postfix).
1951 * @return a reference to the iterator after incrementing by one
1953 const_iterator
operator++(int);
1956 * Dereference operator.
1957 * @return a reference to the constructor this iterator points to
1959 const DatatypeConstructor
& operator*() const;
1962 * Dereference operator.
1963 * @return a pointer to the constructor this iterator points to
1965 const DatatypeConstructor
* operator->() const;
1970 * @param slv the associated Solver object
1971 * @param dtype the internal datatype to iterate over
1972 * @param true if this is a begin() iterator
1974 const_iterator(const Solver
* slv
, const CVC4::DType
& dtype
, bool begin
);
1977 * The associated solver object.
1979 const Solver
* d_solver
;
1982 * A pointer to the list of constructors of the internal datatype
1984 * This pointer is maintained for operators == and != only.
1986 const void* d_int_ctors
;
1988 /** The list of datatype constructor (wrappers) to iterate over. */
1989 std::vector
<DatatypeConstructor
> d_ctors
;
1991 /** The current index of the iterator. */
1996 * @return an iterator to the first constructor of this datatype
1998 const_iterator
begin() const;
2001 * @return an iterator to one-off-the-last constructor of this datatype
2003 const_iterator
end() const;
2008 * @param dtype the internal datatype to be wrapped
2009 * @return the Datatype
2011 Datatype(const Solver
* slv
, const CVC4::DType
& dtype
);
2014 * Return constructor for name.
2015 * @param name The name of constructor to find
2016 * @return the constructor object for the name
2018 DatatypeConstructor
getConstructorForName(const std::string
& name
) const;
2021 * The associated solver object.
2023 const Solver
* d_solver
;
2026 * The internal datatype wrapped by this datatype.
2027 * Note: This is a shared_ptr rather than a unique_ptr since CVC4::DType is
2030 std::shared_ptr
<CVC4::DType
> d_dtype
;
2034 * Serialize a datatype declaration to given stream.
2035 * @param out the output stream
2036 * @param dtdecl the datatype declaration to be serialized to the given stream
2037 * @return the output stream
2039 std::ostream
& operator<<(std::ostream
& out
,
2040 const DatatypeDecl
& dtdecl
) CVC4_PUBLIC
;
2043 * Serialize a datatype constructor declaration to given stream.
2044 * @param out the output stream
2045 * @param ctordecl the datatype constructor declaration to be serialized
2046 * @return the output stream
2048 std::ostream
& operator<<(std::ostream
& out
,
2049 const DatatypeConstructorDecl
& ctordecl
) CVC4_PUBLIC
;
2052 * Serialize a vector of datatype constructor declarations to given stream.
2053 * @param out the output stream
2054 * @param vector the vector of datatype constructor declarations to be
2055 * serialized to the given stream
2056 * @return the output stream
2058 std::ostream
& operator<<(std::ostream
& out
,
2059 const std::vector
<DatatypeConstructorDecl
>& vector
);
2062 * Serialize a datatype to given stream.
2063 * @param out the output stream
2064 * @param dtdecl the datatype to be serialized to given stream
2065 * @return the output stream
2067 std::ostream
& operator<<(std::ostream
& out
, const Datatype
& dtype
) CVC4_PUBLIC
;
2070 * Serialize a datatype constructor to given stream.
2071 * @param out the output stream
2072 * @param ctor the datatype constructor to be serialized to given stream
2073 * @return the output stream
2075 std::ostream
& operator<<(std::ostream
& out
,
2076 const DatatypeConstructor
& ctor
) CVC4_PUBLIC
;
2079 * Serialize a datatype selector to given stream.
2080 * @param out the output stream
2081 * @param ctor the datatype selector to be serialized to given stream
2082 * @return the output stream
2084 std::ostream
& operator<<(std::ostream
& out
,
2085 const DatatypeSelector
& stor
) CVC4_PUBLIC
;
2087 /* -------------------------------------------------------------------------- */
2089 /* -------------------------------------------------------------------------- */
2094 class CVC4_PUBLIC Grammar
2096 friend class CVC4::GetAbductCommand
;
2097 friend class CVC4::GetInterpolCommand
;
2098 friend class CVC4::SynthFunCommand
;
2099 friend class Solver
;
2103 * Add <rule> to the set of rules corresponding to <ntSymbol>.
2104 * @param ntSymbol the non-terminal to which the rule is added
2105 * @param rule the rule to add
2107 void addRule(const Term
& ntSymbol
, const Term
& rule
);
2110 * Add <rules> to the set of rules corresponding to <ntSymbol>.
2111 * @param ntSymbol the non-terminal to which the rules are added
2112 * @param rule the rules to add
2114 void addRules(const Term
& ntSymbol
, const std::vector
<Term
>& rules
);
2117 * Allow <ntSymbol> to be an arbitrary constant.
2118 * @param ntSymbol the non-terminal allowed to be any constant
2120 void addAnyConstant(const Term
& ntSymbol
);
2123 * Allow <ntSymbol> to be any input variable to corresponding
2124 * synth-fun/synth-inv with the same sort as <ntSymbol>.
2125 * @param ntSymbol the non-terminal allowed to be any input constant
2127 void addAnyVariable(const Term
& ntSymbol
);
2130 * @return a string representation of this grammar.
2132 std::string
toString() const;
2135 * Nullary constructor. Needed for the Cython API.
2142 * @param slv the solver that created this grammar
2143 * @param sygusVars the input variables to synth-fun/synth-var
2144 * @param ntSymbols the non-terminals of this grammar
2146 Grammar(const Solver
* slv
,
2147 const std::vector
<Term
>& sygusVars
,
2148 const std::vector
<Term
>& ntSymbols
);
2151 * @return the resolved datatype of the Start symbol of the grammar
2156 * Adds a constructor to sygus datatype <dt> whose sygus operator is <term>.
2158 * <ntsToUnres> contains a mapping from non-terminal symbols to the
2159 * unresolved sorts they correspond to. This map indicates how the argument
2160 * <term> should be interpreted (instances of symbols from the domain of
2161 * <ntsToUnres> correspond to constructor arguments).
2163 * The sygus operator that is actually added to <dt> corresponds to replacing
2164 * each occurrence of non-terminal symbols from the domain of <ntsToUnres>
2165 * with bound variables via purifySygusGTerm, and binding these variables
2168 * @param dt the non-terminal's datatype to which a constructor is added
2169 * @param term the sygus operator of the constructor
2170 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2172 void addSygusConstructorTerm(
2175 const std::unordered_map
<Term
, Sort
, TermHashFunction
>& ntsToUnres
) const;
2178 * Purify SyGuS grammar term.
2180 * This returns a term where all occurrences of non-terminal symbols (those
2181 * in the domain of <ntsToUnres>) are replaced by fresh variables. For
2182 * each variable replaced in this way, we add the fresh variable it is
2183 * replaced with to <args>, and the unresolved sorts corresponding to the
2184 * non-terminal symbol to <cargs> (constructor args). In other words, <args>
2185 * contains the free variables in the term returned by this method (which
2186 * should be bound by a lambda), and <cargs> contains the sorts of the
2187 * arguments of the sygus constructor.
2189 * @param term the term to purify
2190 * @param args the free variables in the term returned by this method
2191 * @param cargs the sorts of the arguments of the sygus constructor
2192 * @param ntsToUnres mapping from non-terminals to their unresolved sorts
2193 * @return the purfied term
2195 Term
purifySygusGTerm(
2197 std::vector
<Term
>& args
,
2198 std::vector
<Sort
>& cargs
,
2199 const std::unordered_map
<Term
, Sort
, TermHashFunction
>& ntsToUnres
) const;
2202 * This adds constructors to <dt> for sygus variables in <d_sygusVars> whose
2203 * sort is argument <sort>. This method should be called when the sygus
2204 * grammar term (Variable sort) is encountered.
2206 * @param dt the non-terminal's datatype to which the constructors are added
2207 * @param sort the sort of the sygus variables to add
2209 void addSygusConstructorVariables(DatatypeDecl
& dt
, const Sort
& sort
) const;
2211 /** The solver that created this grammar. */
2212 const Solver
* d_solver
;
2213 /** Input variables to the corresponding function/invariant to synthesize.*/
2214 std::vector
<Term
> d_sygusVars
;
2215 /** The non-terminal symbols of this grammar. */
2216 std::vector
<Term
> d_ntSyms
;
2217 /** The mapping from non-terminal symbols to their production terms. */
2218 std::unordered_map
<Term
, std::vector
<Term
>, TermHashFunction
> d_ntsToTerms
;
2219 /** The set of non-terminals that can be arbitrary constants. */
2220 std::unordered_set
<Term
, TermHashFunction
> d_allowConst
;
2221 /** The set of non-terminals that can be sygus variables. */
2222 std::unordered_set
<Term
, TermHashFunction
> d_allowVars
;
2223 /** Did we call resolve() before? */
2228 * Serialize a grammar to given stream.
2229 * @param out the output stream
2230 * @param g the grammar to be serialized to the given output stream
2231 * @return the output stream
2233 std::ostream
& operator<<(std::ostream
& out
, const Grammar
& g
) CVC4_PUBLIC
;
2235 /* -------------------------------------------------------------------------- */
2236 /* Rounding Mode for Floating Points */
2237 /* -------------------------------------------------------------------------- */
2240 * A CVC4 floating point rounding mode.
2242 enum CVC4_PUBLIC RoundingMode
2244 ROUND_NEAREST_TIES_TO_EVEN
,
2245 ROUND_TOWARD_POSITIVE
,
2246 ROUND_TOWARD_NEGATIVE
,
2248 ROUND_NEAREST_TIES_TO_AWAY
,
2252 * Hash function for RoundingModes.
2254 struct CVC4_PUBLIC RoundingModeHashFunction
2256 inline size_t operator()(const RoundingMode
& rm
) const;
2259 /* -------------------------------------------------------------------------- */
2261 /* -------------------------------------------------------------------------- */
2266 class CVC4_PUBLIC Solver
2268 friend class Datatype
;
2269 friend class DatatypeDecl
;
2270 friend class DatatypeConstructor
;
2271 friend class DatatypeConstructorDecl
;
2272 friend class DatatypeSelector
;
2273 friend class Grammar
;
2279 /* .................................................................... */
2280 /* Constructors/Destructors */
2281 /* .................................................................... */
2285 * @param opts an optional pointer to a solver options object
2286 * @return the Solver
2288 Solver(Options
* opts
= nullptr);
2296 * Disallow copy/assignment.
2298 Solver(const Solver
&) = delete;
2299 Solver
& operator=(const Solver
&) = delete;
2301 /* .................................................................... */
2302 /* Solver Configuration */
2303 /* .................................................................... */
2305 bool supportsFloatingPoint() const;
2307 /* .................................................................... */
2308 /* Sorts Handling */
2309 /* .................................................................... */
2314 Sort
getNullSort() const;
2317 * @return sort Boolean
2319 Sort
getBooleanSort() const;
2322 * @return sort Integer (in CVC4, Integer is a subtype of Real)
2324 Sort
getIntegerSort() const;
2329 Sort
getRealSort() const;
2332 * @return sort RegExp
2334 Sort
getRegExpSort() const;
2337 * @return sort RoundingMode
2339 Sort
getRoundingModeSort() const;
2342 * @return sort String
2344 Sort
getStringSort() const;
2347 * Create an array sort.
2348 * @param indexSort the array index sort
2349 * @param elemSort the array element sort
2350 * @return the array sort
2352 Sort
mkArraySort(const Sort
& indexSort
, const Sort
& elemSort
) const;
2355 * Create a bit-vector sort.
2356 * @param size the bit-width of the bit-vector sort
2357 * @return the bit-vector sort
2359 Sort
mkBitVectorSort(uint32_t size
) const;
2362 * Create a floating-point sort.
2363 * @param exp the bit-width of the exponent of the floating-point sort.
2364 * @param sig the bit-width of the significand of the floating-point sort.
2366 Sort
mkFloatingPointSort(uint32_t exp
, uint32_t sig
) const;
2369 * Create a datatype sort.
2370 * @param dtypedecl the datatype declaration from which the sort is created
2371 * @return the datatype sort
2373 Sort
mkDatatypeSort(const DatatypeDecl
& dtypedecl
) const;
2376 * Create a vector of datatype sorts. The names of the datatype declarations
2379 * @param dtypedecls the datatype declarations from which the sort is created
2380 * @return the datatype sorts
2382 std::vector
<Sort
> mkDatatypeSorts(
2383 const std::vector
<DatatypeDecl
>& dtypedecls
) const;
2386 * Create a vector of datatype sorts using unresolved sorts. The names of
2387 * the datatype declarations in dtypedecls must be distinct.
2389 * This method is called when the DatatypeDecl objects dtypedecls have been
2390 * built using "unresolved" sorts.
2392 * We associate each sort in unresolvedSorts with exacly one datatype from
2393 * dtypedecls. In particular, it must have the same name as exactly one
2394 * datatype declaration in dtypedecls.
2396 * When constructing datatypes, unresolved sorts are replaced by the datatype
2397 * sort constructed for the datatype declaration it is associated with.
2399 * @param dtypedecls the datatype declarations from which the sort is created
2400 * @param unresolvedSorts the list of unresolved sorts
2401 * @return the datatype sorts
2403 std::vector
<Sort
> mkDatatypeSorts(
2404 const std::vector
<DatatypeDecl
>& dtypedecls
,
2405 const std::set
<Sort
>& unresolvedSorts
) const;
2408 * Create function sort.
2409 * @param domain the sort of the fuction argument
2410 * @param codomain the sort of the function return value
2411 * @return the function sort
2413 Sort
mkFunctionSort(const Sort
& domain
, const Sort
& codomain
) const;
2416 * Create function sort.
2417 * @param sorts the sort of the function arguments
2418 * @param codomain the sort of the function return value
2419 * @return the function sort
2421 Sort
mkFunctionSort(const std::vector
<Sort
>& sorts
,
2422 const Sort
& codomain
) const;
2425 * Create a sort parameter.
2426 * @param symbol the name of the sort
2427 * @return the sort parameter
2429 Sort
mkParamSort(const std::string
& symbol
) const;
2432 * Create a predicate sort.
2433 * @param sorts the list of sorts of the predicate
2434 * @return the predicate sort
2436 Sort
mkPredicateSort(const std::vector
<Sort
>& sorts
) const;
2439 * Create a record sort
2440 * @param fields the list of fields of the record
2441 * @return the record sort
2444 const std::vector
<std::pair
<std::string
, Sort
>>& fields
) const;
2447 * Create a set sort.
2448 * @param elemSort the sort of the set elements
2449 * @return the set sort
2451 Sort
mkSetSort(const Sort
& elemSort
) const;
2454 * Create a bag sort.
2455 * @param elemSort the sort of the bag elements
2456 * @return the bag sort
2458 Sort
mkBagSort(const Sort
& elemSort
) const;
2461 * Create a sequence sort.
2462 * @param elemSort the sort of the sequence elements
2463 * @return the sequence sort
2465 Sort
mkSequenceSort(const Sort
& elemSort
) const;
2468 * Create an uninterpreted sort.
2469 * @param symbol the name of the sort
2470 * @return the uninterpreted sort
2472 Sort
mkUninterpretedSort(const std::string
& symbol
) const;
2475 * Create a sort constructor sort.
2476 * @param symbol the symbol of the sort
2477 * @param arity the arity of the sort
2478 * @return the sort constructor sort
2480 Sort
mkSortConstructorSort(const std::string
& symbol
, size_t arity
) const;
2483 * Create a tuple sort.
2484 * @param sorts of the elements of the tuple
2485 * @return the tuple sort
2487 Sort
mkTupleSort(const std::vector
<Sort
>& sorts
) const;
2489 /* .................................................................... */
2491 /* .................................................................... */
2494 * Create 0-ary term of given kind.
2495 * @param kind the kind of the term
2498 Term
mkTerm(Kind kind
) const;
2501 * Create a unary term of given kind.
2502 * @param kind the kind of the term
2503 * @param child the child of the term
2506 Term
mkTerm(Kind kind
, const Term
& child
) const;
2509 * Create binary term of given kind.
2510 * @param kind the kind of the term
2511 * @param child1 the first child of the term
2512 * @param child2 the second child of the term
2515 Term
mkTerm(Kind kind
, const Term
& child1
, const Term
& child2
) const;
2518 * Create ternary term of given kind.
2519 * @param kind the kind of the term
2520 * @param child1 the first child of the term
2521 * @param child2 the second child of the term
2522 * @param child3 the third child of the term
2525 Term
mkTerm(Kind kind
,
2528 const Term
& child3
) const;
2531 * Create n-ary term of given kind.
2532 * @param kind the kind of the term
2533 * @param children the children of the term
2536 Term
mkTerm(Kind kind
, const std::vector
<Term
>& children
) const;
2539 * Create nullary term of given kind from a given operator.
2540 * Create operators with mkOp().
2541 * @param the operator
2544 Term
mkTerm(const Op
& op
) const;
2547 * Create unary term of given kind from a given operator.
2548 * Create operators with mkOp().
2549 * @param the operator
2550 * @child the child of the term
2553 Term
mkTerm(const Op
& op
, const Term
& child
) const;
2556 * Create binary term of given kind from a given operator.
2557 * Create operators with mkOp().
2558 * @param the operator
2559 * @child1 the first child of the term
2560 * @child2 the second child of the term
2563 Term
mkTerm(const Op
& op
, const Term
& child1
, const Term
& child2
) const;
2566 * Create ternary term of given kind from a given operator.
2567 * Create operators with mkOp().
2568 * @param the operator
2569 * @child1 the first child of the term
2570 * @child2 the second child of the term
2571 * @child3 the third child of the term
2574 Term
mkTerm(const Op
& op
,
2577 const Term
& child3
) const;
2580 * Create n-ary term of given kind from a given operator.
2581 * Create operators with mkOp().
2582 * @param op the operator
2583 * @children the children of the term
2586 Term
mkTerm(const Op
& op
, const std::vector
<Term
>& children
) const;
2589 * Create a tuple term. Terms are automatically converted if sorts are
2591 * @param sorts The sorts of the elements in the tuple
2592 * @param terms The elements in the tuple
2593 * @return the tuple Term
2595 Term
mkTuple(const std::vector
<Sort
>& sorts
,
2596 const std::vector
<Term
>& terms
) const;
2598 /* .................................................................... */
2599 /* Create Operators */
2600 /* .................................................................... */
2603 * Create an operator for a builtin Kind
2604 * The Kind may not be the Kind for an indexed operator
2605 * (e.g. BITVECTOR_EXTRACT)
2606 * Note: in this case, the Op simply wraps the Kind.
2607 * The Kind can be used in mkTerm directly without
2608 * creating an op first.
2609 * @param kind the kind to wrap
2611 Op
mkOp(Kind kind
) const;
2614 * Create operator of kind:
2616 * - DIVISIBLE (to support arbitrary precision integers)
2617 * See enum Kind for a description of the parameters.
2618 * @param kind the kind of the operator
2619 * @param arg the string argument to this operator
2621 Op
mkOp(Kind kind
, const std::string
& arg
) const;
2624 * Create operator of kind:
2626 * - BITVECTOR_REPEAT
2627 * - BITVECTOR_ZERO_EXTEND
2628 * - BITVECTOR_SIGN_EXTEND
2629 * - BITVECTOR_ROTATE_LEFT
2630 * - BITVECTOR_ROTATE_RIGHT
2631 * - INT_TO_BITVECTOR
2632 * - FLOATINGPOINT_TO_UBV
2633 * - FLOATINGPOINT_TO_UBV_TOTAL
2634 * - FLOATINGPOINT_TO_SBV
2635 * - FLOATINGPOINT_TO_SBV_TOTAL
2637 * See enum Kind for a description of the parameters.
2638 * @param kind the kind of the operator
2639 * @param arg the uint32_t argument to this operator
2641 Op
mkOp(Kind kind
, uint32_t arg
) const;
2644 * Create operator of Kind:
2645 * - BITVECTOR_EXTRACT
2646 * - FLOATINGPOINT_TO_FP_IEEE_BITVECTOR
2647 * - FLOATINGPOINT_TO_FP_FLOATINGPOINT
2648 * - FLOATINGPOINT_TO_FP_REAL
2649 * - FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR
2650 * - FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR
2651 * - FLOATINGPOINT_TO_FP_GENERIC
2652 * See enum Kind for a description of the parameters.
2653 * @param kind the kind of the operator
2654 * @param arg1 the first uint32_t argument to this operator
2655 * @param arg2 the second uint32_t argument to this operator
2657 Op
mkOp(Kind kind
, uint32_t arg1
, uint32_t arg2
) const;
2660 * Create operator of Kind:
2662 * See enum Kind for a description of the parameters.
2663 * @param kind the kind of the operator
2665 Op
mkOp(Kind kind
, const std::vector
<uint32_t>& args
) const;
2667 /* .................................................................... */
2668 /* Create Constants */
2669 /* .................................................................... */
2672 * Create a Boolean true constant.
2673 * @return the true constant
2675 Term
mkTrue() const;
2678 * Create a Boolean false constant.
2679 * @return the false constant
2681 Term
mkFalse() const;
2684 * Create a Boolean constant.
2685 * @return the Boolean constant
2686 * @param val the value of the constant
2688 Term
mkBoolean(bool val
) const;
2691 * Create a constant representing the number Pi.
2692 * @return a constant representing Pi
2696 * Create an integer constant from a string.
2697 * @param s the string representation of the constant, may represent an
2698 * integer (e.g., "123").
2699 * @return a constant of sort Integer assuming 's' represents an integer)
2701 Term
mkInteger(const std::string
& s
) const;
2704 * Create an integer constant from a c++ int.
2705 * @param val the value of the constant
2706 * @return a constant of sort Integer
2708 Term
mkInteger(int64_t val
) const;
2711 * Create a real constant from a string.
2712 * @param s the string representation of the constant, may represent an
2713 * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34").
2714 * @return a constant of sort Real
2716 Term
mkReal(const std::string
& s
) const;
2719 * Create a real constant from an integer.
2720 * @param val the value of the constant
2721 * @return a constant of sort Integer
2723 Term
mkReal(int64_t val
) const;
2726 * Create a real constant from a rational.
2727 * @param num the value of the numerator
2728 * @param den the value of the denominator
2729 * @return a constant of sort Real
2731 Term
mkReal(int64_t num
, int64_t den
) const;
2734 * Create a regular expression empty term.
2735 * @return the empty term
2737 Term
mkRegexpEmpty() const;
2740 * Create a regular expression sigma term.
2741 * @return the sigma term
2743 Term
mkRegexpSigma() const;
2746 * Create a constant representing an empty set of the given sort.
2747 * @param s the sort of the set elements.
2748 * @return the empty set constant
2750 Term
mkEmptySet(const Sort
& s
) const;
2753 * Create a constant representing an empty bag of the given sort.
2754 * @param s the sort of the bag elements.
2755 * @return the empty bag constant
2757 Term
mkEmptyBag(const Sort
& s
) const;
2760 * Create a separation logic nil term.
2761 * @param sort the sort of the nil term
2762 * @return the separation logic nil term
2764 Term
mkSepNil(const Sort
& sort
) const;
2767 * Create a String constant.
2768 * @param s the string this constant represents
2769 * @param useEscSequences determines whether escape sequences in \p s should
2770 * be converted to the corresponding character
2771 * @return the String constant
2773 Term
mkString(const std::string
& s
, bool useEscSequences
= false) const;
2776 * Create a String constant.
2777 * @param c the character this constant represents
2778 * @return the String constant
2780 Term
mkString(const unsigned char c
) const;
2783 * Create a String constant.
2784 * @param s a list of unsigned values this constant represents as string
2785 * @return the String constant
2787 Term
mkString(const std::vector
<unsigned>& s
) const;
2790 * Create a character constant from a given string.
2791 * @param s the string denoting the code point of the character (in base 16)
2792 * @return the character constant
2794 Term
mkChar(const std::string
& s
) const;
2797 * Create an empty sequence of the given element sort.
2798 * @param sort The element sort of the sequence.
2799 * @return the empty sequence with given element sort.
2801 Term
mkEmptySequence(const Sort
& sort
) const;
2804 * Create a universe set of the given sort.
2805 * @param sort the sort of the set elements
2806 * @return the universe set constant
2808 Term
mkUniverseSet(const Sort
& sort
) const;
2811 * Create a bit-vector constant of given size and value.
2812 * @param size the bit-width of the bit-vector sort
2813 * @param val the value of the constant
2814 * @return the bit-vector constant
2816 Term
mkBitVector(uint32_t size
, uint64_t val
= 0) const;
2819 * Create a bit-vector constant from a given string of base 2, 10 or 16.
2821 * The size of resulting bit-vector is
2822 * - base 2: the size of the binary string
2823 * - base 10: the min. size required to represent the decimal as a bit-vector
2824 * - base 16: the max. size required to represent the hexadecimal as a
2825 * bit-vector (4 * size of the given value string)
2827 * @param s the string representation of the constant
2828 * @param base the base of the string representation (2, 10, or 16)
2829 * @return the bit-vector constant
2831 Term
mkBitVector(const std::string
& s
, uint32_t base
= 2) const;
2834 * Create a bit-vector constant of a given bit-width from a given string of
2836 * @param size the bit-width of the constant
2837 * @param s the string representation of the constant
2838 * @param base the base of the string representation (2, 10, or 16)
2839 * @return the bit-vector constant
2841 Term
mkBitVector(uint32_t size
, const std::string
& s
, uint32_t base
) const;
2844 * Create a constant array with the provided constant value stored at every
2846 * @param sort the sort of the constant array (must be an array sort)
2847 * @param val the constant value to store (must match the sort's element sort)
2848 * @return the constant array term
2850 Term
mkConstArray(const Sort
& sort
, const Term
& val
) const;
2853 * Create a positive infinity floating-point constant. Requires CVC4 to be
2854 * compiled with SymFPU support.
2855 * @param exp Number of bits in the exponent
2856 * @param sig Number of bits in the significand
2857 * @return the floating-point constant
2859 Term
mkPosInf(uint32_t exp
, uint32_t sig
) const;
2862 * Create a negative infinity floating-point constant. Requires CVC4 to be
2863 * compiled with SymFPU support.
2864 * @param exp Number of bits in the exponent
2865 * @param sig Number of bits in the significand
2866 * @return the floating-point constant
2868 Term
mkNegInf(uint32_t exp
, uint32_t sig
) const;
2871 * Create a not-a-number (NaN) floating-point constant. Requires CVC4 to be
2872 * compiled with SymFPU support.
2873 * @param exp Number of bits in the exponent
2874 * @param sig Number of bits in the significand
2875 * @return the floating-point constant
2877 Term
mkNaN(uint32_t exp
, uint32_t sig
) const;
2880 * Create a positive zero (+0.0) floating-point constant. Requires CVC4 to be
2881 * compiled with SymFPU support.
2882 * @param exp Number of bits in the exponent
2883 * @param sig Number of bits in the significand
2884 * @return the floating-point constant
2886 Term
mkPosZero(uint32_t exp
, uint32_t sig
) const;
2889 * Create a negative zero (-0.0) floating-point constant. Requires CVC4 to be
2890 * compiled with SymFPU support.
2891 * @param exp Number of bits in the exponent
2892 * @param sig Number of bits in the significand
2893 * @return the floating-point constant
2895 Term
mkNegZero(uint32_t exp
, uint32_t sig
) const;
2898 * Create a roundingmode constant.
2899 * @param rm the floating point rounding mode this constant represents
2901 Term
mkRoundingMode(RoundingMode rm
) const;
2904 * Create uninterpreted constant.
2905 * @param arg1 Sort of the constant
2906 * @param arg2 Index of the constant
2908 Term
mkUninterpretedConst(const Sort
& sort
, int32_t index
) const;
2911 * Create an abstract value constant.
2912 * @param index Index of the abstract value
2914 Term
mkAbstractValue(const std::string
& index
) const;
2917 * Create an abstract value constant.
2918 * @param index Index of the abstract value
2920 Term
mkAbstractValue(uint64_t index
) const;
2923 * Create a floating-point constant (requires CVC4 to be compiled with symFPU
2925 * @param exp Size of the exponent
2926 * @param sig Size of the significand
2927 * @param val Value of the floating-point constant as a bit-vector term
2929 Term
mkFloatingPoint(uint32_t exp
, uint32_t sig
, Term val
) const;
2931 /* .................................................................... */
2932 /* Create Variables */
2933 /* .................................................................... */
2936 * Create (first-order) constant (0-arity function symbol).
2937 * SMT-LIB: ( declare-const <symbol> <sort> )
2938 * SMT-LIB: ( declare-fun <symbol> ( ) <sort> )
2940 * @param sort the sort of the constant
2941 * @param symbol the name of the constant
2942 * @return the first-order constant
2944 Term
mkConst(const Sort
& sort
, const std::string
& symbol
) const;
2946 * Create (first-order) constant (0-arity function symbol), with a default
2949 * @param sort the sort of the constant
2950 * @return the first-order constant
2952 Term
mkConst(const Sort
& sort
) const;
2955 * Create a bound variable to be used in a binder (i.e. a quantifier, a
2956 * lambda, or a witness binder).
2957 * @param sort the sort of the variable
2958 * @param symbol the name of the variable
2959 * @return the variable
2961 Term
mkVar(const Sort
& sort
, const std::string
& symbol
= std::string()) const;
2963 /* .................................................................... */
2964 /* Create datatype constructor declarations */
2965 /* .................................................................... */
2967 DatatypeConstructorDecl
mkDatatypeConstructorDecl(const std::string
& name
);
2969 /* .................................................................... */
2970 /* Create datatype declarations */
2971 /* .................................................................... */
2974 * Create a datatype declaration.
2975 * @param name the name of the datatype
2976 * @param isCoDatatype true if a codatatype is to be constructed
2977 * @return the DatatypeDecl
2979 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
2980 bool isCoDatatype
= false);
2983 * Create a datatype declaration.
2984 * Create sorts parameter with Solver::mkParamSort().
2985 * @param name the name of the datatype
2986 * @param param the sort parameter
2987 * @param isCoDatatype true if a codatatype is to be constructed
2988 * @return the DatatypeDecl
2990 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
2992 bool isCoDatatype
= false);
2995 * Create a datatype declaration.
2996 * Create sorts parameter with Solver::mkParamSort().
2997 * @param name the name of the datatype
2998 * @param params a list of sort parameters
2999 * @param isCoDatatype true if a codatatype is to be constructed
3000 * @return the DatatypeDecl
3002 DatatypeDecl
mkDatatypeDecl(const std::string
& name
,
3003 const std::vector
<Sort
>& params
,
3004 bool isCoDatatype
= false);
3006 /* .................................................................... */
3007 /* Formula Handling */
3008 /* .................................................................... */
3011 * Simplify a formula without doing "much" work. Does not involve
3012 * the SAT Engine in the simplification, but uses the current
3013 * definitions, assertions, and the current partial model, if one
3014 * has been constructed. It also involves theory normalization.
3015 * @param t the formula to simplify
3016 * @return the simplified formula
3018 Term
simplify(const Term
& t
);
3022 * SMT-LIB: ( assert <term> )
3023 * @param term the formula to assert
3025 void assertFormula(const Term
& term
) const;
3028 * Check satisfiability.
3029 * SMT-LIB: ( check-sat )
3030 * @return the result of the satisfiability check.
3032 Result
checkSat() const;
3035 * Check satisfiability assuming the given formula.
3036 * SMT-LIB: ( check-sat-assuming ( <prop_literal> ) )
3037 * @param assumption the formula to assume
3038 * @return the result of the satisfiability check.
3040 Result
checkSatAssuming(const Term
& assumption
) const;
3043 * Check satisfiability assuming the given formulas.
3044 * SMT-LIB: ( check-sat-assuming ( <prop_literal>+ ) )
3045 * @param assumptions the formulas to assume
3046 * @return the result of the satisfiability check.
3048 Result
checkSatAssuming(const std::vector
<Term
>& assumptions
) const;
3051 * Check entailment of the given formula w.r.t. the current set of assertions.
3052 * @param term the formula to check entailment for
3053 * @return the result of the entailment check.
3055 Result
checkEntailed(const Term
& term
) const;
3058 * Check entailment of the given set of given formulas w.r.t. the current
3059 * set of assertions.
3060 * @param terms the terms to check entailment for
3061 * @return the result of the entailmentcheck.
3063 Result
checkEntailed(const std::vector
<Term
>& terms
) const;
3066 * Create datatype sort.
3067 * SMT-LIB: ( declare-datatype <symbol> <datatype_decl> )
3068 * @param symbol the name of the datatype sort
3069 * @param ctors the constructor declarations of the datatype sort
3070 * @return the datatype sort
3072 Sort
declareDatatype(const std::string
& symbol
,
3073 const std::vector
<DatatypeConstructorDecl
>& ctors
) const;
3076 * Declare n-ary function symbol.
3077 * SMT-LIB: ( declare-fun <symbol> ( <sort>* ) <sort> )
3078 * @param symbol the name of the function
3079 * @param sorts the sorts of the parameters to this function
3080 * @param sort the sort of the return value of this function
3081 * @return the function
3083 Term
declareFun(const std::string
& symbol
,
3084 const std::vector
<Sort
>& sorts
,
3085 const Sort
& sort
) const;
3088 * Declare uninterpreted sort.
3089 * SMT-LIB: ( declare-sort <symbol> <numeral> )
3090 * @param symbol the name of the sort
3091 * @param arity the arity of the sort
3094 Sort
declareSort(const std::string
& symbol
, uint32_t arity
) const;
3097 * Define n-ary function.
3098 * SMT-LIB: ( define-fun <function_def> )
3099 * @param symbol the name of the function
3100 * @param bound_vars the parameters to this function
3101 * @param sort the sort of the return value of this function
3102 * @param term the function body
3103 * @param global determines whether this definition is global (i.e. persists
3104 * when popping the context)
3105 * @return the function
3107 Term
defineFun(const std::string
& symbol
,
3108 const std::vector
<Term
>& bound_vars
,
3111 bool global
= false) const;
3113 * Define n-ary function.
3114 * SMT-LIB: ( define-fun <function_def> )
3115 * Create parameter 'fun' with mkConst().
3116 * @param fun the sorted function
3117 * @param bound_vars the parameters to this function
3118 * @param term the function body
3119 * @param global determines whether this definition is global (i.e. persists
3120 * when popping the context)
3121 * @return the function
3123 Term
defineFun(const Term
& fun
,
3124 const std::vector
<Term
>& bound_vars
,
3126 bool global
= false) const;
3129 * Define recursive function.
3130 * SMT-LIB: ( define-fun-rec <function_def> )
3131 * @param symbol the name of the function
3132 * @param bound_vars the parameters to this function
3133 * @param sort the sort of the return value of this function
3134 * @param term the function body
3135 * @param global determines whether this definition is global (i.e. persists
3136 * when popping the context)
3137 * @return the function
3139 Term
defineFunRec(const std::string
& symbol
,
3140 const std::vector
<Term
>& bound_vars
,
3143 bool global
= false) const;
3146 * Define recursive function.
3147 * SMT-LIB: ( define-fun-rec <function_def> )
3148 * Create parameter 'fun' with mkConst().
3149 * @param fun the sorted function
3150 * @param bound_vars the parameters to this function
3151 * @param term the function body
3152 * @param global determines whether this definition is global (i.e. persists
3153 * when popping the context)
3154 * @return the function
3156 Term
defineFunRec(const Term
& fun
,
3157 const std::vector
<Term
>& bound_vars
,
3159 bool global
= false) const;
3162 * Define recursive functions.
3163 * SMT-LIB: ( define-funs-rec ( <function_decl>^{n+1} ) ( <term>^{n+1} ) )
3164 * Create elements of parameter 'funs' with mkConst().
3165 * @param funs the sorted functions
3166 * @param bound_vars the list of parameters to the functions
3167 * @param term the list of function bodies of the functions
3168 * @param global determines whether this definition is global (i.e. persists
3169 * when popping the context)
3170 * @return the function
3172 void defineFunsRec(const std::vector
<Term
>& funs
,
3173 const std::vector
<std::vector
<Term
>>& bound_vars
,
3174 const std::vector
<Term
>& terms
,
3175 bool global
= false) const;
3178 * Echo a given string to the given output stream.
3179 * SMT-LIB: ( echo <std::string> )
3180 * @param out the output stream
3181 * @param str the string to echo
3183 void echo(std::ostream
& out
, const std::string
& str
) const;
3186 * Get the list of asserted formulas.
3187 * SMT-LIB: ( get-assertions )
3188 * @return the list of asserted formulas
3190 std::vector
<Term
> getAssertions() const;
3193 * Get info from the solver.
3194 * SMT-LIB: ( get-info <info_flag> )
3197 std::string
getInfo(const std::string
& flag
) const;
3200 * Get the value of a given option.
3201 * SMT-LIB: ( get-option <keyword> )
3202 * @param option the option for which the value is queried
3203 * @return a string representation of the option value
3205 std::string
getOption(const std::string
& option
) const;
3208 * Get the set of unsat ("failed") assumptions.
3209 * SMT-LIB: ( get-unsat-assumptions )
3210 * Requires to enable option 'produce-unsat-assumptions'.
3211 * @return the set of unsat assumptions.
3213 std::vector
<Term
> getUnsatAssumptions() const;
3216 * Get the unsatisfiable core.
3217 * SMT-LIB: ( get-unsat-core )
3218 * Requires to enable option 'produce-unsat-cores'.
3219 * @return a set of terms representing the unsatisfiable core
3221 std::vector
<Term
> getUnsatCore() const;
3224 * Get the value of the given term.
3225 * SMT-LIB: ( get-value ( <term> ) )
3226 * @param term the term for which the value is queried
3227 * @return the value of the given term
3229 Term
getValue(const Term
& term
) const;
3231 * Get the values of the given terms.
3232 * SMT-LIB: ( get-value ( <term>+ ) )
3233 * @param terms the terms for which the value is queried
3234 * @return the values of the given terms
3236 std::vector
<Term
> getValue(const std::vector
<Term
>& terms
) const;
3239 * Do quantifier elimination.
3240 * SMT-LIB: ( get-qe <q> )
3241 * Requires a logic that supports quantifier elimination. Currently, the only
3242 * logics supported by quantifier elimination is LRA and LIA.
3243 * @param q a quantified formula of the form:
3244 * Q x1...xn. P( x1...xn, y1...yn )
3245 * where P( x1...xn, y1...yn ) is a quantifier-free formula
3246 * @return a formula ret such that, given the current set of formulas A
3247 * asserted to this solver:
3248 * - ( A ^ q ) and ( A ^ ret ) are equivalent
3249 * - ret is quantifier-free formula containing only free variables in
3252 Term
getQuantifierElimination(const Term
& q
) const;
3255 * Do partial quantifier elimination, which can be used for incrementally
3256 * computing the result of a quantifier elimination.
3257 * SMT-LIB: ( get-qe-disjunct <q> )
3258 * Requires a logic that supports quantifier elimination. Currently, the only
3259 * logics supported by quantifier elimination is LRA and LIA.
3260 * @param q a quantified formula of the form:
3261 * Q x1...xn. P( x1...xn, y1...yn )
3262 * where P( x1...xn, y1...yn ) is a quantifier-free formula
3263 * @return a formula ret such that, given the current set of formulas A
3264 * asserted to this solver:
3265 * - (A ^ q) => (A ^ ret) if Q is forall or (A ^ ret) => (A ^ q) if Q is
3267 * - ret is quantifier-free formula containing only free variables in
3269 * - If Q is exists, let A^Q_n be the formula
3270 * A ^ ~ret^Q_1 ^ ... ^ ~ret^Q_n
3271 * where for each i=1,...n, formula ret^Q_i is the result of calling
3272 * getQuantifierEliminationDisjunct for q with the set of assertions
3273 * A^Q_{i-1}. Similarly, if Q is forall, then let A^Q_n be
3274 * A ^ ret^Q_1 ^ ... ^ ret^Q_n
3275 * where ret^Q_i is the same as above. In either case, we have
3276 * that ret^Q_j will eventually be true or false, for some finite j.
3278 Term
getQuantifierEliminationDisjunct(const Term
& q
) const;
3281 * When using separation logic, this sets the location sort and the
3282 * datatype sort to the given ones. This method should be invoked exactly
3283 * once, before any separation logic constraints are provided.
3284 * @param locSort The location sort of the heap
3285 * @param dataSort The data sort of the heap
3287 void declareSeparationHeap(const Sort
& locSort
, const Sort
& dataSort
) const;
3290 * When using separation logic, obtain the term for the heap.
3291 * @return The term for the heap
3293 Term
getSeparationHeap() const;
3296 * When using separation logic, obtain the term for nil.
3297 * @return The term for nil
3299 Term
getSeparationNilTerm() const;
3302 * Pop (a) level(s) from the assertion stack.
3303 * SMT-LIB: ( pop <numeral> )
3304 * @param nscopes the number of levels to pop
3306 void pop(uint32_t nscopes
= 1) const;
3309 * Get an interpolant
3310 * SMT-LIB: ( get-interpol <conj> )
3311 * Requires to enable option 'produce-interpols'.
3312 * @param conj the conjecture term
3313 * @param output a Term I such that A->I and I->B are valid, where A is the
3314 * current set of assertions and B is given in the input by conj.
3315 * @return true if it gets I successfully, false otherwise.
3317 bool getInterpolant(const Term
& conj
, Term
& output
) const;
3320 * Get an interpolant
3321 * SMT-LIB: ( get-interpol <conj> <g> )
3322 * Requires to enable option 'produce-interpols'.
3323 * @param conj the conjecture term
3324 * @param g the grammar for the interpolant I
3325 * @param output a Term I such that A->I and I->B are valid, where A is the
3326 * current set of assertions and B is given in the input by conj.
3327 * @return true if it gets I successfully, false otherwise.
3329 bool getInterpolant(const Term
& conj
, Grammar
& g
, Term
& output
) const;
3333 * SMT-LIB: ( get-abduct <conj> )
3334 * Requires enabling option 'produce-abducts'
3335 * @param conj the conjecture term
3336 * @param output a term C such that A^C is satisfiable, and A^~B^C is
3337 * unsatisfiable, where A is the current set of assertions and B is
3338 * given in the input by conj
3339 * @return true if it gets C successfully, false otherwise
3341 bool getAbduct(const Term
& conj
, Term
& output
) const;
3345 * SMT-LIB: ( get-abduct <conj> <g> )
3346 * Requires enabling option 'produce-abducts'
3347 * @param conj the conjecture term
3348 * @param g the grammar for the abduct C
3349 * @param output a term C such that A^C is satisfiable, and A^~B^C is
3350 * unsatisfiable, where A is the current set of assertions and B is
3351 * given in the input by conj
3352 * @return true if it gets C successfully, false otherwise
3354 bool getAbduct(const Term
& conj
, Grammar
& g
, Term
& output
) const;
3357 * Block the current model. Can be called only if immediately preceded by a
3358 * SAT or INVALID query.
3359 * SMT-LIB: ( block-model )
3360 * Requires enabling 'produce-models' option and setting 'block-models' option
3361 * to a mode other than "none".
3363 void blockModel() const;
3366 * Block the current model values of (at least) the values in terms. Can be
3367 * called only if immediately preceded by a SAT or NOT_ENTAILED query.
3368 * SMT-LIB: ( block-model-values ( <terms>+ ) )
3369 * Requires enabling 'produce-models' option and setting 'block-models' option
3370 * to a mode other than "none".
3372 void blockModelValues(const std::vector
<Term
>& terms
) const;
3375 * Print all instantiations made by the quantifiers module.
3376 * @param out the output stream
3378 void printInstantiations(std::ostream
& out
) const;
3381 * Push (a) level(s) to the assertion stack.
3382 * SMT-LIB: ( push <numeral> )
3383 * @param nscopes the number of levels to push
3385 void push(uint32_t nscopes
= 1) const;
3388 * Remove all assertions.
3389 * SMT-LIB: ( reset-assertions )
3391 void resetAssertions() const;
3395 * SMT-LIB: ( set-info <attribute> )
3396 * @param keyword the info flag
3397 * @param value the value of the info flag
3399 void setInfo(const std::string
& keyword
, const std::string
& value
) const;
3403 * SMT-LIB: ( set-logic <symbol> )
3404 * @param logic the logic to set
3406 void setLogic(const std::string
& logic
) const;
3410 * SMT-LIB: ( set-option <option> )
3411 * @param option the option name
3412 * @param value the option value
3414 void setOption(const std::string
& option
, const std::string
& value
) const;
3417 * If needed, convert this term to a given sort. Note that the sort of the
3418 * term must be convertible into the target sort. Currently only Int to Real
3419 * conversions are supported.
3420 * @param s the target sort
3421 * @return the term wrapped into a sort conversion if needed
3423 Term
ensureTermSort(const Term
& t
, const Sort
& s
) const;
3426 * Append <symbol> to the current list of universal variables.
3427 * SyGuS v2: ( declare-var <symbol> <sort> )
3428 * @param sort the sort of the universal variable
3429 * @param symbol the name of the universal variable
3430 * @return the universal variable
3432 Term
mkSygusVar(const Sort
& sort
,
3433 const std::string
& symbol
= std::string()) const;
3436 * Create a Sygus grammar. The first non-terminal is treated as the starting
3437 * non-terminal, so the order of non-terminals matters.
3439 * @param boundVars the parameters to corresponding synth-fun/synth-inv
3440 * @param ntSymbols the pre-declaration of the non-terminal symbols
3441 * @return the grammar
3443 Grammar
mkSygusGrammar(const std::vector
<Term
>& boundVars
,
3444 const std::vector
<Term
>& ntSymbols
) const;
3447 * Synthesize n-ary function.
3448 * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> )
3449 * @param symbol the name of the function
3450 * @param boundVars the parameters to this function
3451 * @param sort the sort of the return value of this function
3452 * @return the function
3454 Term
synthFun(const std::string
& symbol
,
3455 const std::vector
<Term
>& boundVars
,
3456 const Sort
& sort
) const;
3459 * Synthesize n-ary function following specified syntactic constraints.
3460 * SyGuS v2: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g> )
3461 * @param symbol the name of the function
3462 * @param boundVars the parameters to this function
3463 * @param sort the sort of the return value of this function
3464 * @param g the syntactic constraints
3465 * @return the function
3467 Term
synthFun(const std::string
& symbol
,
3468 const std::vector
<Term
>& boundVars
,
3473 * Synthesize invariant.
3474 * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) )
3475 * @param symbol the name of the invariant
3476 * @param boundVars the parameters to this invariant
3477 * @param sort the sort of the return value of this invariant
3478 * @return the invariant
3480 Term
synthInv(const std::string
& symbol
,
3481 const std::vector
<Term
>& boundVars
) const;
3484 * Synthesize invariant following specified syntactic constraints.
3485 * SyGuS v2: ( synth-inv <symbol> ( <boundVars>* ) <g> )
3486 * @param symbol the name of the invariant
3487 * @param boundVars the parameters to this invariant
3488 * @param sort the sort of the return value of this invariant
3489 * @param g the syntactic constraints
3490 * @return the invariant
3492 Term
synthInv(const std::string
& symbol
,
3493 const std::vector
<Term
>& boundVars
,
3497 * Add a forumla to the set of Sygus constraints.
3498 * SyGuS v2: ( constraint <term> )
3499 * @param term the formula to add as a constraint
3501 void addSygusConstraint(const Term
& term
) const;
3504 * Add a set of Sygus constraints to the current state that correspond to an
3505 * invariant synthesis problem.
3506 * SyGuS v2: ( inv-constraint <inv> <pre> <trans> <post> )
3507 * @param inv the function-to-synthesize
3508 * @param pre the pre-condition
3509 * @param trans the transition relation
3510 * @param post the post-condition
3512 void addSygusInvConstraint(Term inv
, Term pre
, Term trans
, Term post
) const;
3515 * Try to find a solution for the synthesis conjecture corresponding to the
3516 * current list of functions-to-synthesize, universal variables and
3518 * SyGuS v2: ( check-synth )
3519 * @return the result of the synthesis conjecture.
3521 Result
checkSynth() const;
3524 * Get the synthesis solution of the given term. This method should be called
3525 * immediately after the solver answers unsat for sygus input.
3526 * @param term the term for which the synthesis solution is queried
3527 * @return the synthesis solution of the given term
3529 Term
getSynthSolution(Term term
) const;
3532 * Get the synthesis solutions of the given terms. This method should be
3533 * called immediately after the solver answers unsat for sygus input.
3534 * @param terms the terms for which the synthesis solutions is queried
3535 * @return the synthesis solutions of the given terms
3537 std::vector
<Term
> getSynthSolutions(const std::vector
<Term
>& terms
) const;
3540 * Print solution for synthesis conjecture to the given output stream.
3541 * @param out the output stream
3543 void printSynthSolution(std::ostream
& out
) const;
3546 // !!! This is only temporarily available until the parser is fully migrated
3547 // to the new API. !!!
3548 SmtEngine
* getSmtEngine(void) const;
3550 // !!! This is only temporarily available until options are refactored at
3551 // the driver level. !!!
3552 Options
& getOptions(void);
3555 /** @return the node manager of this solver */
3556 NodeManager
* getNodeManager(void) const;
3558 /** Helper to check for API misuse in mkOp functions. */
3559 void checkMkTerm(Kind kind
, uint32_t nchildren
) const;
3560 /** Helper for mk-functions that call d_nodeMgr->mkConst(). */
3561 template <typename T
>
3562 Term
mkValHelper(T t
) const;
3563 /** Helper for mkReal functions that take a string as argument. */
3564 Term
mkRealFromStrHelper(const std::string
& s
) const;
3565 /** Helper for mkBitVector functions that take a string as argument. */
3566 Term
mkBVFromStrHelper(const std::string
& s
, uint32_t base
) const;
3568 * Helper for mkBitVector functions that take a string and a size as
3571 Term
mkBVFromStrHelper(uint32_t size
,
3572 const std::string
& s
,
3573 uint32_t base
) const;
3574 /** Helper for mkBitVector functions that take an integer as argument. */
3575 Term
mkBVFromIntHelper(uint32_t size
, uint64_t val
) const;
3576 /** Helper for mkTerm functions that create Term from a Kind */
3577 Term
mkTermFromKind(Kind kind
) const;
3578 /** Helper for mkChar functions that take a string as argument. */
3579 Term
mkCharFromStrHelper(const std::string
& s
) const;
3580 /** Get value helper, which accounts for subtyping */
3581 Term
getValueHelper(const Term
& term
) const;
3584 * Helper function that ensures that a given term is of sort real (as opposed
3585 * to being of sort integer).
3586 * @param t a term of sort integer or real
3587 * @return a term of sort real
3589 Term
ensureRealSort(const Term
& t
) const;
3592 * Create n-ary term of given kind. This handles the cases of left/right
3593 * associative operators, chainable operators, and cases when the number of
3594 * children exceeds the maximum arity for the kind.
3595 * @param kind the kind of the term
3596 * @param children the children of the term
3599 Term
mkTermHelper(Kind kind
, const std::vector
<Term
>& children
) const;
3602 * Create n-ary term of given kind from a given operator.
3603 * @param op the operator
3604 * @param children the children of the term
3607 Term
mkTermHelper(const Op
& op
, const std::vector
<Term
>& children
) const;
3610 * Create a vector of datatype sorts, using unresolved sorts.
3611 * @param dtypedecls the datatype declarations from which the sort is created
3612 * @param unresolvedSorts the list of unresolved sorts
3613 * @return the datatype sorts
3615 std::vector
<Sort
> mkDatatypeSortsInternal(
3616 const std::vector
<DatatypeDecl
>& dtypedecls
,
3617 const std::set
<Sort
>& unresolvedSorts
) const;
3620 * Synthesize n-ary function following specified syntactic constraints.
3621 * SMT-LIB: ( synth-fun <symbol> ( <boundVars>* ) <sort> <g>? )
3622 * @param symbol the name of the function
3623 * @param boundVars the parameters to this function
3624 * @param sort the sort of the return value of this function
3625 * @param isInv determines whether this is synth-fun or synth-inv
3626 * @param g the syntactic constraints
3627 * @return the function
3629 Term
synthFunHelper(const std::string
& symbol
,
3630 const std::vector
<Term
>& boundVars
,
3633 Grammar
* g
= nullptr) const;
3635 /** Check whether string s is a valid decimal integer. */
3636 bool isValidInteger(const std::string
& s
) const;
3638 /** Increment the term stats counter. */
3639 void increment_term_stats(Kind kind
) const;
3640 /** Increment the vars stats (if 'is_var') or consts stats counter. */
3641 void increment_vars_consts_stats(const Sort
& sort
, bool is_var
) const;
3643 /** The node manager of this solver. */
3644 std::unique_ptr
<NodeManager
> d_nodeMgr
;
3645 /** The SMT engine of this solver. */
3646 std::unique_ptr
<SmtEngine
> d_smtEngine
;
3647 /** The random number generator of this solver. */
3648 std::unique_ptr
<Random
> d_rng
;
3649 /** The statistics collected on the Api level. */
3650 std::unique_ptr
<Statistics
> d_stats
;