From: Aina Niemetz Date: Mon, 4 Apr 2022 22:59:32 +0000 (-0700) Subject: api: First batch of fixes in the api docs. (#8558) X-Git-Tag: cvc5-1.0.0~18 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c3610b9b44bc2df1baf5de268ec7dd03dbd17c3b;p=cvc5.git api: First batch of fixes in the api docs. (#8558) Uses `@return .... ` and `@param ... `, plus various fixes in the docs. --- diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index d9f816a6e..7927bd0f4 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -217,33 +217,33 @@ class CVC5_EXPORT Result /** * Operator overloading for equality of two results. - * @param r the result to compare to for equality - * @return true if the results are equal + * @param r The result to compare to for equality. + * @return True if the results are equal. */ bool operator==(const Result& r) const; /** * Operator overloading for disequality of two results. - * @param r the result to compare to for disequality - * @return true if the results are disequal + * @param r The result to compare to for disequality. + * @return True if the results are disequal. */ bool operator!=(const Result& r) const; /** - * @return an explanation for an unknown query result. + * @return An explanation for an unknown query result. */ UnknownExplanation getUnknownExplanation() const; /** - * @return a string representation of this result. + * @return A string representation of this result. */ std::string toString() const; private: /** * Constructor. - * @param r the internal result that is to be wrapped by this result - * @return the Result + * @param r The internal result that is to be wrapped by this result. + * @return The Result. */ Result(const internal::Result& r); @@ -258,9 +258,9 @@ class CVC5_EXPORT Result /** * Serialize a Result to given stream. - * @param out the output stream - * @param r the result to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param r The result to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Result& r) CVC5_EXPORT; @@ -287,38 +287,38 @@ class CVC5_EXPORT SynthResult SynthResult(); /** - * @return true if SynthResult is null, i.e., not a SynthResult returned - * from a synthesis query. + * @return True if SynthResult is null, i.e., not a SynthResult returned + * from a synthesis query. */ bool isNull() const; /** - * @return true if the synthesis query has a solution. + * @return True if the synthesis query has a solution. */ bool hasSolution() const; /** - * @return true if the synthesis query has no solution. In this case, it - * was determined that there was no solution. + * @return True if the synthesis query has no solution. In this case, it + * was determined that there was no solution. */ bool hasNoSolution() const; /** - * @return true if the result of the synthesis query could not be determined. + * @return True if the result of the synthesis query could not be determined. */ bool isUnknown() const; /** - * @return a string representation of this synthesis result. + * @return A string representation of this synthesis result. */ std::string toString() const; private: /** * Constructor. - * @param r the internal synth result that is to be wrapped by this synth + * @param r The internal synth result that is to be wrapped by this synth. * result - * @return the SynthResult + * @return The SynthResult. */ SynthResult(const internal::SynthResult& r); /** @@ -332,9 +332,9 @@ class CVC5_EXPORT SynthResult /** * Serialize a SynthResult to given stream. - * @param out the output stream - * @param r the result to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param r The result to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const SynthResult& r) CVC5_EXPORT; @@ -374,51 +374,52 @@ class CVC5_EXPORT Sort /** * Comparison for structural equality. - * @param s the sort to compare to - * @return true if the sorts are equal + * @param s The sort to compare to. + * @return True if the sorts are equal. */ bool operator==(const Sort& s) const; /** * Comparison for structural disequality. - * @param s the sort to compare to - * @return true if the sorts are not equal + * @param s The sort to compare to. + * @return True if the sorts are not equal. */ bool operator!=(const Sort& s) const; /** * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is less than s + * @param s The sort to compare to. + * @return True if this sort is less than s. */ bool operator<(const Sort& s) const; /** * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is greater than s + * @param s The sort to compare to. + * @return True if this sort is greater than s. */ bool operator>(const Sort& s) const; /** * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is less than or equal to s + * @param s The sort to compare to. + * @return True if this sort is less than or equal to s. */ bool operator<=(const Sort& s) const; /** * Comparison for ordering on sorts. - * @param s the sort to compare to - * @return true if this sort is greater than or equal to s + * @param s The sort to compare to. + * @return True if this sort is greater than or equal to s. */ bool operator>=(const Sort& s) const; /** - * Does the sort have a symbol, i.e., a name? + * Does this sort have a symbol, that is, a name? * - * For example, uninterpreted sorts and uninterpreted sort constructors have symbols. - * @return true if the sort has a symbol. + * For example, uninterpreted sorts and uninterpreted sort constructors have + * symbols. + * @return True if the sort has a symbol. */ bool hasSymbol() const; @@ -430,167 +431,171 @@ class CVC5_EXPORT Sort * Solver::mkUninterpretedSort(const std::string&) const, * Solver::mkUnresolvedSort(const std::string&, size_t) const, or * Solver::mkUninterpretedSortConstructorSort(const std::string&, size_t). - * @return the raw symbol of the sort. + * @return The raw symbol of the sort. */ std::string getSymbol() const; /** - * @return true if this Sort is a null sort. + * Determine if this is the null sort (Sort::Sort()). + * @return True if this Sort is the null sort. */ bool isNull() const; /** - * Is this a Boolean sort? - * @return true if the sort is the Boolean sort + * Determine if this is the Boolean sort (SMT-LIB: `Bool`). + * @return True if this sort is the Boolean sort. */ bool isBoolean() const; /** - * Is this a integer sort? - * @return true if the sort is the integer sort + * Determine if this is the integer sort (SMT-LIB: `Int`). + * @return True if this sort is the integer sort. */ bool isInteger() const; /** - * Is this a real sort? - * @return true if the sort is the real sort + * Determine if this is the real sort (SMT-LIB: `Real`). + * @return True if this sort is the real sort. */ bool isReal() const; /** - * Is this a string sort? - * @return true if the sort is the string sort + * Determine if this is the string sort (SMT-LIB: `String`). + * @return True if this sort is the string sort. */ bool isString() const; /** - * Is this a regexp sort? - * @return true if the sort is the regexp sort + * Determine if this is the regular expression sort (SMT-LIB: `RegLan`). + * @return True if this sort is the regular expression sort. */ bool isRegExp() const; /** - * Is this a rounding mode sort? - * @return true if the sort is the rounding mode sort + * Determine if this is the rounding mode sort (SMT-LIB: `RoundingMode`). + * @return True if this sort is the rounding mode sort. */ bool isRoundingMode() const; /** - * Is this a bit-vector sort? - * @return true if the sort is a bit-vector sort + * Determine if this is a bit-vector sort (SMT-LIB: `(_ BitVec i)`). + * @return True if this sort is a bit-vector sort. */ bool isBitVector() const; /** - * Is this a floating-point sort? - * @return true if the sort is a floating-point sort + * Determine if this is a floatingpoint sort + * (SMT-LIB: `(_ FloatingPoint eb sb)`). + * @return True if this sort is a floating-point sort. */ bool isFloatingPoint() const; /** - * Is this a datatype sort? - * @return true if the sort is a datatype sort + * Determine if this is a datatype sort. + * @return True if this sort is a datatype sort. */ bool isDatatype() const; /** - * Is this a datatype constructor sort? - * @return true if the sort is a datatype constructor sort + * Determine if this is a datatype constructor sort. + * @return True if this sort is a datatype constructor sort. */ bool isDatatypeConstructor() const; /** - * Is this a datatype selector sort? - * @return true if the sort is a datatype selector sort + * Determine if this is a datatype selector sort. + * @return True if this sort is a datatype selector sort. */ bool isDatatypeSelector() const; /** - * Is this a datatype tester sort? - * @return true if the sort is a datatype tester sort + * Determine if this is a datatype tester sort. + * @return True if this sort is a datatype tester sort. */ bool isDatatypeTester() const; /** - * Is this a datatype updater sort? - * @return true if the sort is a datatype updater sort + * Determine if this is a datatype updater sort. + * @return True if this sort is a datatype updater sort. */ bool isDatatypeUpdater() const; /** - * Is this a function sort? - * @return true if the sort is a function sort + * Determine if this is a function sort. + * @return True if this sort is a function sort. */ bool isFunction() const; /** - * Is this a predicate sort? - * That is, is this a function sort mapping to Boolean? All predicate - * sorts are also function sorts. - * @return true if the sort is a predicate sort + * Determine if this is a predicate sort. + * + * A predicate sort is a function sort that maps to the Boolean sort. All + * predicate sorts are also function sorts. + * + * @return True if this sort is a predicate sort. */ bool isPredicate() const; /** - * Is this a tuple sort? - * @return true if the sort is a tuple sort + * Determine if this a tuple sort. + * @return True if this sort is a tuple sort. */ bool isTuple() const; /** - * Is this a record sort? + * Determine if this is a record sort. * @warning This method is experimental and may change in future versions. - * @return true if the sort is a record sort + * @return True if the sort is a record sort. */ bool isRecord() const; /** - * Is this an array sort? - * @return true if the sort is an array sort + * Determine if this is an array sort. + * @return True if the sort is an array sort. */ bool isArray() const; /** - * Is this a Set sort? - * @return true if the sort is a Set sort + * Determine if this is a Set sort. + * @return True if the sort is a Set sort. */ bool isSet() const; /** - * Is this a Bag sort? - * @return true if the sort is a Bag sort + * Determine if this is a Bag sort. + * @return True if the sort is a Bag sort. */ bool isBag() const; /** - * Is this a Sequence sort? - * @return true if the sort is a Sequence sort + * Determine if this is a Sequence sort. + * @return True if the sort is a Sequence sort. */ bool isSequence() const; /** - * Is this an uninterpreted sort? - * @return true if this is an uninterpreted sort + * Determine if this is an uninterpreted sort. + * @return True if this is an uninterpreted sort. */ bool isUninterpretedSort() const; /** - * Is this an uninterpreted sort constructor kind? + * Determine if this is an uninterpreted sort constructor. * * An uninterpreted sort constructor has arity > 0 and can be instantiated to * construct uninterpreted sorts with given sort parameters. * - * @return true if this is a sort constructor kind + * @return True if this is a sort constructor kind. */ bool isUninterpretedSortConstructor() const; /** - * Is this an instantiated (parametric datatype or uninterpreted sort - * constructor) sort? + * Determine if this is an instantiated (parametric datatype or uninterpreted + * sort constructor) sort. * * An instantiated sort is a sort that has been constructed from * instantiating a sort with sort arguments * (see Sort::instantiate(const std::vector&) const)). * - * @return true if this is an instantiated sort + * @return True if this is an instantiated sort. */ bool isInstantiated() const; @@ -598,12 +603,12 @@ class CVC5_EXPORT Sort * Get the associated uninterpreted sort constructor of an instantiated * uninterpreted sort. * - * @return the uninterpreted sort constructor sort + * @return The uninterpreted sort constructor sort. */ Sort getUninterpretedSortConstructor() const; /** - * @return the underlying datatype of a datatype sort + * @return The underlying datatype of a datatype sort. */ Datatype getDatatype() const; @@ -613,8 +618,8 @@ class CVC5_EXPORT Sort * * Create sort parameters with Solver::mkParamSort(). * - * @param params the list of sort parameters to instantiate with - * @return the instantiated sort + * @param params The list of sort parameters to instantiate with. + * @return The instantiated sort. */ Sort instantiate(const std::vector& params) const; @@ -623,7 +628,7 @@ class CVC5_EXPORT Sort * sort (parametric datatype or uninterpreted sort constructor sort, * see Sort::instantiate(const std::vector& const)). * - * @return the sorts used to instantiate the sort parameters of a + * @return The sorts used to instantiate the sort parameters of a * parametric sort */ std::vector getInstantiatedParameters() const; @@ -635,13 +640,13 @@ class CVC5_EXPORT Sort * only once to the sort. It is not run until fix point. * * For example, - * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will - * return (Array (Array C D) B). + * `(Array A B).substitute({A, C}, {(Array C D), (Array A B)})` will + * return `(Array (Array C D) B)`. * * @warning This method is experimental and may change in future versions. * - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. + * @param sort The subsort to be substituted within this sort. + * @param replacement The sort replacing the substituted subsort. */ Sort substitute(const Sort& sort, const Sort& replacement) const; @@ -655,62 +660,62 @@ class CVC5_EXPORT Sort * * @warning This method is experimental and may change in future versions. * - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. + * @param sorts The subsorts to be substituted within this sort. + * @param replacements The sort replacing the substituted subsorts. */ Sort substitute(const std::vector& sorts, const std::vector& replacements) const; /** * Output a string representation of this sort to a given stream. - * @param out the output stream + * @param out The output stream. */ void toStream(std::ostream& out) const; /** - * @return a string representation of this sort + * @return A string representation of this sort. */ std::string toString() const; /* Datatype constructor sort ------------------------------------------- */ /** - * @return the arity of a datatype constructor sort + * @return The arity of a datatype constructor sort. */ size_t getDatatypeConstructorArity() const; /** - * @return the domain sorts of a datatype constructor sort + * @return The domain sorts of a datatype constructor sort. */ std::vector getDatatypeConstructorDomainSorts() const; /** - * @return the codomain sort of a constructor sort + * @return The codomain sort of a constructor sort. */ Sort getDatatypeConstructorCodomainSort() const; /* Selector sort ------------------------------------------------------- */ /** - * @return the domain sort of a datatype selector sort + * @return The domain sort of a datatype selector sort. */ Sort getDatatypeSelectorDomainSort() const; /** - * @return the codomain sort of a datatype selector sort + * @return The codomain sort of a datatype selector sort. */ Sort getDatatypeSelectorCodomainSort() const; /* Tester sort ------------------------------------------------------- */ /** - * @return the domain sort of a datatype tester sort + * @return The domain sort of a datatype tester sort. */ Sort getDatatypeTesterDomainSort() const; /** - * @return the codomain sort of a datatype tester sort, which is the Boolean - * sort + * @return The codomain sort of a datatype tester sort, which is the Boolean + * sort. * * @note We mainly need this for the symbol table, which doesn't have * access to the solver object. @@ -720,76 +725,76 @@ class CVC5_EXPORT Sort /* Function sort ------------------------------------------------------- */ /** - * @return the arity of a function sort + * @return The arity of a function sort. */ size_t getFunctionArity() const; /** - * @return the domain sorts of a function sort + * @return The domain sorts of a function sort. */ std::vector getFunctionDomainSorts() const; /** - * @return the codomain sort of a function sort + * @return The codomain sort of a function sort. */ Sort getFunctionCodomainSort() const; /* Array sort ---------------------------------------------------------- */ /** - * @return the array index sort of an array sort + * @return The array index sort of an array sort. */ Sort getArrayIndexSort() const; /** - * @return the array element sort of an array sort + * @return The array element sort of an array sort. */ Sort getArrayElementSort() const; /* Set sort ------------------------------------------------------------ */ /** - * @return the element sort of a set sort + * @return The element sort of a set sort. */ Sort getSetElementSort() const; /* Bag sort ------------------------------------------------------------ */ /** - * @return the element sort of a bag sort + * @return The element sort of a bag sort. */ Sort getBagElementSort() const; /* Sequence sort ------------------------------------------------------- */ /** - * @return the element sort of a sequence sort + * @return The element sort of a sequence sort. */ Sort getSequenceElementSort() const; /* Uninterpreted sort constructor sort --------------------------------- */ /** - * @return the arity of an uninterpreted sort constructor sort + * @return The arity of an uninterpreted sort constructor sort. */ size_t getUninterpretedSortConstructorArity() const; /* Bit-vector sort ----------------------------------------------------- */ /** - * @return the bit-width of the bit-vector sort + * @return The bit-width of the bit-vector sort. */ uint32_t getBitVectorSize() const; /* Floating-point sort ------------------------------------------------- */ /** - * @return the bit-width of the exponent of the floating-point sort + * @return The bit-width of the exponent of the floating-point sort. */ uint32_t getFloatingPointExponentSize() const; /** - * @return the width of the significand of the floating-point sort + * @return The width of the significand of the floating-point sort. */ uint32_t getFloatingPointSignificandSize() const; @@ -798,24 +803,24 @@ class CVC5_EXPORT Sort /** * Get the arity of a datatype sort, which is the number of type parameters * if the datatype is parametric, or 0 otherwise. - * @return the arity of a datatype sort + * @return The arity of a datatype sort. */ size_t getDatatypeArity() const; /* Tuple sort ---------------------------------------------------------- */ /** - * @return the length of a tuple sort + * @return The length of a tuple sort. */ size_t getTupleLength() const; /** - * @return the element sorts of a tuple sort + * @return The element sorts of a tuple sort. */ std::vector getTupleSorts() const; private: - /** @return the internal wrapped TypeNode of this sort. */ + /** @return The internal wrapped TypeNode of this sort. */ const internal::TypeNode& getTypeNode(void) const; /** Helper to convert a set of Sorts to internal TypeNodes. */ @@ -830,9 +835,9 @@ class CVC5_EXPORT Sort /** * Constructor. - * @param slv the associated solver object - * @param t the internal type that is to be wrapped by this sort - * @return the Sort + * @param slv The associated solver object. + * @param t The internal type that is to be wrapped by this sort. + * @return The Sort. */ Sort(const Solver* slv, const internal::TypeNode& t); @@ -859,9 +864,9 @@ class CVC5_EXPORT Sort /** * Serialize a sort to given stream. - * @param out the output stream - * @param s the sort to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param s The sort to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Sort& s) CVC5_EXPORT; @@ -912,8 +917,8 @@ class CVC5_EXPORT Op * Syntactic equality operator. * Return true if both operators are syntactically identical. * Both operators must belong to the same solver object. - * @param t the operator to compare to for equality - * @return true if the operators are equal + * @param t The operator to compare to for equality. + * @return True if the operators are equal. */ bool operator==(const Op& t) const; @@ -921,57 +926,57 @@ class CVC5_EXPORT Op * Syntactic disequality operator. * Return true if both operators differ syntactically. * Both terms must belong to the same solver object. - * @param t the operator to compare to for disequality - * @return true if operators are disequal + * @param t The operator to compare to for disequality. + * @return True if operators are disequal. */ bool operator!=(const Op& t) const; /** - * @return the kind of this operator + * @return The kind of this operator. */ Kind getKind() const; /** - * @return true if this operator is a null term + * @return True if this operator is a null term. */ bool isNull() const; /** - * @return true iff this operator is indexed + * @return True iff this operator is indexed. */ bool isIndexed() const; /** - * @return the number of indices of this op + * @return The number of indices of this op. */ size_t getNumIndices() const; /** * Get the index at position i. - * @param i the position of the index to return - * @return the index at position i + * @param i The position of the index to return. + * @return The index at position i. */ Term operator[](size_t i) const; /** - * @return a string representation of this operator + * @return A string representation of this operator. */ std::string toString() const; private: /** * Constructor for a single kind (non-indexed operator). - * @param slv the associated solver object - * @param k the kind of this Op + * @param slv The associated solver object. + * @param k The kind of this Op. */ Op(const Solver* slv, const Kind k); /** * Constructor. - * @param slv the associated solver object - * @param k the kind of this Op - * @param n the internal node that is to be wrapped by this term - * @return the Term + * @param slv The associated solver object. + * @param k The kind of this Op. + * @param n The internal node that is to be wrapped by this term. + * @return The Term. */ Op(const Solver* slv, const Kind k, const internal::Node& n); @@ -987,20 +992,21 @@ class CVC5_EXPORT Op * @note We use a helper method to avoid having API functions call other API * functions (we need to call this internally). * - * @return true iff this Op is indexed + * @return True iff this Op is indexed. */ bool isIndexedHelper() const; /** * Helper for getNumIndices - * @return the number of indices of this op + * @return The number of indices of this op. */ size_t getNumIndicesHelper() const; /** * Helper for operator[](size_t index). - * @param index position of the index. Should be less than getNumIndicesHelper(). - * @return the index at position index + * @param index Position of the index. Should be less than + * getNumIndicesHelper(). + * @return The index at position index. */ Term getIndexHelper(size_t index) const; @@ -1024,9 +1030,9 @@ class CVC5_EXPORT Op /** * Serialize an operator to given stream. - * @param out the output stream - * @param t the operator to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param t The operator to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Op& t) CVC5_EXPORT; @@ -1077,8 +1083,8 @@ class CVC5_EXPORT Term * Syntactic equality operator. * Return true if both terms are syntactically identical. * Both terms must belong to the same solver object. - * @param t the term to compare to for equality - * @return true if the terms are equal + * @param t The term to compare to for equality. + * @return True if the terms are equal. */ bool operator==(const Term& t) const; @@ -1086,66 +1092,66 @@ class CVC5_EXPORT Term * Syntactic disequality operator. * Return true if both terms differ syntactically. * Both terms must belong to the same solver object. - * @param t the term to compare to for disequality - * @return true if terms are disequal + * @param t The term to compare to for disequality. + * @return True if terms are disequal. */ bool operator!=(const Term& t) const; /** * Comparison for ordering on terms by their id. - * @param t the term to compare to - * @return true if this term is less than t + * @param t The term to compare to. + * @return True if this term is less than t. */ bool operator<(const Term& t) const; /** * Comparison for ordering on terms by their id. - * @param t the term to compare to - * @return true if this term is greater than t + * @param t The term to compare to. + * @return True if this term is greater than t. */ bool operator>(const Term& t) const; /** * Comparison for ordering on terms by their id. - * @param t the term to compare to - * @return true if this term is less than or equal to t + * @param t The term to compare to. + * @return True if this term is less than or equal to t. */ bool operator<=(const Term& t) const; /** * Comparison for ordering on terms by their id. - * @param t the term to compare to - * @return true if this term is greater than or equal to t + * @param t The term to compare to. + * @return True if this term is greater than or equal to t. */ bool operator>=(const Term& t) const; - /** @return the number of children of this term */ + /** @return The number of children of this term */ size_t getNumChildren() const; /** * Get the child term at a given index. - * @param index the index of the child term to return - * @return the child term with the given index + * @param index The index of the child term to return. + * @return The child term with the given index. */ Term operator[](size_t index) const; /** - * @return the id of this term + * @return The id of this term. */ uint64_t getId() const; /** - * @return the kind of this term + * @return The kind of this term. */ Kind getKind() const; /** - * @return the sort of this term + * @return The sort of this term. */ Sort getSort() const; /** - * @return the result of replacing 'term' by 'replacement' in this term. + * @return The result of replacing 'term' by 'replacement' in this term. * * Note that this replacement is applied during a pre-order traversal and * only once to the term. It is not run until fix point. @@ -1153,8 +1159,8 @@ class CVC5_EXPORT Term Term substitute(const Term& term, const Term& replacement) const; /** - * @return the result of simultaneously replacing 'terms' by 'replacements' - * in this term + * @return The result of simultaneously replacing 'terms' by 'replacements' + * in this term. * * Note that this replacement is applied during a pre-order traversal and * only once to the term. It is not run until fix point. In the case that @@ -1167,14 +1173,14 @@ class CVC5_EXPORT Term const std::vector& replacements) const; /** - * @return true iff this term has an operator + * @return True iff this term has an operator. */ bool hasOp() const; /** * @note This is safe to call when hasOp() returns true. * - * @return the Op used to create this term + * @return The Op used to create this term. */ Op getOp() const; @@ -1182,7 +1188,7 @@ class CVC5_EXPORT Term * Does the term have a symbol, i.e., a name? * * For example, free constants and variables have symbols. - * @return true if the term has a symbol. + * @return True if the term has a symbol. */ bool hasSymbol() const; @@ -1191,66 +1197,66 @@ class CVC5_EXPORT Term * * Asserts hasSymbol(). The symbol of the term is the string that was * provided when constructing it via Solver::mkConst() or Solver::mkVar(). - * @return the raw symbol of the term. + * @return The raw symbol of the term. */ std::string getSymbol() const; /** - * @return true if this Term is a null term + * @return True if this Term is a null term. */ bool isNull() const; /** * Boolean negation. - * @return the Boolean negation of this term + * @return The Boolean negation of this term. */ Term notTerm() const; /** * Boolean and. - * @param t a Boolean term - * @return the conjunction of this term and the given term + * @param t A Boolean term. + * @return The conjunction of this term and the given term. */ Term andTerm(const Term& t) const; /** * Boolean or. - * @param t a Boolean term - * @return the disjunction of this term and the given term + * @param t A Boolean term. + * @return The disjunction of this term and the given term. */ Term orTerm(const Term& t) const; /** * Boolean exclusive or. - * @param t a Boolean term - * @return the exclusive disjunction of this term and the given term + * @param t A Boolean term. + * @return The exclusive disjunction of this term and the given term. */ Term xorTerm(const Term& t) const; /** * Equality. - * @param t a Boolean term - * @return the Boolean equivalence of this term and the given term + * @param t A Boolean term. + * @return The Boolean equivalence of this term and the given term. */ Term eqTerm(const Term& t) const; /** * Boolean implication. - * @param t a Boolean term - * @return the implication of this term and the given term + * @param t A Boolean term. + * @return The implication of this term and the given term. */ Term impTerm(const Term& t) const; /** * If-then-else with this term as the Boolean condition. - * @param then_t the 'then' term - * @param else_t the 'else' term - * @return the if-then-else term with this term as the Boolean condition + * @param then_t The 'then' term. + * @param else_t The 'else' term. + * @return The if-then-else term with this term as the Boolean condition. */ Term iteTerm(const Term& then_t, const Term& else_t) const; /** - * @return a string representation of this term + * @return A string representation of this term. */ std::string toString() const; @@ -1291,9 +1297,9 @@ class CVC5_EXPORT Term /** * Constructor - * @param slv the associated solver object - * @param e a ``std::shared pointer`` to the node that we're iterating over - * @param p the position of the iterator (e.g. which child it's on) + * @param slv The associated solver object. + * @param e A ``std::shared pointer`` to the node that we're iterating over. + * @param p The position of the iterator (e.g. which child it's on). */ const_iterator(const Solver* slv, const std::shared_ptr& e, @@ -1306,40 +1312,40 @@ class CVC5_EXPORT Term /** * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment + * @param it The iterator to assign to. + * @return The reference to the iterator after assignment. */ const_iterator& operator=(const const_iterator& it); /** * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal + * @param it The iterator to compare to for equality. + * @return True if the iterators are equal. */ bool operator==(const const_iterator& it) const; /** * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal + * @param it The iterator to compare to for disequality. + * @return True if the iterators are disequal. */ bool operator!=(const const_iterator& it) const; /** * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator& operator++(); /** * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator operator++(int); /** * Dereference operator. - * @return the term this iterator points to + * @return The term this iterator points to. */ Term operator*() const; @@ -1355,12 +1361,12 @@ class CVC5_EXPORT Term }; /** - * @return an iterator to the first child of this Term + * @return An iterator to the first child of this Term. */ const_iterator begin() const; /** - * @return an iterator to one-off-the-last child of this Term + * @return An iterator to one-off-the-last child of this Term. */ const_iterator end() const; @@ -1368,197 +1374,201 @@ class CVC5_EXPORT Term * Get integer or real value sign. Must be called on integer or real values, * or otherwise an exception is thrown. * @return 0 if this term is zero, -1 if this term is a negative real or - * integer value, 1 if this term is a positive real or integer value. + * integer value, 1 if this term is a positive real or integer value. */ int32_t getRealOrIntegerValueSign() const; /** - * @return true if the term is an integer value that fits within int32_t. + * @return True if the term is an integer value that fits within int32_t. */ bool isInt32Value() const; /** * Asserts isInt32Value(). - * @return the integer term as a int32_t. + * @return The integer term as a int32_t. */ int32_t getInt32Value() const; /** - * @return true if the term is an integer value that fits within uint32_t. + * @return True if the term is an integer value that fits within uint32_t. */ bool isUInt32Value() const; /** * Asserts isUInt32Value(). - * @return the integer term as a uint32_t. + * @return The integer term as a uint32_t. */ uint32_t getUInt32Value() const; /** - * @return true if the term is an integer value that fits within int64_t. + * @return True if the term is an integer value that fits within int64_t. */ bool isInt64Value() const; /** * Asserts isInt64Value(). - * @return the integer term as a int64_t. + * @return The integer term as a int64_t. */ int64_t getInt64Value() const; /** - * @return true if the term is an integer value that fits within uint64_t. + * @return True if the term is an integer value that fits within uint64_t. */ bool isUInt64Value() const; /** * Asserts isUInt64Value(). - * @return the integer term as a uint64_t. + * @return The integer term as a uint64_t. */ uint64_t getUInt64Value() const; /** - * @return true if the term is an integer value. + * @return True if the term is an integer value. */ bool isIntegerValue() const; /** * Asserts isIntegerValue(). - * @return the integer term in (decimal) string representation. + * @return The integer term in (decimal) string representation. */ std::string getIntegerValue() const; /** - * @return true if the term is a string value. + * @return True if the term is a string value. */ bool isStringValue() const; /** * Asserts isStringValue(). * @note This method is not to be confused with toString(), which returns * some string representation of the term, whatever data it may hold. - * @return the string term as a native string value. + * @return The string term as a native string value. */ std::wstring getStringValue() const; /** - * @return true if the term is a rational value whose numerator and - * denominator fit within int32_t and uint32_t, respectively. + * @return True if the term is a rational value whose numerator and + * denominator fit within int32_t and uint32_t, respectively. */ bool isReal32Value() const; /** * Asserts isReal32Value(). - * @return the representation of a rational value as a pair of its numerator - * and denominator. + * @return The representation of a rational value as a pair of its numerator + * and denominator. */ std::pair getReal32Value() const; /** - * @return true if the term is a rational value whose numerator and - * denominator fit within int64_t and uint64_t, respectively. + * @return True if the term is a rational value whose numerator and + * denominator fit within int64_t and uint64_t, respectively. */ bool isReal64Value() const; /** * Asserts isReal64Value(). - * @return the representation of a rational value as a pair of its numerator - * and denominator. + * @return The representation of a rational value as a pair of its numerator + * and denominator. */ std::pair getReal64Value() const; /** * @note A term of kind PI is not considered to be a real value. - * @return true if the term is a rational value. + * @return True if the term is a rational value. */ bool isRealValue() const; /** * Asserts isRealValue(). - * @return the representation of a rational value as a (rational) string. + * @return The representation of a rational value as a (rational) string. */ std::string getRealValue() const; /** - * @return true if the term is a constant array. + * @return True if the term is a constant array. */ bool isConstArray() const; /** * Asserts isConstArray(). - * @return the base (element stored at all indices) of a constant array + * @return The base (element stored at all indices) of a constant array. */ Term getConstArrayBase() const; /** - * @return true if the term is a Boolean value. + * @return True if the term is a Boolean value. */ bool isBooleanValue() const; /** * Asserts isBooleanValue(). - * @return the representation of a Boolean value as a native Boolean value. + * @return The representation of a Boolean value as a native Boolean value. */ bool getBooleanValue() const; /** - * @return true if the term is a bit-vector value. + * @return True if the term is a bit-vector value. */ bool isBitVectorValue() const; /** - * Asserts isBitVectorValue(). - * @return the representation of a bit-vector value in string representation. - * Supported bases are 2 (bit string), 10 (decimal string) or 16 (hexadecimal - * string). + * Get the string representation of a bit-vector value. + * + * Supported values for `base` are `2` (bit string), `10` (decimal string) or + * `16` (hexadecimal string). + * + * @note Asserts isBitVectorValue(). + * + * @return The string representation of a bit-vector value. */ std::string getBitVectorValue(uint32_t base = 2) const; /** - * @return true if the term is an abstract value. + * @return True if the term is an abstract value. */ bool isUninterpretedSortValue() const; /** * Asserts isUninterpretedSortValue(). - * @return the representation of an uninterpreted sort value as a string. + * @return The representation of an uninterpreted sort value as a string. */ std::string getUninterpretedSortValue() const; /** - * @return true if the term is a tuple value. + * @return True if the term is a tuple value. */ bool isTupleValue() const; /** * Asserts isTupleValue(). - * @return the representation of a tuple value as a vector of terms. + * @return The representation of a tuple value as a vector of terms. */ std::vector getTupleValue() const; /** - * @return true if the term is a floating-point rounding mode value. + * @return True if the term is a floating-point rounding mode value. */ bool isRoundingModeValue() const; /** * Asserts isRoundingModeValue(). - * @return the floating-point rounding mode value held by the term. + * @return The floating-point rounding mode value held by the term. */ RoundingMode getRoundingModeValue() const; /** - * @return true if the term is the floating-point value for positive zero. + * @return True if the term is the floating-point value for positive zero. */ bool isFloatingPointPosZero() const; /** - * @return true if the term is the floating-point value for negative zero. + * @return True if the term is the floating-point value for negative zero. */ bool isFloatingPointNegZero() const; /** - * @return true if the term is the floating-point value for positive + * @return True if the term is the floating-point value for positive. * infinity. */ bool isFloatingPointPosInf() const; /** - * @return true if the term is the floating-point value for negative + * @return True if the term is the floating-point value for negative. * infinity. */ bool isFloatingPointNegInf() const; /** - * @return true if the term is the floating-point value for not a number. + * @return True if the term is the floating-point value for not a number. */ bool isFloatingPointNaN() const; /** - * @return true if the term is a floating-point value. + * @return True if the term is a floating-point value. */ bool isFloatingPointValue() const; /** * Asserts isFloatingPointValue(). - * @return the representation of a floating-point value as a tuple of the - * exponent width, the significand width and a bit-vector value. + * @return The representation of a floating-point value as a tuple of the + * exponent width, the significand width and a bit-vector value. */ std::tuple getFloatingPointValue() const; /** - * @return true if the term is a set value. + * @return True if the term is a set value. * * A term is a set value if it is considered to be a (canonical) constant set * value. A canonical set value is one whose AST is: @@ -1578,7 +1588,7 @@ class CVC5_EXPORT Term bool isSetValue() const; /** * Asserts isSetValue(). - * @return the representation of a set value as a set of terms. + * @return The representation of a set value as a set of terms. */ std::set getSetValue() const; @@ -1626,22 +1636,22 @@ class CVC5_EXPORT Term * returned in response to API calls such Solver::getValue() and * Solver::simplify(). * - * @return true if the term is a sequence value. + * @return True if the term is a sequence value. */ bool isSequenceValue() const; /** * Asserts isSequenceValue(). - * @return the representation of a sequence value as a vector of terms. + * @return The representation of a sequence value as a vector of terms. */ std::vector getSequenceValue() const; /** - * @return true if the term is a cardinality constraint + * @return True if the term is a cardinality constraint. */ bool isCardinalityConstraint() const; /** * Asserts isCardinalityConstraint(). - * @return the sort the cardinality constraint is for and its upper bound. + * @return The sort the cardinality constraint is for and its upper bound. */ std::pair getCardinalityConstraint() const; @@ -1670,13 +1680,13 @@ class CVC5_EXPORT Term /** * Constructor. - * @param slv the associated solver object - * @param n the internal node that is to be wrapped by this term - * @return the Term + * @param slv The associated solver object. + * @param n The internal node that is to be wrapped by this term. + * @return The Term. */ Term(const Solver* slv, const internal::Node& n); - /** @return the internal wrapped Node of this term. */ + /** @return The internal wrapped Node of this term. */ const internal::Node& getNode(void) const; /** @@ -1688,13 +1698,13 @@ class CVC5_EXPORT Term /** * Helper function that returns the kind of the term, which takes into * account special cases of the conversion for internal to external kinds. - * @return the kind of this term + * @return The kind of this term. */ Kind getKindHelper() const; /** - * @return true if the current term is a constant integer that is casted into - * real using the operator CAST_TO_REAL, and returns false otherwise + * @return True if the current term is a constant integer that is casted into + * real using the operator CAST_TO_REAL, and returns false otherwise */ bool isCastedReal() const; /** @@ -1708,26 +1718,26 @@ class CVC5_EXPORT Term /** * Serialize a term to given stream. - * @param out the output stream - * @param t the term to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param t The term to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Term& t) CVC5_EXPORT; /** * Serialize a vector of terms to given stream. - * @param out the output stream - * @param vector the vector of terms to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param vector The vector of terms to be serialized to the given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const std::vector& vector) CVC5_EXPORT; /** * Serialize a set of terms to the given stream. - * @param out the output stream - * @param set the set of terms to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param set The set of terms to be serialized to the given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const std::set& set) CVC5_EXPORT; @@ -1735,9 +1745,9 @@ std::ostream& operator<<(std::ostream& out, /** * Serialize an unordered_set of terms to the given stream. * - * @param out the output stream - * @param unordered_set the set of terms to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param unordered_set The set of terms to be serialized to the given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const std::unordered_set& unordered_set) @@ -1746,9 +1756,9 @@ std::ostream& operator<<(std::ostream& out, /** * Serialize a map of terms to the given stream. * - * @param out the output stream - * @param map the map of terms to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param map The map of terms to be serialized to the given stream. + * @return The output stream. */ template std::ostream& operator<<(std::ostream& out, @@ -1757,9 +1767,9 @@ std::ostream& operator<<(std::ostream& out, /** * Serialize an unordered_map of terms to the given stream. * - * @param out the output stream - * @param unordered_map the map of terms to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param unordered_map The map of terms to be serialized to the given stream. + * @return The output stream. */ template std::ostream& operator<<(std::ostream& out, @@ -1808,22 +1818,22 @@ class CVC5_EXPORT DatatypeConstructorDecl /** * Add datatype selector declaration. - * @param name the name of the datatype selector declaration to add - * @param sort the codomain sort of the datatype selector declaration to add + * @param name The name of the datatype selector declaration to add. + * @param sort The codomain sort of the datatype selector declaration to add. */ void addSelector(const std::string& name, const Sort& sort); /** * Add datatype selector declaration whose codomain type is the datatype * itself. - * @param name the name of the datatype selector declaration to add + * @param name The name of the datatype selector declaration to add. */ void addSelectorSelf(const std::string& name); /** * Add datatype selector declaration whose codomain sort is an unresolved * datatype with the given name. - * @param name the name of the datatype selector declaration to add - * @param unresDataypeName the name of the unresolved datatype. The codomain + * @param name The name of the datatype selector declaration to add. + * @param unresDataypeName The name of the unresolved datatype. The codomain * of the selector will be the resolved datatype with * the given name. */ @@ -1831,21 +1841,21 @@ class CVC5_EXPORT DatatypeConstructorDecl const std::string& unresDataypeName); /** - * @return true if this DatatypeConstructorDecl is a null declaration. + * @return True if this DatatypeConstructorDecl is a null declaration. */ bool isNull() const; /** - * @return a string representation of this datatype constructor declaration + * @return A string representation of this datatype constructor declaration. */ std::string toString() const; private: /** * Constructor. - * @param slv the associated solver object - * @param name the name of the datatype constructor - * @return the DatatypeConstructorDecl + * @param slv The associated solver object. + * @param name The name of the datatype constructor. + * @return The DatatypeConstructorDecl. */ DatatypeConstructorDecl(const Solver* slv, const std::string& name); @@ -1906,7 +1916,7 @@ class CVC5_EXPORT DatatypeDecl /** * Add datatype constructor declaration. - * @param ctor the datatype constructor declaration to add + * @param ctor The datatype constructor declaration to add. */ void addConstructor(const DatatypeConstructorDecl& ctor); @@ -1914,32 +1924,32 @@ class CVC5_EXPORT DatatypeDecl size_t getNumConstructors() const; /** - * Is this Datatype declaration parametric? + * Determine if this Datatype declaration is parametric. * * @warning This method is experimental and may change in future versions. */ bool isParametric() const; /** - * @return true if this DatatypeDecl is a null object + * @return True if this DatatypeDecl is a null object. */ bool isNull() const; /** - * @return a string representation of this datatype declaration + * @return A string representation of this datatype declaration. */ std::string toString() const; - /** @return the name of this datatype declaration. */ + /** @return The name of this datatype declaration. */ std::string getName() const; private: /** * Constructor. - * @param slv the associated solver object - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl + * @param slv The associated solver object. + * @param name The name of the datatype. + * @param isCoDatatype True if a codatatype is to be constructed. + * @return The DatatypeDecl. */ DatatypeDecl(const Solver* slv, const std::string& name, @@ -1948,10 +1958,10 @@ class CVC5_EXPORT DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the associated solver object - * @param name the name of the datatype - * @param param the sort parameter - * @param isCoDatatype true if a codatatype is to be constructed + * @param slv The associated solver object. + * @param name The name of the datatype. + * @param param The sort parameter. + * @param isCoDatatype True if a codatatype is to be constructed. */ DatatypeDecl(const Solver* slv, const std::string& name, @@ -1961,17 +1971,17 @@ class CVC5_EXPORT DatatypeDecl /** * Constructor for parameterized datatype declaration. * Create sorts parameter with Solver::mkParamSort(). - * @param slv the associated solver object - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed + * @param slv The associated solver object. + * @param name The name of the datatype. + * @param params A list of sort parameters. + * @param isCoDatatype True if a codatatype is to be constructed. */ DatatypeDecl(const Solver* slv, const std::string& name, const std::vector& params, bool isCoDatatype = false); - /** @return the internal wrapped Dtype of this datatype declaration. */ + /** @return The internal wrapped Dtype of this datatype declaration. */ internal::DType& getDatatype(void) const; /** @@ -2014,7 +2024,7 @@ class CVC5_EXPORT DatatypeSelector */ ~DatatypeSelector(); - /** @return the name of this Datatype selector. */ + /** @return The name of this Datatype selector. */ std::string getName() const; /** @@ -2024,7 +2034,7 @@ class CVC5_EXPORT DatatypeSelector * sort (Sort::isDatatypeSelector()), and should be used as the first * argument of Terms of kind #APPLY_SELECTOR. * - * @return the selector term + * @return The selector term. */ Term getTerm() const; @@ -2035,29 +2045,29 @@ class CVC5_EXPORT DatatypeSelector * updater Sort (Sort::isDatatypeUpdater()), and should be used as the first * argument of Terms of kind #APPLY_UPDATER. * - * @return the updater term + * @return The updater term. */ Term getUpdaterTerm() const; - /** @return the codomain sort of this selector. */ + /** @return The codomain sort of this selector. */ Sort getCodomainSort() const; /** - * @return true if this DatatypeSelector is a null object + * @return True if this DatatypeSelector is a null object. */ bool isNull() const; /** - * @return a string representation of this datatype selector + * @return A string representation of this datatype selector. */ std::string toString() const; private: /** * Constructor. - * @param slv the associated solver object - * @param stor the internal datatype selector to be wrapped - * @return the DatatypeSelector + * @param slv The associated solver object. + * @param stor The internal datatype selector to be wrapped. + * @return The DatatypeSelector. */ DatatypeSelector(const Solver* slv, const internal::DTypeSelector& stor); @@ -2099,7 +2109,7 @@ class CVC5_EXPORT DatatypeConstructor */ ~DatatypeConstructor(); - /** @return the name of this Datatype constructor. */ + /** @return The name of this Datatype constructor. */ std::string getName() const; /** @@ -2116,7 +2126,7 @@ class CVC5_EXPORT DatatypeConstructor * @note This method should not be used for parametric datatypes. Instead, * use the method DatatypeConstructor::getInstantiatedTerm() below. * - * @return the constructor term + * @return The constructor term. */ Term getTerm() const; @@ -2155,8 +2165,8 @@ class CVC5_EXPORT DatatypeConstructor * * @warning This method is experimental and may change in future versions. * - * @param retSort the desired return sort of the constructor - * @return the constructor term + * @param retSort The desired return sort of the constructor. + * @return The constructor term. */ Term getInstantiatedTerm(const Sort& retSort) const; @@ -2167,41 +2177,41 @@ class CVC5_EXPORT DatatypeConstructor * tester sort (Sort::isDatatypeConstructor()) which should be used as the * first argument of Terms of kind #APPLY_TESTER. * - * @return the tester term + * @return The tester term. */ Term getTesterTerm() const; /** - * @return the number of selectors (so far) of this Datatype constructor. + * @return The number of selectors (so far) of this Datatype constructor. */ size_t getNumSelectors() const; - /** @return the i^th DatatypeSelector. */ + /** @return The i^th DatatypeSelector. */ DatatypeSelector operator[](size_t index) const; /** * Get the datatype selector with the given name. * This is a linear search through the selectors, so in case of * multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the first datatype selector with the given name + * @param name The name of the datatype selector. + * @return The first datatype selector with the given name. */ DatatypeSelector operator[](const std::string& name) const; /** * Get the datatype selector with the given name. * This is a linear search through the selectors, so in case of * multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the first datatype selector with the given name + * @param name The name of the datatype selector. + * @return The first datatype selector with the given name. */ DatatypeSelector getSelector(const std::string& name) const; /** - * @return true if this DatatypeConstructor is a null object + * @return True if this DatatypeConstructor is a null object. */ bool isNull() const; /** - * @return a string representation of this datatype constructor + * @return A string representation of this datatype constructor. */ std::string toString() const; @@ -2237,55 +2247,55 @@ class CVC5_EXPORT DatatypeConstructor /** * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment + * @param it The iterator to assign to. + * @return The reference to the iterator after assignment. */ const_iterator& operator=(const const_iterator& it); /** * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal + * @param it The iterator to compare to for equality. + * @return True if the iterators are equal. */ bool operator==(const const_iterator& it) const; /** * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal + * @param it The iterator to compare to for disequality. + * @return True if the iterators are disequal. */ bool operator!=(const const_iterator& it) const; /** * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator& operator++(); /** * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator operator++(int); /** * Dereference operator. - * @return a reference to the selector this iterator points to + * @return A reference to the selector this iterator points to. */ const DatatypeSelector& operator*() const; /** * Dereference operator. - * @return a pointer to the selector this iterator points to + * @return A pointer to the selector this iterator points to. */ const DatatypeSelector* operator->() const; private: /** * Constructor. - * @param slv the associated Solver object - * @param ctor the internal datatype constructor to iterate over - * @param begin true if this is a begin() iterator + * @param slv The associated Solver object. + * @param ctor The internal datatype constructor to iterate over. + * @param begin True if this is a `begin()` iterator. */ const_iterator(const Solver* slv, const internal::DTypeConstructor& ctor, @@ -2311,29 +2321,29 @@ class CVC5_EXPORT DatatypeConstructor }; /** - * @return an iterator to the first selector of this constructor + * @return An iterator to the first selector of this constructor. */ const_iterator begin() const; /** - * @return an iterator to one-off-the-last selector of this constructor + * @return An iterator to one-off-the-last selector of this constructor. */ const_iterator end() const; private: /** * Constructor. - * @param slv the associated solver instance - * @param ctor the internal datatype constructor to be wrapped - * @return the DatatypeConstructor + * @param slv The associated solver instance. + * @param ctor The internal datatype constructor to be wrapped. + * @return The DatatypeConstructor. */ DatatypeConstructor(const Solver* slv, const internal::DTypeConstructor& ctor); /** * Return selector for name. - * @param name The name of selector to find - * @return the selector object for the name + * @param name The name of selector to find. + * @return The selector object for the name. */ DatatypeSelector getSelectorForName(const std::string& name) const; @@ -2375,8 +2385,8 @@ class CVC5_EXPORT Datatype /** * Get the datatype constructor at a given index. - * @param idx the index of the datatype constructor to return - * @return the datatype constructor with the given index + * @param idx The index of the datatype constructor to return. + * @return The datatype constructor with the given index. */ DatatypeConstructor operator[](size_t idx) const; @@ -2384,8 +2394,8 @@ class CVC5_EXPORT Datatype * Get the datatype constructor with the given name. * This is a linear search through the constructors, so in case of multiple, * similarly-named constructors, the first is returned. - * @param name the name of the datatype constructor - * @return the datatype constructor with the given name + * @param name The name of the datatype constructor. + * @return The datatype constructor with the given name. */ DatatypeConstructor operator[](const std::string& name) const; DatatypeConstructor getConstructor(const std::string& name) const; @@ -2394,62 +2404,66 @@ class CVC5_EXPORT Datatype * Get the datatype constructor with the given name. * This is a linear search through the constructors and their selectors, so * in case of multiple, similarly-named selectors, the first is returned. - * @param name the name of the datatype selector - * @return the datatype selector with the given name + * @param name The name of the datatype selector. + * @return The datatype selector with the given name. */ DatatypeSelector getSelector(const std::string& name) const; - /** @return the name of this Datatype. */ + /** @return The name of this Datatype. */ std::string getName() const; - /** @return the number of constructors for this Datatype. */ + /** @return The number of constructors for this Datatype. */ size_t getNumConstructors() const; /** + * Get the parameters of this datatype, if it is parametric. + * + * @note Asserts that this datatype is parametric. + * * @warning This method is experimental and may change in future versions. * - * @return the parameters of this datatype, if it is parametric. An exception - * is thrown if this datatype is not parametric. + * @return The parameters of this datatype. */ std::vector getParameters() const; /** * @warning This method is experimental and may change in future versions. - * @return true if this datatype is parametric + * @return True if this datatype is parametric. */ bool isParametric() const; - /** @return true if this datatype corresponds to a co-datatype */ + /** @return True if this datatype corresponds to a co-datatype */ bool isCodatatype() const; - /** @return true if this datatype corresponds to a tuple */ + /** @return True if this datatype corresponds to a tuple */ bool isTuple() const; /** * @warning This method is experimental and may change in future versions. - * @return true if this datatype corresponds to a record + * @return True if this datatype corresponds to a record. */ bool isRecord() const; - /** @return true if this datatype is finite */ + /** @return True if this datatype is finite */ bool isFinite() const; /** - * Is this datatype well-founded? If this datatype is not a codatatype, - * this returns false if there are no values of this datatype that are of - * finite size. + * Determine if this datatype is well-founded. + * + * If this datatype is not a codatatype, this returns false if there are no + * values of this datatype that are of finite size. * - * @return true if this datatype is well-founded + * @return True if this datatype is well-founded. */ bool isWellFounded() const; /** - * @return true if this Datatype is a null object + * @return True if this Datatype is a null object. */ bool isNull() const; /** - * @return a string representation of this datatype + * @return A string representation of this datatype. */ std::string toString() const; @@ -2485,55 +2499,55 @@ class CVC5_EXPORT Datatype /** * Assignment operator. - * @param it the iterator to assign to - * @return the reference to the iterator after assignment + * @param it The iterator to assign to. + * @return The reference to the iterator after assignment. */ const_iterator& operator=(const const_iterator& it); /** * Equality operator. - * @param it the iterator to compare to for equality - * @return true if the iterators are equal + * @param it The iterator to compare to for equality. + * @return True if the iterators are equal. */ bool operator==(const const_iterator& it) const; /** * Disequality operator. - * @param it the iterator to compare to for disequality - * @return true if the iterators are disequal + * @param it The iterator to compare to for disequality. + * @return True if the iterators are disequal. */ bool operator!=(const const_iterator& it) const; /** * Increment operator (prefix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator& operator++(); /** * Increment operator (postfix). - * @return a reference to the iterator after incrementing by one + * @return A reference to the iterator after incrementing by one. */ const_iterator operator++(int); /** * Dereference operator. - * @return a reference to the constructor this iterator points to + * @return A reference to the constructor this iterator points to. */ const DatatypeConstructor& operator*() const; /** * Dereference operator. - * @return a pointer to the constructor this iterator points to + * @return A pointer to the constructor this iterator points to. */ const DatatypeConstructor* operator->() const; private: /** * Constructor. - * @param slv the associated Solver object - * @param dtype the internal datatype to iterate over - * @param begin true if this is a begin() iterator + * @param slv The associated Solver object. + * @param dtype The internal datatype to iterate over. + * @param begin True if this is a begin() iterator. */ const_iterator(const Solver* slv, const internal::DType& dtype, bool begin); @@ -2557,35 +2571,35 @@ class CVC5_EXPORT Datatype }; /** - * @return an iterator to the first constructor of this datatype + * @return An iterator to the first constructor of this datatype. */ const_iterator begin() const; /** - * @return an iterator to one-off-the-last constructor of this datatype + * @return An iterator to one-off-the-last constructor of this datatype. */ const_iterator end() const; private: /** * Constructor. - * @param slv the associated solver instance - * @param dtype the internal datatype to be wrapped - * @return the Datatype + * @param slv The associated solver instance. + * @param dtype The internal datatype to be wrapped. + * @return The Datatype. */ Datatype(const Solver* slv, const internal::DType& dtype); /** * Return constructor for name. - * @param name The name of constructor to find - * @return the constructor object for the name + * @param name The name of constructor to find. + * @return The constructor object for the name. */ DatatypeConstructor getConstructorForName(const std::string& name) const; /** * Return selector for name. - * @param name The name of selector to find - * @return the selector object for the name + * @param name The name of selector to find. + * @return The selector object for the name. */ DatatypeSelector getSelectorForName(const std::string& name) const; @@ -2610,28 +2624,28 @@ class CVC5_EXPORT Datatype /** * Serialize a datatype declaration to given stream. - * @param out the output stream - * @param dtdecl the datatype declaration to be serialized to the given stream - * @return the output stream + * @param out The output stream. + * @param dtdecl The datatype declaration to be serialized to the given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const DatatypeDecl& dtdecl) CVC5_EXPORT; /** * Serialize a datatype constructor declaration to given stream. - * @param out the output stream - * @param ctordecl the datatype constructor declaration to be serialized - * @return the output stream + * @param out The output stream. + * @param ctordecl The datatype constructor declaration to be serialized. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const DatatypeConstructorDecl& ctordecl) CVC5_EXPORT; /** * Serialize a vector of datatype constructor declarations to given stream. - * @param out the output stream - * @param vector the vector of datatype constructor declarations to be + * @param out The output stream. + * @param vector The vector of datatype constructor declarations to be. * serialized to the given stream - * @return the output stream + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const std::vector& vector) @@ -2639,26 +2653,26 @@ std::ostream& operator<<(std::ostream& out, /** * Serialize a datatype to given stream. - * @param out the output stream - * @param dtype the datatype to be serialized to given stream - * @return the output stream + * @param out The output stream. + * @param dtype The datatype to be serialized to given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Datatype& dtype) CVC5_EXPORT; /** * Serialize a datatype constructor to given stream. - * @param out the output stream - * @param ctor the datatype constructor to be serialized to given stream - * @return the output stream + * @param out The output stream. + * @param ctor The datatype constructor to be serialized to given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const DatatypeConstructor& ctor) CVC5_EXPORT; /** * Serialize a datatype selector to given stream. - * @param out the output stream - * @param stor the datatype selector to be serialized to given stream - * @return the output stream + * @param out The output stream. + * @param stor The datatype selector to be serialized to given stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const DatatypeSelector& stor) CVC5_EXPORT; @@ -2680,33 +2694,33 @@ class CVC5_EXPORT Grammar public: /** * Add \p rule to the set of rules corresponding to \p ntSymbol. - * @param ntSymbol the non-terminal to which the rule is added - * @param rule the rule to add + * @param ntSymbol The non-terminal to which the rule is added. + * @param rule The rule to add. */ void addRule(const Term& ntSymbol, const Term& rule); /** * Add \p rules to the set of rules corresponding to \p ntSymbol. - * @param ntSymbol the non-terminal to which the rules are added - * @param rules the rules to add + * @param ntSymbol The non-terminal to which the rules are added. + * @param rules The rules to add. */ void addRules(const Term& ntSymbol, const std::vector& rules); /** * Allow \p ntSymbol to be an arbitrary constant. - * @param ntSymbol the non-terminal allowed to be any constant + * @param ntSymbol The non-terminal allowed to be any constant. */ void addAnyConstant(const Term& ntSymbol); /** * Allow \p ntSymbol to be any input variable to corresponding * synth-fun/synth-inv with the same sort as \p ntSymbol. - * @param ntSymbol the non-terminal allowed to be any input variable + * @param ntSymbol The non-terminal allowed to be any input variable. */ void addAnyVariable(const Term& ntSymbol); /** - * @return a string representation of this grammar. + * @return A string representation of this grammar. */ std::string toString() const; @@ -2718,16 +2732,16 @@ class CVC5_EXPORT Grammar private: /** * Constructor. - * @param slv the solver that created this grammar - * @param sygusVars the input variables to synth-fun/synth-var - * @param ntSymbols the non-terminals of this grammar + * @param slv The solver that created this grammar. + * @param sygusVars The input variables to synth-fun/synth-var. + * @param ntSymbols The non-terminals of this grammar. */ Grammar(const Solver* slv, const std::vector& sygusVars, const std::vector& ntSymbols); /** - * @return the resolved datatype of the Start symbol of the grammar + * @return The resolved datatype of the Start symbol of the grammar. */ Sort resolve(); @@ -2744,9 +2758,9 @@ class CVC5_EXPORT Grammar * with bound variables via purifySygusGTerm, and binding these variables * via a lambda. * - * @param dt the non-terminal's datatype to which a constructor is added - * @param term the sygus operator of the constructor - * @param ntsToUnres mapping from non-terminals to their unresolved sorts + * @param dt The non-terminal's datatype to which a constructor is added. + * @param term The sygus operator of the constructor. + * @param ntsToUnres Mapping from non-terminals to their unresolved sorts. */ void addSygusConstructorTerm( DatatypeDecl& dt, @@ -2765,11 +2779,11 @@ class CVC5_EXPORT Grammar * (which should be bound by a lambda), and \p cargs contains the sorts of * the arguments of the sygus constructor. * - * @param term the term to purify - * @param args the free variables in the term returned by this method - * @param cargs the sorts of the arguments of the sygus constructor - * @param ntsToUnres mapping from non-terminals to their unresolved sorts - * @return the purfied term + * @param term The term to purify. + * @param args The free variables in the term returned by this method. + * @param cargs The sorts of the arguments of the sygus constructor. + * @param ntsToUnres Mapping from non-terminals to their unresolved sorts. + * @return The purfied term. */ Term purifySygusGTerm(const Term& term, std::vector& args, @@ -2781,16 +2795,16 @@ class CVC5_EXPORT Grammar * whose sort is argument \p sort. This method should be called when the * sygus grammar term (Variable sort) is encountered. * - * @param dt the non-terminal's datatype to which the constructors are added - * @param sort the sort of the sygus variables to add + * @param dt The non-terminal's datatype to which the constructors are added. + * @param sort The sort of the sygus variables to add. */ void addSygusConstructorVariables(DatatypeDecl& dt, const Sort& sort) const; /** * Check if \p rule contains variables that are neither parameters of * the corresponding synthFun/synthInv nor non-terminals. - * @param rule the non-terminal allowed to be any constant - * @return true if \p rule contains free variables and false otherwise + * @param rule The non-terminal allowed to be any constant. + * @return True if \p rule contains free variables and false otherwise. */ bool containsFreeVariables(const Term& rule) const; @@ -2812,9 +2826,9 @@ class CVC5_EXPORT Grammar /** * Serialize a grammar to given stream. - * @param out the output stream - * @param g the grammar to be serialized to the given output stream - * @return the output stream + * @param out The output stream. + * @param g The grammar to be serialized to the given output stream. + * @return The output stream. */ std::ostream& operator<<(std::ostream& out, const Grammar& g) CVC5_EXPORT; @@ -3011,19 +3025,19 @@ class CVC5_EXPORT Stat Stat& operator=(const Stat& s); /** - * Is this value intended for internal use only? - * @return Whether this is an internal statistic. + * Determine if this value is intended for internal use only. + * @return True if this is an internal statistic. */ bool isInternal() const; /** - * Does this value hold the default value? - * @return Whether this is a defaulted statistic. + * Determine if this value holds the default value. + * @return True if this is a defaulted statistic. */ bool isDefault() const; /** - * Is this value an integer? - * @return Whether the value is an integer. + * Determine if this value is an integer. + * @return True if this value is an integer. */ bool isInt() const; /** @@ -3032,8 +3046,8 @@ class CVC5_EXPORT Stat */ int64_t getInt() const; /** - * Is this value a double? - * @return Whether the value is a double. + * Determine if this value is a double. + * @return True if this value is a double. */ bool isDouble() const; /** @@ -3042,8 +3056,8 @@ class CVC5_EXPORT Stat */ double getDouble() const; /** - * Is this value a string? - * @return Whether the value is a string. + * Determine if this value is a string. + * @return True if this value is a string. */ bool isString() const; /** @@ -3052,8 +3066,8 @@ class CVC5_EXPORT Stat */ const std::string& getString() const; /** - * Is this value a histogram? - * @return Whether the value is a histogram. + * Determine if this value is a histogram. + * @return True if this value is a histogram. */ bool isHistogram() const; /** @@ -3191,7 +3205,7 @@ class CVC5_EXPORT Solver /** * Constructor. - * @return the Solver + * @return The Solver. */ Solver(); @@ -3211,66 +3225,66 @@ class CVC5_EXPORT Solver /* .................................................................... */ /** - * @return sort null + * @return Sort null. */ Sort getNullSort() const; /** - * @return sort Boolean + * @return Sort Boolean. */ Sort getBooleanSort() const; /** - * @return sort Integer (in cvc5, Integer is a subtype of Real) + * @return Sort Integer (in cvc5, Integer is a subtype of Real) */ Sort getIntegerSort() const; /** - * @return sort Real + * @return Sort Real. */ Sort getRealSort() const; /** - * @return sort RegExp + * @return Sort RegExp. */ Sort getRegExpSort() const; /** - * @return sort RoundingMode + * @return Sort RoundingMode. */ Sort getRoundingModeSort() const; /** - * @return sort String + * @return Sort String. */ Sort getStringSort() const; /** * Create an array sort. - * @param indexSort the array index sort - * @param elemSort the array element sort - * @return the array sort + * @param indexSort The array index sort. + * @param elemSort The array element sort. + * @return The array sort. */ Sort mkArraySort(const Sort& indexSort, const Sort& elemSort) const; /** * Create a bit-vector sort. - * @param size the bit-width of the bit-vector sort - * @return the bit-vector sort + * @param size The bit-width of the bit-vector sort. + * @return The bit-vector sort. */ Sort mkBitVectorSort(uint32_t size) const; /** * Create a floating-point sort. - * @param exp the bit-width of the exponent of the floating-point sort. - * @param sig the bit-width of the significand of the floating-point sort. + * @param exp The bit-width of the exponent of the floating-point sort. + * @param sig The bit-width of the significand of the floating-point sort. */ Sort mkFloatingPointSort(uint32_t exp, uint32_t sig) const; /** * Create a datatype sort. - * @param dtypedecl the datatype declaration from which the sort is created - * @return the datatype sort + * @param dtypedecl The datatype declaration from which the sort is created. + * @return The datatype sort. */ Sort mkDatatypeSort(const DatatypeDecl& dtypedecl) const; @@ -3278,17 +3292,17 @@ class CVC5_EXPORT Solver * Create a vector of datatype sorts. The names of the datatype declarations * must be distinct. * - * @param dtypedecls the datatype declarations from which the sort is created - * @return the datatype sorts + * @param dtypedecls The datatype declarations from which the sort is created. + * @return The datatype sorts. */ std::vector mkDatatypeSorts( const std::vector& dtypedecls) const; /** * Create function sort. - * @param sorts the sort of the function arguments - * @param codomain the sort of the function return value - * @return the function sort + * @param sorts The sort of the function arguments. + * @param codomain The sort of the function return value. + * @return The function sort. */ Sort mkFunctionSort(const std::vector& sorts, const Sort& codomain) const; @@ -3298,8 +3312,8 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param symbol the name of the sort - * @return the sort parameter + * @param symbol The name of the sort. + * @return The sort parameter. */ Sort mkParamSort( const std::optional& symbol = std::nullopt) const; @@ -3309,8 +3323,8 @@ class CVC5_EXPORT Solver * * This is equivalent to calling mkFunctionSort() with the Boolean sort as the * codomain. - * @param sorts the list of sorts of the predicate - * @return the predicate sort + * @param sorts The list of sorts of the predicate. + * @return The predicate sort. */ Sort mkPredicateSort(const std::vector& sorts) const; @@ -3319,37 +3333,37 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param fields the list of fields of the record - * @return the record sort + * @param fields The list of fields of the record. + * @return The record sort. */ Sort mkRecordSort( const std::vector>& fields) const; /** * Create a set sort. - * @param elemSort the sort of the set elements - * @return the set sort + * @param elemSort The sort of the set elements. + * @return The set sort. */ Sort mkSetSort(const Sort& elemSort) const; /** * Create a bag sort. - * @param elemSort the sort of the bag elements - * @return the bag sort + * @param elemSort The sort of the bag elements. + * @return The bag sort. */ Sort mkBagSort(const Sort& elemSort) const; /** * Create a sequence sort. - * @param elemSort the sort of the sequence elements - * @return the sequence sort + * @param elemSort The sort of the sequence elements. + * @return The sequence sort. */ Sort mkSequenceSort(const Sort& elemSort) const; /** * Create an uninterpreted sort. - * @param symbol the name of the sort - * @return the uninterpreted sort + * @param symbol The name of the sort. + * @return The uninterpreted sort. */ Sort mkUninterpretedSort( const std::optional& symbol = std::nullopt) const; @@ -3360,9 +3374,9 @@ class CVC5_EXPORT Solver * This is for creating yet unresolved sort placeholders for mutually * recursive parametric datatypes. * - * @param symbol the symbol of the sort - * @param arity the number of sort parameters of the sort - * @return the unresolved sort + * @param symbol The symbol of the sort. + * @param arity The number of sort parameters of the sort. + * @return The unresolved sort. * * @warning This method is experimental and may change in future versions. */ @@ -3374,9 +3388,9 @@ class CVC5_EXPORT Solver * * An uninterpreted sort constructor is an uninterpreted sort with arity > 0. * - * @param symbol the symbol of the sort - * @param arity the arity of the sort (must be > 0) - * @return the uninterpreted sort constructor sort + * @param symbol The symbol of the sort. + * @param arity The arity of the sort (must be > 0) + * @return The uninterpreted sort constructor sort. */ Sort mkUninterpretedSortConstructorSort( size_t arity, @@ -3384,8 +3398,8 @@ class CVC5_EXPORT Solver /** * Create a tuple sort. - * @param sorts of the elements of the tuple - * @return the tuple sort + * @param sorts Of the elements of the tuple. + * @return The tuple sort. */ Sort mkTupleSort(const std::vector& sorts) const; @@ -3395,26 +3409,26 @@ class CVC5_EXPORT Solver /** * Create n-ary term of given kind. - * @param kind the kind of the term - * @param children the children of the term - * @return the Term */ + * @param kind The kind of the term. + * @param children The children of the term. + * @return The Term */ Term mkTerm(Kind kind, const std::vector& children = {}) const; /** * Create n-ary term of given kind from a given operator. * Create operators with mkOp(). - * @param op the operator - * @param children the children of the term - * @return the Term + * @param op The operator. + * @param children The children of the term. + * @return The Term. */ Term mkTerm(const Op& op, const std::vector& children = {}) const; /** * Create a tuple term. Terms are automatically converted if sorts are * compatible. - * @param sorts The sorts of the elements in the tuple - * @param terms The elements in the tuple - * @return the tuple Term + * @param sorts The sorts of the elements in the tuple. + * @param terms The elements in the tuple. + * @return The tuple Term. */ Term mkTuple(const std::vector& sorts, const std::vector& terms) const; @@ -3443,8 +3457,8 @@ class CVC5_EXPORT Solver * - #TUPLE_PROJECT * * See cvc5::Kind for a description of the parameters. - * @param kind the kind of the operator - * @param args the arguments (indices) of the operator + * @param kind The kind of the operator. + * @param args The arguments (indices) of the operator. * * @note If ``args`` is empty, the Op simply wraps the cvc5::Kind. The * Kind can be used in Solver::mkTerm directly without creating an Op @@ -3462,8 +3476,8 @@ class CVC5_EXPORT Solver * Create operator of kind: * - DIVISIBLE (to support arbitrary precision integers) * See cvc5::Kind for a description of the parameters. - * @param kind the kind of the operator - * @param arg the string argument to this operator + * @param kind The kind of the operator. + * @param arg The string argument to this operator. */ Op mkOp(Kind kind, const std::string& arg) const; @@ -3473,95 +3487,95 @@ class CVC5_EXPORT Solver /** * Create a Boolean true constant. - * @return the true constant + * @return The true constant. */ Term mkTrue() const; /** * Create a Boolean false constant. - * @return the false constant + * @return The false constant. */ Term mkFalse() const; /** * Create a Boolean constant. - * @return the Boolean constant - * @param val the value of the constant + * @return The Boolean constant. + * @param val The value of the constant. */ Term mkBoolean(bool val) const; /** * Create a constant representing the number Pi. - * @return a constant representing Pi + * @return A constant representing Pi. */ Term mkPi() const; /** * Create an integer constant from a string. - * @param s the string representation of the constant, may represent an + * @param s The string representation of the constant, may represent an * integer (e.g., "123"). - * @return a constant of sort Integer assuming 's' represents an integer) + * @return A constant of sort Integer assuming 's' represents an integer) */ Term mkInteger(const std::string& s) const; /** * Create an integer constant from a c++ int. - * @param val the value of the constant - * @return a constant of sort Integer + * @param val The value of the constant. + * @return A constant of sort Integer. */ Term mkInteger(int64_t val) const; /** * Create a real constant from a string. - * @param s the string representation of the constant, may represent an + * @param s The string representation of the constant, may represent an * integer (e.g., "123") or real constant (e.g., "12.34" or "12/34"). - * @return a constant of sort Real + * @return A constant of sort Real. */ Term mkReal(const std::string& s) const; /** * Create a real constant from an integer. - * @param val the value of the constant - * @return a constant of sort Integer + * @param val The value of the constant. + * @return A constant of sort Integer. */ Term mkReal(int64_t val) const; /** * Create a real constant from a rational. - * @param num the value of the numerator - * @param den the value of the denominator - * @return a constant of sort Real + * @param num The value of the numerator. + * @param den The value of the denominator. + * @return A constant of sort Real. */ Term mkReal(int64_t num, int64_t den) const; /** * Create a regular expression all (re.all) term. - * @return the all term + * @return The all term. */ Term mkRegexpAll() const; /** * Create a regular expression allchar (re.allchar) term. - * @return the allchar term + * @return The allchar term. */ Term mkRegexpAllchar() const; /** * Create a regular expression none (re.none) term. - * @return the none term + * @return The none term. */ Term mkRegexpNone() const; /** * Create a constant representing an empty set of the given sort. - * @param sort the sort of the set elements. - * @return the empty set constant + * @param sort The sort of the set elements. + * @return The empty set constant. */ Term mkEmptySet(const Sort& sort) const; /** * Create a constant representing an empty bag of the given sort. - * @param sort the sort of the bag elements. - * @return the empty bag constant + * @param sort The sort of the bag elements. + * @return The empty bag constant. */ Term mkEmptyBag(const Sort& sort) const; @@ -3570,7 +3584,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return the separation logic empty term + * @return The separation logic empty term. */ Term mkSepEmp() const; @@ -3579,18 +3593,18 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param sort the sort of the nil term - * @return the separation logic nil term + * @param sort The sort of the nil term. + * @return The separation logic nil term. */ Term mkSepNil(const Sort& sort) const; /** * Create a String constant from a `std::string` which may contain SMT-LIB * compatible escape sequences like `\u1234` to encode unicode characters. - * @param s the string this constant represents - * @param useEscSequences determines whether escape sequences in `s` should + * @param s The string this constant represents. + * @param useEscSequences Determines whether escape sequences in `s` should. * be converted to the corresponding unicode character - * @return the String constant + * @return The String constant. */ Term mkString(const std::string& s, bool useEscSequences = false) const; @@ -3598,22 +3612,22 @@ class CVC5_EXPORT Solver * Create a String constant from a `std::wstring`. * This method does not support escape sequences as `std::wstring` already * supports unicode characters. - * @param s the string this constant represents - * @return the String constant + * @param s The string this constant represents. + * @return The String constant. */ Term mkString(const std::wstring& s) const; /** * Create an empty sequence of the given element sort. * @param sort The element sort of the sequence. - * @return the empty sequence with given element sort. + * @return The empty sequence with given element sort. */ Term mkEmptySequence(const Sort& sort) const; /** * Create a universe set of the given sort. - * @param sort the sort of the set elements - * @return the universe set constant + * @param sort The sort of the set elements. + * @return The universe set constant. */ Term mkUniverseSet(const Sort& sort) const; @@ -3622,9 +3636,9 @@ class CVC5_EXPORT Solver * * @note The given value must fit into a bit-vector of the given size. * - * @param size the bit-width of the bit-vector sort - * @param val the value of the constant - * @return the bit-vector constant + * @param size The bit-width of the bit-vector sort. + * @param val The value of the constant. + * @return The bit-vector constant. */ Term mkBitVector(uint32_t size, uint64_t val = 0) const; @@ -3634,73 +3648,74 @@ class CVC5_EXPORT Solver * * @note The given value must fit into a bit-vector of the given size. * - * @param size the bit-width of the constant - * @param s the string representation of the constant - * @param base the base of the string representation (2, 10, or 16) - * @return the bit-vector constant + * @param size The bit-width of the constant. + * @param s The string representation of the constant. + * @param base The base of the string representation (2, 10, or 16) + * @return The bit-vector constant. */ Term mkBitVector(uint32_t size, const std::string& s, uint32_t base) const; /** * Create a constant array with the provided constant value stored at every * index - * @param sort the sort of the constant array (must be an array sort) - * @param val the constant value to store (must match the sort's element sort) - * @return the constant array term + * @param sort The sort of the constant array (must be an array sort). + * @param val The constant value to store (must match the sort's element + * sort). + * @return The constant array term. */ Term mkConstArray(const Sort& sort, const Term& val) const; /** * Create a positive infinity floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant + * @param exp Number of bits in the exponent. + * @param sig Number of bits in the significand. + * @return The floating-point constant. */ Term mkFloatingPointPosInf(uint32_t exp, uint32_t sig) const; /** * Create a negative infinity floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant + * @param exp Number of bits in the exponent. + * @param sig Number of bits in the significand. + * @return The floating-point constant. */ Term mkFloatingPointNegInf(uint32_t exp, uint32_t sig) const; /** * Create a not-a-number (NaN) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant + * @param exp Number of bits in the exponent. + * @param sig Number of bits in the significand. + * @return The floating-point constant. */ Term mkFloatingPointNaN(uint32_t exp, uint32_t sig) const; /** * Create a positive zero (+0.0) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant + * @param exp Number of bits in the exponent. + * @param sig Number of bits in the significand. + * @return The floating-point constant. */ Term mkFloatingPointPosZero(uint32_t exp, uint32_t sig) const; /** * Create a negative zero (-0.0) floating-point constant. - * @param exp Number of bits in the exponent - * @param sig Number of bits in the significand - * @return the floating-point constant + * @param exp Number of bits in the exponent. + * @param sig Number of bits in the significand. + * @return The floating-point constant. */ Term mkFloatingPointNegZero(uint32_t exp, uint32_t sig) const; /** * Create a roundingmode constant. - * @param rm the floating point rounding mode this constant represents + * @param rm The floating point rounding mode this constant represents. */ Term mkRoundingMode(RoundingMode rm) const; /** * Create a floating-point constant. - * @param exp Size of the exponent - * @param sig Size of the significand - * @param val Value of the floating-point constant as a bit-vector term + * @param exp Size of the exponent. + * @param sig Size of the significand. + * @param val Value of the floating-point constant as a bit-vector term. */ Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const; @@ -3709,9 +3724,9 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param sort the sort the cardinality constraint is for - * @param upperBound the upper bound on the cardinality of the sort - * @return the cardinality constraint + * @param sort The sort the cardinality constraint is for. + * @param upperBound The upper bound on the cardinality of the sort. + * @return The cardinality constraint. */ Term mkCardinalityConstraint(const Sort& sort, uint32_t upperBound) const; @@ -3731,9 +3746,9 @@ class CVC5_EXPORT Solver * (declare-fun () ) * \endverbatim * - * @param sort the sort of the constant - * @param symbol the name of the constant (optional) - * @return the constant + * @param sort The sort of the constant. + * @param symbol The name of the constant (optional). + * @return The constant. */ Term mkConst(const Sort& sort, const std::optional& symbol = std::nullopt) const; @@ -3741,9 +3756,9 @@ class CVC5_EXPORT Solver /** * Create a bound variable to be used in a binder (i.e. a quantifier, a * lambda, or a witness binder). - * @param sort the sort of the variable - * @param symbol the name of the variable (optional) - * @return the variable + * @param sort The sort of the variable. + * @param symbol The name of the variable (optional). + * @return The variable. */ Term mkVar(const Sort& sort, const std::optional& symbol = std::nullopt) const; @@ -3754,8 +3769,8 @@ class CVC5_EXPORT Solver /** * Create a datatype constructor declaration. - * @param name the name of the datatype constructor - * @return the DatatypeConstructorDecl + * @param name The name of the datatype constructor. + * @return The DatatypeConstructorDecl. */ DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); @@ -3765,9 +3780,9 @@ class CVC5_EXPORT Solver /** * Create a datatype declaration. - * @param name the name of the datatype - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl + * @param name The name of the datatype. + * @param isCoDatatype True if a codatatype is to be constructed. + * @return The DatatypeDecl. */ DatatypeDecl mkDatatypeDecl(const std::string& name, bool isCoDatatype = false); @@ -3778,10 +3793,10 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param name the name of the datatype - * @param params a list of sort parameters - * @param isCoDatatype true if a codatatype is to be constructed - * @return the DatatypeDecl + * @param name The name of the datatype. + * @param params A list of sort parameters. + * @param isCoDatatype True if a codatatype is to be constructed. + * @return The DatatypeDecl. */ DatatypeDecl mkDatatypeDecl(const std::string& name, const std::vector& params, @@ -3798,8 +3813,8 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param t the formula to simplify - * @return the simplified formula + * @param t The formula to simplify. + * @return The simplified formula. */ Term simplify(const Term& t); @@ -3814,7 +3829,7 @@ class CVC5_EXPORT Solver * (assert ) * \endverbatim * - * @param term the formula to assert + * @param term The formula to assert. */ void assertFormula(const Term& term) const; @@ -3829,7 +3844,7 @@ class CVC5_EXPORT Solver * (check-sat) * \endverbatim * - * @return the result of the satisfiability check. + * @return The result of the satisfiability check. */ Result checkSat() const; @@ -3844,8 +3859,8 @@ class CVC5_EXPORT Solver * (check-sat-assuming ( )) * \endverbatim * - * @param assumption the formula to assume - * @return the result of the satisfiability check. + * @param assumption The formula to assume. + * @return The result of the satisfiability check. */ Result checkSatAssuming(const Term& assumption) const; @@ -3860,8 +3875,8 @@ class CVC5_EXPORT Solver * (check-sat-assuming ( + )) * \endverbatim * - * @param assumptions the formulas to assume - * @return the result of the satisfiability check. + * @param assumptions The formulas to assume. + * @return The result of the satisfiability check. */ Result checkSatAssuming(const std::vector& assumptions) const; @@ -3876,9 +3891,9 @@ class CVC5_EXPORT Solver * (declare-datatype ) * \endverbatim * - * @param symbol the name of the datatype sort - * @param ctors the constructor declarations of the datatype sort - * @return the datatype sort + * @param symbol The name of the datatype sort. + * @param ctors The constructor declarations of the datatype sort. + * @return The datatype sort. */ Sort declareDatatype(const std::string& symbol, const std::vector& ctors) const; @@ -3894,10 +3909,10 @@ class CVC5_EXPORT Solver * (declare-fun ( * ) ) * \endverbatim * - * @param symbol the name of the function - * @param sorts the sorts of the parameters to this function - * @param sort the sort of the return value of this function - * @return the function + * @param symbol The name of the function. + * @param sorts The sorts of the parameters to this function. + * @param sort The sort of the return value of this function. + * @return The function. */ Term declareFun(const std::string& symbol, const std::vector& sorts, @@ -3919,9 +3934,9 @@ class CVC5_EXPORT Solver * mkUninterpretedSortConstructorSort(const std::string&, size_t arity) const * if arity > 0. * - * @param symbol the name of the sort - * @param arity the arity of the sort - * @return the sort + * @param symbol The name of the sort. + * @param arity The arity of the sort. + * @return The sort. */ Sort declareSort(const std::string& symbol, uint32_t arity) const; @@ -3936,13 +3951,13 @@ class CVC5_EXPORT Solver * (define-fun ) * \endverbatim * - * @param symbol the name of the function - * @param bound_vars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function + * @param symbol The name of the function. + * @param bound_vars The parameters to this function. + * @param sort The sort of the return value of this function. + * @param term The function body. + * @param global Determines whether this definition is global (i.e. persists + * when popping the context). + * @return The function. */ Term defineFun(const std::string& symbol, const std::vector& bound_vars, @@ -3961,13 +3976,13 @@ class CVC5_EXPORT Solver * (define-fun-rec ) * \endverbatim * - * @param symbol the name of the function - * @param bound_vars the parameters to this function - * @param sort the sort of the return value of this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function + * @param symbol The name of the function. + * @param bound_vars The parameters to this function. + * @param sort The sort of the return value of this function. + * @param term The function body. + * @param global Determines whether this definition is global (i.e. persists + * when popping the context). + * @return The function. */ Term defineFunRec(const std::string& symbol, const std::vector& bound_vars, @@ -3987,12 +4002,12 @@ class CVC5_EXPORT Solver * \endverbatim * * Create parameter 'fun' with mkConst(). - * @param fun the sorted function - * @param bound_vars the parameters to this function - * @param term the function body - * @param global determines whether this definition is global (i.e. persists - * when popping the context) - * @return the function + * @param fun The sorted function. + * @param bound_vars The parameters to this function. + * @param term The function body. + * @param global Determines whether this definition is global (i.e. persists + * when popping the context). + * @return The function. */ Term defineFunRec(const Term& fun, const std::vector& bound_vars, @@ -4014,11 +4029,11 @@ class CVC5_EXPORT Solver * \endverbatim * * Create elements of parameter 'funs' with mkConst(). - * @param funs the sorted functions - * @param bound_vars the list of parameters to the functions - * @param terms the list of function bodies of the functions - * @param global determines whether this definition is global (i.e. persists - * when popping the context) + * @param funs The sorted functions. + * @param bound_vars The list of parameters to the functions. + * @param terms The list of function bodies of the functions. + * @param global Determines whether this definition is global (i.e. persists + * when popping the context). */ void defineFunsRec(const std::vector& funs, const std::vector>& bound_vars, @@ -4036,7 +4051,7 @@ class CVC5_EXPORT Solver * (get-assertions) * \endverbatim * - * @return the list of asserted formulas + * @return The list of asserted formulas. */ std::vector getAssertions() const; @@ -4051,7 +4066,7 @@ class CVC5_EXPORT Solver * (get-info ) * \endverbatim * - * @return the info + * @return The info. */ std::string getInfo(const std::string& flag) const; @@ -4066,29 +4081,29 @@ class CVC5_EXPORT Solver * (get-option ) * \endverbatim * - * @param option the option for which the value is queried - * @return a string representation of the option value + * @param option The option for which the value is queried. + * @return A string representation of the option value. */ std::string getOption(const std::string& option) const; /** * Get all option names that can be used with `setOption`, `getOption` and * `getOptionInfo`. - * @return all option names + * @return All option names. */ std::vector getOptionNames() const; /** * Get some information about the given option. Check the `OptionInfo` class * for more details on which information is available. - * @return information about the given option + * @return Information about the given option. */ OptionInfo getOptionInfo(const std::string& option) const; /** * Get the driver options, which provide access to options that can not be * communicated properly via getOption() and getOptionInfo(). - * @return a DriverOptions object. + * @return A DriverOptions object. */ DriverOptions getDriverOptions() const; @@ -4106,7 +4121,7 @@ class CVC5_EXPORT Solver * :ref:`produce-unsat-assumptions `. * \endverbatim * - * @return the set of unsat assumptions. + * @return The set of unsat assumptions. */ std::vector getUnsatAssumptions() const; @@ -4131,7 +4146,7 @@ class CVC5_EXPORT Solver * returned by this method. * \endverbatim * - * @return a set of terms representing the unsatisfiable core + * @return A set of terms representing the unsatisfiable core. */ std::vector getUnsatCore() const; @@ -4141,7 +4156,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return a map from (a subset of) the input assertions to a real value that + * @return A map from (a subset of) the input assertions to a real value that. * is an estimate of how difficult each assertion was to solve. * Unmentioned assertions can be assumed to have zero difficulty. */ @@ -4159,12 +4174,13 @@ class CVC5_EXPORT Solver * * Requires to enable option * :ref:`produce-proofs `. + * The string representation depends on the value of option + * :ref:`produce-proofs `. * \endverbatim * * @warning This method is experimental and may change in future versions. * - * @return a string representing the proof, according to the value of - * proof-format-mode. + * @return A string representing the proof. */ std::string getProof() const; @@ -4174,7 +4190,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return a list of literals that were learned at top-level. + * @return A list of literals that were learned at top-level. */ std::vector getLearnedLiterals() const; @@ -4189,8 +4205,8 @@ class CVC5_EXPORT Solver * (get-value ( )) * \endverbatim * - * @param term the term for which the value is queried - * @return the value of the given term + * @param term The term for which the value is queried. + * @return The value of the given term. */ Term getValue(const Term& term) const; @@ -4205,8 +4221,8 @@ class CVC5_EXPORT Solver * (get-value ( * )) * \endverbatim * - * @param terms the terms for which the value is queried - * @return the values of the given terms + * @param terms The terms for which the value is queried. + * @return The values of the given terms. */ std::vector getValue(const std::vector& terms) const; @@ -4215,8 +4231,8 @@ class CVC5_EXPORT Solver * current model interprets s as the finite sort whose domain elements are * given in the return value of this method. * - * @param s The uninterpreted sort in question - * @return the domain elements of s in the current model + * @param s The uninterpreted sort in question. + * @return The domain elements of s in the current model. */ std::vector getModelDomainElements(const Sort& s) const; @@ -4230,8 +4246,8 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param v The term in question - * @return true if v is a model core symbol + * @param v The term in question. + * @return True if v is a model core symbol. */ bool isModelCoreSymbol(const Term& v) const; @@ -4251,11 +4267,12 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param sorts The list of uninterpreted sorts that should be printed in the - * model. + * @param sorts The list of uninterpreted sorts that should be printed in + * the model. * @param vars The list of free constants that should be printed in the - * model. A subset of these may be printed based on isModelCoreSymbol. - * @return a string representing the model. + * model. A subset of these may be printed based on + * isModelCoreSymbol(). + * @return A string representing the model. */ std::string getModel(const std::vector& sorts, const std::vector& vars) const; @@ -4276,13 +4293,13 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param q a quantified formula of the form + * @param q A quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ * where * @f$Q\bar{x}@f$ is a set of quantified variables of the form * @f$Q x_1...x_k@f$ and * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula - * @return a formula @f$\phi@f$ such that, given the current set of formulas + * @return A formula @f$\phi@f$ such that, given the current set of formulas * @f$A@f$ asserted to this solver: * - @f$(A \wedge q)@f$ and @f$(A \wedge \phi)@f$ are equivalent * - @f$\phi@f$ is quantifier-free formula containing only free @@ -4307,13 +4324,13 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param q a quantified formula of the form + * @param q A quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ * where * @f$Q\bar{x}@f$ is a set of quantified variables of the form * @f$Q x_1...x_k@f$ and * @f$P( x_1...x_i, y_1...y_j )@f$ is a quantifier-free formula - * @return a formula @f$\phi@f$ such that, given the current set of formulas + * @return A formula @f$\phi@f$ such that, given the current set of formulas * @f$A@f$ asserted to this solver: * - @f$(A \wedge q \implies A \wedge \phi)@f$ if @f$Q@f$ is * @f$\forall@f$, and @f$(A \wedge \phi \implies A \wedge q)@f$ if @@ -4345,8 +4362,8 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param locSort The location sort of the heap - * @param dataSort The data sort of the heap + * @param locSort The location sort of the heap. + * @param dataSort The data sort of the heap. */ void declareSepHeap(const Sort& locSort, const Sort& dataSort) const; @@ -4355,7 +4372,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return The term for the heap + * @return The term for the heap. */ Term getValueSepHeap() const; @@ -4364,7 +4381,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return The term for nil + * @return The term for nil. */ Term getValueSepNil() const; @@ -4384,10 +4401,10 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param symbol The name of the pool + * @param symbol The name of the pool. * @param sort The sort of the elements of the pool. - * @param initValue The initial value of the pool - * @return The pool symbol + * @param initValue The initial value of the pool. + * @return The pool symbol. */ Term declarePool(const std::string& symbol, const Sort& sort, @@ -4403,7 +4420,7 @@ class CVC5_EXPORT Solver * (pop ) * \endverbatim * - * @param nscopes the number of levels to pop + * @param nscopes The number of levels to pop. */ void pop(uint32_t nscopes = 1) const; @@ -4423,10 +4440,11 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param conj the conjecture term - * @return a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj, - * or the null term if such a term cannot be found. + * @param conj The conjecture term. + * @return A Term @f$I@f$ such that @f$A \rightarrow I@f$ and + * @f$I \rightarrow B@f$ are valid, where @f$A@f$ is the + * current set of assertions and @f$B@f$ is given in the input by + * `conj`, or the null term if such a term cannot be found. */ Term getInterpolant(const Term& conj) const; @@ -4446,11 +4464,12 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param conj the conjecture term - * @param grammar the grammar for the interpolant I - * @return a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj, - * or the null term if such a term cannot be found. + * @param conj The conjecture term. + * @param grammar The grammar for the interpolant I. + * @return A Term @f$I@f$ such that @f$A \rightarrow I@f$ and + * @f$I \rightarrow B@f$ are valid, where @f$A@f$ is the + * current set of assertions and @f$B@f$ is given in the input by + * `conj`, or the null term if such a term cannot be found. */ Term getInterpolant(const Term& conj, Grammar& grammar) const; @@ -4473,9 +4492,10 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return a Term I such that A->I and I->B are valid, where A is the - * current set of assertions and B is given in the input by conj - * on the last call to getInterpolant. + * @return A Term @f$I@f$ such that @f$A \rightarrow I@f$ and + * @f$I \rightarrow B@f$ are valid, where @f$A@f$ is the + * current set of assertions and @f$B@f$ is given in the input by + * `conj`, or the null term if such a term cannot be found. */ Term getInterpolantNext() const; @@ -4495,8 +4515,8 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param conj the conjecture term - * @return a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, + * @param conj The conjecture term. + * @return A term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where * @f$A@f$ is the current set of assertions and @f$B@f$ is * given in the input by ``conj``, or the null term if such a term @@ -4521,12 +4541,12 @@ class CVC5_EXPORT Solver * @warning This method is experimental and may change in future versions. * * - * @param conj the conjecture term - * @param grammar the grammar for the abduct @f$C@f$ - * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and + * @param conj The conjecture term. + * @param grammar The grammar for the abduct @f$C@f$ + * @return A term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by - * ``conj``, or the null term if such a term cannot be found. + * `conj`, or the null term if such a term cannot be found. */ Term getAbduct(const Term& conj, Grammar& grammar) const; @@ -4548,11 +4568,11 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and + * @return A term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by - * the last call to getAbduct, or the null term if such a term cannot - * be found. + * the last call to getAbduct(), or the null term if such a term + * cannot be found. */ Term getAbductNext() const; @@ -4573,7 +4593,7 @@ class CVC5_EXPORT Solver * * @warning This method is experimental and may change in future versions. * - * @param mode The mode to use for blocking + * @param mode The mode to use for blocking. */ void blockModel(modes::BlockModelsMode mode) const; @@ -4599,8 +4619,8 @@ class CVC5_EXPORT Solver /** * @warning This method is experimental and may change in future versions. * - * @return a string that contains information about all instantiations made by - * the quantifiers module. + * @return A string that contains information about all instantiations made + * by the quantifiers module. */ std::string getInstantiations() const; @@ -4615,7 +4635,7 @@ class CVC5_EXPORT Solver * (push ) * \endverbatim * - * @param nscopes the number of levels to push + * @param nscopes The number of levels to push. */ void push(uint32_t nscopes = 1) const; @@ -4644,8 +4664,8 @@ class CVC5_EXPORT Solver * (set-info ) * \endverbatim * - * @param keyword the info flag - * @param value the value of the info flag + * @param keyword The info flag. + * @param value The value of the info flag. */ void setInfo(const std::string& keyword, const std::string& value) const; @@ -4660,7 +4680,7 @@ class CVC5_EXPORT Solver * (set-logic ) * \endverbatim * - * @param logic the logic to set + * @param logic The logic to set. */ void setLogic(const std::string& logic) const; @@ -4675,8 +4695,8 @@ class CVC5_EXPORT Solver * (set-option :