/**
* Get the symbol of this Sort.
*
- * Asserts hasSymbol(). The symbol of this sort is the string that was
+ * @note Asserts hasSymbol().
+ *
+ * The symbol of this sort is the string that was
* provided when constructing it via
* 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.
*/
std::string getSymbol() const;
/**
* Get the symbol of this Term.
*
- * Asserts hasSymbol(). The symbol of the term is the string that was
+ * @note 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.
*/
std::string getSymbol() const;
*/
bool isInt32Value() const;
/**
- * Asserts isInt32Value().
- * @return The integer term as a int32_t.
+ * Get the `int32_t` representation of this integer value.
+ * @note Asserts isInt32Value().
+ * @return This integer value as a `int32_t`.
*/
int32_t getInt32Value() const;
/**
*/
bool isUInt32Value() const;
/**
- * Asserts isUInt32Value().
- * @return The integer term as a uint32_t.
+ * Get the `uint32_t` representation of this integer value.
+ * @note Asserts isUInt32Value().
+ * @return This integer value as a `uint32_t`.
*/
uint32_t getUInt32Value() const;
/**
*/
bool isInt64Value() const;
/**
- * Asserts isInt64Value().
- * @return The integer term as a int64_t.
+ * Get the `int64_t` representation of this integer value.
+ * @note Asserts isInt64Value().
+ * @return This integer value as a `int64_t`.
*/
int64_t getInt64Value() const;
/**
*/
bool isUInt64Value() const;
/**
- * Asserts isUInt64Value().
- * @return The integer term as a uint64_t.
+ * Get the `uint64_t` representation of this integer value.
+ * @note Asserts isUInt64Value().
+ * @return This integer value as a `uint64_t`.
*/
uint64_t getUInt64Value() const;
/**
*/
bool isIntegerValue() const;
/**
- * Asserts isIntegerValue().
+ * @note Asserts isIntegerValue().
* @return The integer term in (decimal) string representation.
*/
std::string getIntegerValue() const;
*/
bool isStringValue() const;
/**
- * Asserts isStringValue().
+ * @note 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.
*/
bool isReal32Value() const;
/**
- * Asserts isReal32Value().
+ * @note Asserts isReal32Value().
* @return The representation of a rational value as a pair of its numerator
* and denominator.
*/
*/
bool isReal64Value() const;
/**
- * Asserts isReal64Value().
+ * @note Asserts isReal64Value().
* @return The representation of a rational value as a pair of its numerator
* and denominator.
*/
*/
bool isRealValue() const;
/**
- * Asserts isRealValue().
+ * @note Asserts isRealValue().
* @return The representation of a rational value as a (rational) string.
*/
std::string getRealValue() const;
*/
bool isConstArray() const;
/**
- * Asserts isConstArray().
+ * @note Asserts isConstArray().
* @return The base (element stored at all indices) of a constant array.
*/
Term getConstArrayBase() const;
*/
bool isBooleanValue() const;
/**
- * Asserts isBooleanValue().
+ * @note Asserts isBooleanValue().
* @return The representation of a Boolean value as a native Boolean value.
*/
bool getBooleanValue() const;
*/
bool isUninterpretedSortValue() const;
/**
- * Asserts isUninterpretedSortValue().
+ * @note Asserts isUninterpretedSortValue().
* @return The representation of an uninterpreted sort value as a string.
*/
std::string getUninterpretedSortValue() const;
*/
bool isTupleValue() const;
/**
- * Asserts isTupleValue().
+ * @note Asserts isTupleValue().
* @return The representation of a tuple value as a vector of terms.
*/
std::vector<Term> getTupleValue() const;
*/
bool isRoundingModeValue() const;
/**
- * Asserts isRoundingModeValue().
+ * @note Asserts isRoundingModeValue().
* @return The floating-point rounding mode value held by the term.
*/
RoundingMode getRoundingModeValue() const;
*/
bool isFloatingPointValue() const;
/**
- * Asserts isFloatingPointValue().
+ * @note 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.
*/
*/
bool isSetValue() const;
/**
- * Asserts isSetValue().
+ * @note Asserts isSetValue().
* @return The representation of a set value as a set of terms.
*/
std::set<Term> getSetValue() const;
*/
bool isSequenceValue() const;
/**
- * Asserts isSequenceValue().
+ * @note Asserts isSequenceValue().
* @return The representation of a sequence value as a vector of terms.
*/
std::vector<Term> getSequenceValue() const;
*/
bool isCardinalityConstraint() const;
/**
- * Asserts isCardinalityConstraint().
+ * @note Asserts isCardinalityConstraint().
* @return The sort the cardinality constraint is for and its upper bound.
*/
std::pair<Sort, uint32_t> getCardinalityConstraint() const;
ModeInfo>;
/** The option value information */
OptionInfoVariant valueInfo;
- /** Obtain the current value as a `bool`. Asserts that `valueInfo` holds a
- * `bool`.
+ /**
+ * Get the current value as a `bool`.
+ * @note Asserts that `valueInfo` holds a `bool`.
+ * @return The current value as a `bool`.
*/
bool boolValue() const;
- /** Obtain the current value as a `std::string`. Asserts that `valueInfo`
- * holds a `std::string`. */
+ /**
+ * Get the current value as a `std::string`.
+ * @note Asserts that `valueInfo` holds a `std::string`.
+ * @return The current value as a `std::string`.
+ */
std::string stringValue() const;
- /** Obtain the current value as an `int64_t`. Asserts that `valueInfo` holds
- * an `int64_t`.
+ /**
+ * Get the current value as an `int64_t`.
+ * @note Asserts that `valueInfo` holds an `int64_t`.
+ * @return The current value as a `int64_t`.
*/
int64_t intValue() const;
- /** Obtain the current value as a `uint64_t`. Asserts that `valueInfo` holds a
- * `uint64_t`.
+ /**
+ * Get the current value as a `uint64_t`.
+ * @note Asserts that `valueInfo` holds a `uint64_t`.
+ * @return The current value as a `uint64_t`.
*/
uint64_t uintValue() const;
- /** Obtain the current value as a `double`. Asserts that `valueInfo` holds a
- * `double`. */
+ /**
+ * Obtain the current value as a `double`.
+ * @note Asserts that `valueInfo` holds a `double`.
+ * @return The current value as a `double`.
+ */
double doubleValue() const;
};
/**
* Retrieve the statistic with the given name.
- * Asserts that a statistic with the given name actually exists and throws
- * a `CVC5ApiRecoverableException` if it does not.
- * @param name Name of the statistic.
+ * @note Asserts that a statistic with the given name actually exists and
+ * throws a CVC5ApiRecoverableException if it does not.
+ * @param name The name of the statistic.
* @return The statistic with the given name.
*/
const Stat& get(const std::string& name);
def getSymbol(self):
"""
- Asserts :py:meth:`hasSymbol()`.
+ .. note:: Asserts :py:meth:`hasSymbol()`.
:return: The raw symbol of the sort.
"""
def getSymbol(self):
"""
- Asserts :py:meth:`hasSymbol()`.
+ ..note:: Asserts :py:meth:`hasSymbol()`.
:return: The raw symbol of the term.
"""
def getConstArrayBase(self):
"""
- Asserts :py:meth:`isConstArray()`.
+ .. note:: Asserts :py:meth:`isConstArray()`.
:return: The base (element stored at all indicies) of this constant
array.
def getBooleanValue(self):
"""
- Asserts :py:meth:`isBooleanValue()`
+ .. note:: Asserts :py:meth:`isBooleanValue()`
:return: The representation of a Boolean value as a native Boolean
value.
def getStringValue(self):
"""
- Asserts :py:meth:`isStringValue()`.
+ .. note:: Asserts :py:meth:`isStringValue()`.
.. note::
This method is not to be confused with :py:meth:`__str__()`
def getIntegerValue(self):
"""
- Asserts :py:meth:`isIntegerValue()`.
+ .. note:: Asserts :py:meth:`isIntegerValue()`.
:return: The integer term as a native python integer.
"""
def getFloatingPointValue(self):
"""
- Asserts :py:meth:`isFloatingPointValue()`.
+ .. note:: Asserts :py:meth:`isFloatingPointValue()`.
:return: The representation of a floating-point value as a tuple of
the exponent width, the significand width and a bit-vector
def getSetValue(self):
"""
- Asserts :py:meth:`isSetValue()`.
+ .. note:: Asserts :py:meth:`isSetValue()`.
:return: The representation of a set value as a set of terms.
"""
def getSequenceValue(self):
"""
- Asserts :py:meth:`isSequenceValue()`.
+ .. note:: Asserts :py:meth:`isSequenceValue()`.
.. note::
def getUninterpretedSortValue(self):
"""
- Asserts :py:meth:`isUninterpretedSortValue()`.
+ .. note:: Asserts :py:meth:`isUninterpretedSortValue()`.
:return: The representation of an uninterpreted value as a pair of
its sort and its index.
def getRoundingModeValue(self):
"""
- Asserts :py:meth:`isRoundingModeValue()`.
+ .. note:: Asserts :py:meth:`isRoundingModeValue()`.
:return: The floating-point rounding mode value held by the term.
"""
return RoundingMode(<int> self.cterm.getRoundingModeValue())
def getTupleValue(self):
"""
- Asserts :py:meth:`isTupleValue()`.
+ .. note:: Asserts :py:meth:`isTupleValue()`.
:return: The representation of a tuple value as a vector of terms.
"""
def getRealValue(self):
"""
- Asserts :py:meth:`isRealValue()`.
+ .. note:: Asserts :py:meth:`isRealValue()`.
:return: The representation of a rational value as a python Fraction.
"""
def getBitVectorValue(self, base = 2):
"""
- Asserts :py:meth:`isBitVectorValue()`.
+ .. note:: Asserts :py:meth:`isBitVectorValue()`.
Supported bases are 2 (bit string), 10 (decimal string) or 16
(hexdecimal string).
projects / cvc5.git / commitdiff