summaryrefslogtreecommitdiff
path: root/src/api/cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/api/cpp')
-rw-r--r--src/api/cpp/cvc5.cpp72
-rw-r--r--src/api/cpp/cvc5.h34
-rw-r--r--src/api/cpp/cvc5_kind.h13
3 files changed, 4 insertions, 115 deletions
diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 778f700c0..3efcf491f 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -54,7 +54,6 @@
#include "expr/node_manager.h"
#include "expr/sequence.h"
#include "expr/type_node.h"
-#include "expr/uninterpreted_constant.h"
#include "options/base_options.h"
#include "options/main_options.h"
#include "options/option_exception.h"
@@ -108,7 +107,6 @@ const static std::unordered_map<Kind, cvc5::Kind> s_kinds{
{UNDEFINED_KIND, cvc5::Kind::UNDEFINED_KIND},
{NULL_EXPR, cvc5::Kind::NULL_EXPR},
/* Builtin ------------------------------------------------------------- */
- {UNINTERPRETED_CONSTANT, cvc5::Kind::UNINTERPRETED_CONSTANT},
{ABSTRACT_VALUE, cvc5::Kind::ABSTRACT_VALUE},
{EQUAL, cvc5::Kind::EQUAL},
{DISTINCT, cvc5::Kind::DISTINCT},
@@ -387,7 +385,6 @@ const static std::unordered_map<cvc5::Kind, Kind, cvc5::kind::KindHashFunction>
{cvc5::Kind::UNDEFINED_KIND, UNDEFINED_KIND},
{cvc5::Kind::NULL_EXPR, NULL_EXPR},
/* Builtin --------------------------------------------------------- */
- {cvc5::Kind::UNINTERPRETED_CONSTANT, UNINTERPRETED_CONSTANT},
{cvc5::Kind::ABSTRACT_VALUE, ABSTRACT_VALUE},
{cvc5::Kind::EQUAL, EQUAL},
{cvc5::Kind::DISTINCT, DISTINCT},
@@ -3103,7 +3100,9 @@ std::string Term::getAbstractValue() const
<< "Term to be an abstract value when calling "
"getAbstractValue()";
//////// all checks before this line
- return d_node->getConst<AbstractValue>().getIndex().toString();
+ std::stringstream ss;
+ ss << d_node->getConst<AbstractValue>();
+ return ss.str();
////////
CVC5_API_TRY_CATCH_END;
}
@@ -3309,31 +3308,6 @@ std::vector<Term> Term::getSequenceValue() const
CVC5_API_TRY_CATCH_END;
}
-bool Term::isUninterpretedValue() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- //////// all checks before this line
- return d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT;
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-std::pair<Sort, std::int32_t> Term::getUninterpretedValue() const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_CHECK_NOT_NULL;
- CVC5_API_ARG_CHECK_EXPECTED(
- d_node->getKind() == cvc5::Kind::UNINTERPRETED_CONSTANT, *d_node)
- << "Term to be an uninterpreted value when calling "
- "getUninterpretedValue()";
- //////// all checks before this line
- const auto& uc = d_node->getConst<UninterpretedConstant>();
- return std::make_pair(Sort(d_solver, uc.getType()),
- uc.getIndex().toUnsignedInt());
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
std::ostream& operator<<(std::ostream& out, const Term& t)
{
out << t.toString();
@@ -5983,46 +5957,6 @@ Term Solver::mkRoundingMode(RoundingMode rm) const
CVC5_API_TRY_CATCH_END;
}
-Term Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_SOLVER_CHECK_SORT(sort);
- //////// all checks before this line
- return mkValHelper<cvc5::UninterpretedConstant>(
- cvc5::UninterpretedConstant(*sort.d_type, index));
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(const std::string& index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_ARG_CHECK_EXPECTED(!index.empty(), index) << "a non-empty string";
-
- cvc5::Integer idx(index, 10);
- CVC5_API_ARG_CHECK_EXPECTED(idx > 0, index)
- << "a string representing an integer > 0";
- //////// all checks before this line
- return Term(this, getNodeManager()->mkConst(cvc5::AbstractValue(idx)));
- // do not call getType(), for abstract values, type can not be computed
- // until it is substituted away
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
-Term Solver::mkAbstractValue(uint64_t index) const
-{
- CVC5_API_TRY_CATCH_BEGIN;
- CVC5_API_ARG_CHECK_EXPECTED(index > 0, index) << "an integer > 0";
- //////// all checks before this line
- return Term(this,
- getNodeManager()->mkConst(cvc5::AbstractValue(Integer(index))));
- // do not call getType(), for abstract values, type can not be computed
- // until it is substituted away
- ////////
- CVC5_API_TRY_CATCH_END;
-}
-
Term Solver::mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) const
{
CVC5_API_TRY_CATCH_BEGIN;
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
diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h
index 0ff05022f..69daa1720 100644
--- a/src/api/cpp/cvc5_kind.h
+++ b/src/api/cpp/cvc5_kind.h
@@ -64,18 +64,7 @@ enum CVC5_EXPORT Kind : int32_t
/* Builtin --------------------------------------------------------------- */
/**
- * Uninterpreted constant.
- *
- * Parameters:
- * - 1: Sort of the constant
- * - 2: Index of the constant
- *
- * Create with:
- * - `Solver::mkUninterpretedConst(const Sort& sort, int32_t index) const`
- */
- UNINTERPRETED_CONSTANT,
- /**
- * Abstract value (other than uninterpreted sort constants).
+ * Abstract value.
*
* Parameters:
* - 1: Index of the abstract value
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback