diff options
Diffstat (limited to 'src/api/cpp/cvc5.h')
| -rw-r--r-- | src/api/cpp/cvc5.h | 34 |
1 files changed, 0 insertions, 34 deletions
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 5e0f0d834..28d5cb1c9 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1469,19 +1469,6 @@ class CVC5_EXPORT Term */ std::vector<Term> getSequenceValue() const; - /** - * @return true if the term is a value from an uninterpreted sort. - */ - bool isUninterpretedValue() const; - /** - bool @return() const; - * Asserts isUninterpretedValue(). - * @return the representation of an uninterpreted value as a pair of its - sort and its - * index. - */ - std::pair<Sort, int32_t> getUninterpretedValue() const; - protected: /** * The associated solver object. @@ -3550,27 +3537,6 @@ class CVC5_EXPORT Solver Term mkRoundingMode(RoundingMode rm) const; /** - * Create uninterpreted constant. - * @param sort Sort of the constant - * @param index Index of the constant - */ - Term mkUninterpretedConst(const Sort& sort, int32_t index) const; - - /** - * Create an abstract value constant. - * The given index needs to be a positive integer in base 10. - * @param index Index of the abstract value - */ - Term mkAbstractValue(const std::string& index) const; - - /** - * Create an abstract value constant. - * The given index needs to be positive. - * @param index Index of the abstract value - */ - Term mkAbstractValue(uint64_t index) const; - - /** * Create a floating-point constant. * @param exp Size of the exponent * @param sig Size of the significand |