From: Andres Noetzli Date: Thu, 13 Jan 2022 01:42:26 +0000 (-0800) Subject: Unify abstract values and uninterpreted constants (#7424) X-Git-Tag: cvc5-1.0.0~551 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f5ee6bb4a4477d40d7f6577ea0c5bac17420935;p=cvc5.git Unify abstract values and uninterpreted constants (#7424) This commit unifies abstract values and "uninterpreted constants" into a single kind. Note that "uninterpreted constants" is a bit of a misnomer in the context of the new API, since they do not correspond to the equivalent of a declare-const command, but instead are values for symbols of an uninterpreted sort (and thus special cases of abstract values). Instead of treating "uninterpreted constants" as a separate kind, this commit extends abstract values to hold a type (instead of marking their type via attribute in NodeManager::mkAbstractValue()) and uses the type of the abstract values to determine whether they are a value for a constant of uninterpreted sort or not. Unifying these representations simplifies code and brings the terminology more in line with the SMT-LIB standard. This commit also updates the APIs to remove support for creating abstract values and "uninterpreted constants". Users should never create those. They can only be returned as a value for a term after a satisfiability check. Finally, the commit removes code in the parser for parsing abstract values and updates the code for getting values involving abstract values. Since the parser does not allow the declaration/definition of abstract values, and determining whether a symbol is an abstract value was broken (not all symbols starting with an @ are abstract values), the code was effectively dead. Getting values involving "uninterpreted constants" now no longer requires parsing the string of the values, but instead, we can use existing API functionality. --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1c795431d..e3d70bde5 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -56,7 +56,6 @@ #include "expr/node_manager_attributes.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" @@ -71,7 +70,6 @@ #include "theory/datatypes/tuple_project_op.h" #include "theory/logic_info.h" #include "theory/theory_model.h" -#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/divisible.h" #include "util/floatingpoint.h" @@ -84,6 +82,7 @@ #include "util/statistics_stats.h" #include "util/statistics_value.h" #include "util/string.h" +#include "util/uninterpreted_sort_value.h" #include "util/utility.h" namespace cvc5 { @@ -110,8 +109,7 @@ const static std::unordered_map 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}, + {UNINTERPRETED_SORT_VALUE, cvc5::Kind::UNINTERPRETED_SORT_VALUE}, {EQUAL, cvc5::Kind::EQUAL}, {DISTINCT, cvc5::Kind::DISTINCT}, {CONSTANT, cvc5::Kind::VARIABLE}, @@ -392,8 +390,7 @@ const static std::unordered_map {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::UNINTERPRETED_SORT_VALUE, UNINTERPRETED_SORT_VALUE}, {cvc5::Kind::EQUAL, EQUAL}, {cvc5::Kind::DISTINCT, DISTINCT}, {cvc5::Kind::VARIABLE, CONSTANT}, @@ -3149,25 +3146,27 @@ std::string Term::getBitVectorValue(std::uint32_t base) const CVC5_API_TRY_CATCH_END; } -bool Term::isAbstractValue() const +bool Term::isUninterpretedSortValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; //////// all checks before this line - return d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE; + return d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE; //////// CVC5_API_TRY_CATCH_END; } -std::string Term::getAbstractValue() const +std::string Term::getUninterpretedSortValue() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_ARG_CHECK_EXPECTED(d_node->getKind() == cvc5::Kind::ABSTRACT_VALUE, - *d_node) + CVC5_API_ARG_CHECK_EXPECTED( + d_node->getKind() == cvc5::Kind::UNINTERPRETED_SORT_VALUE, *d_node) << "Term to be an abstract value when calling " - "getAbstractValue()"; + "getUninterpretedSortValue()"; //////// all checks before this line - return d_node->getConst().getIndex().toString(); + std::stringstream ss; + ss << d_node->getConst(); + return ss.str(); //////// CVC5_API_TRY_CATCH_END; } @@ -3373,31 +3372,6 @@ std::vector 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 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(); - 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(); @@ -6113,46 +6087,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(*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 6c29e36f2..ad0054606 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -1466,12 +1466,12 @@ class CVC5_EXPORT Term /** * @return true if the term is an abstract value. */ - bool isAbstractValue() const; + bool isUninterpretedSortValue() const; /** - * Asserts isAbstractValue(). - * @return the representation of an abstract value as a string. + * Asserts isUninterpretedSortValue(). + * @return the representation of an uninterpreted sort value as a string. */ - std::string getAbstractValue() const; + std::string getUninterpretedSortValue() const; /** * @return true if the term is a tuple value. @@ -1554,19 +1554,6 @@ class CVC5_EXPORT Term */ std::vector 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 getUninterpretedValue() const; - protected: /** * The associated solver object. @@ -3678,27 +3665,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 diff --git a/src/api/cpp/cvc5_kind.h b/src/api/cpp/cvc5_kind.h index 9c885cb7b..3bd896814 100644 --- a/src/api/cpp/cvc5_kind.h +++ b/src/api/cpp/cvc5_kind.h @@ -64,27 +64,16 @@ enum 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 * * Create with: - * - `Solver::mkAbstractValue(const std::string& index) const` - * - `Solver::mkAbstractValue(uint64_t index) const` + * - `Solver::mkUninterpretedSortValue(const std::string& index) const` + * - `Solver::mkUninterpretedSortValue(uint64_t index) const` */ - ABSTRACT_VALUE, + UNINTERPRETED_SORT_VALUE, #if 0 /* Built-in operator */ BUILTIN, diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java index 5e2ac0972..06b72dae4 100644 --- a/src/api/java/io/github/cvc5/api/Solver.java +++ b/src/api/java/io/github/cvc5/api/Solver.java @@ -1193,45 +1193,6 @@ public class Solver implements IPointer, AutoCloseable private native long mkRoundingMode(long pointer, int rm); - /** - * Create uninterpreted constant. - * @param sort Sort of the constant - * @param index Index of the constant - */ - public Term mkUninterpretedConst(Sort sort, int index) throws CVC5ApiException - { - Utils.validateUnsigned(index, "index"); - long termPointer = mkUninterpretedConst(pointer, sort.getPointer(), index); - return new Term(this, termPointer); - } - - private native long mkUninterpretedConst(long pointer, long sortPointer, int index); - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - public Term mkAbstractValue(String index) - { - long termPointer = mkAbstractValue(pointer, index); - return new Term(this, termPointer); - } - - private native long mkAbstractValue(long pointer, String index); - - /** - * Create an abstract value constant. - * @param index Index of the abstract value - */ - public Term mkAbstractValue(long index) throws CVC5ApiException - { - Utils.validateUnsigned(index, "index"); - long termPointer = mkAbstractValue(pointer, index); - return new Term(this, termPointer); - } - - private native long mkAbstractValue(long pointer, long index); - /** * Create a floating-point constant. * @param exp Size of the exponent diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java index f6897d59b..be792548e 100644 --- a/src/api/java/io/github/cvc5/api/Term.java +++ b/src/api/java/io/github/cvc5/api/Term.java @@ -492,25 +492,25 @@ public class Term extends AbstractPointer implements Comparable, Iterable< private native String getBitVectorValue(long pointer, int base); /** - * @return true if the term is an abstract value. + * @return true if the term is an uninterpreted sort value. */ - public boolean isAbstractValue() + public boolean isUninterpretedSortValue() { - return isAbstractValue(pointer); + return isUninterpretedSortValue(pointer); } - private native boolean isAbstractValue(long pointer); + private native boolean isUninterpretedSortValue(long pointer); /** - * Asserts isAbstractValue(). - * @return the representation of an abstract value as a string. + * Asserts isUninterpretedSortValue(). + * @return the representation of an uninterpreted sort value as a string. */ - public String getAbstractValue() + public String getUninterpretedSortValue() { - return getAbstractValue(pointer); + return getUninterpretedSortValue(pointer); } - private native String getAbstractValue(long pointer); + private native String getUninterpretedSortValue(long pointer); /** * @return true if the term is a tuple value. @@ -650,32 +650,6 @@ public class Term extends AbstractPointer implements Comparable, Iterable< private native long[] getSequenceValue(long pointer); - /** - * @return true if the term is a value from an uninterpreted sort. - */ - public boolean isUninterpretedValue() - { - return isUninterpretedValue(pointer); - } - - private native boolean isUninterpretedValue(long pointer); - - /** - boolean @return() - * Asserts isUninterpretedValue(). - * @return the representation of an uninterpreted value as a pair of its - sort and its - * index. - */ - public Pair getUninterpretedValue() - { - Pair pair = getUninterpretedValue(pointer); - Sort sort = new Sort(solver, pair.first); - return new Pair(sort, pair.second); - } - - private native Pair getUninterpretedValue(long pointer); - public class ConstIterator implements Iterator { private int currentIndex; diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp index 705803c12..f87ec6f49 100644 --- a/src/api/java/jni/solver.cpp +++ b/src/api/java/jni/solver.cpp @@ -1298,57 +1298,6 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkRoundingMode( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } -/* - * Class: io_github_cvc5_api_Solver - * Method: mkUninterpretedConst - * Signature: (JJI)J - */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkUninterpretedConst( - JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - Sort* sort = reinterpret_cast(sortPointer); - Term* retPointer = - new Term(solver->mkUninterpretedConst(*sort, (int32_t)index)); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: io_github_cvc5_api_Solver - * Method: mkAbstractValue - * Signature: (JLjava/lang/String;)J - */ -JNIEXPORT jlong JNICALL -Java_io_github_cvc5_api_Solver_mkAbstractValue__JLjava_lang_String_2( - JNIEnv* env, jobject, jlong pointer, jstring jIndex) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - const char* s = env->GetStringUTFChars(jIndex, nullptr); - std::string cIndex(s); - Term* retPointer = new Term(solver->mkAbstractValue(cIndex)); - env->ReleaseStringUTFChars(jIndex, s); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: io_github_cvc5_api_Solver - * Method: mkAbstractValue - * Signature: (JJ)J - */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_mkAbstractValue__JJ( - JNIEnv* env, jobject, jlong pointer, jlong index) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast(pointer); - Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index)); - return reinterpret_cast(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - /* * Class: io_github_cvc5_api_Solver * Method: mkFloatingPoint diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp index 1e8669873..c45bb4d6a 100644 --- a/src/api/java/jni/term.cpp +++ b/src/api/java/jni/term.cpp @@ -630,30 +630,35 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getBitVectorValue( } /* + * Class: cvc5_Term * Class: io_github_cvc5_api_Term - * Method: isAbstractValue + * Method: isUninterpretedSortValue * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isAbstractValue( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_api_Term_isUninterpretedSortValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - return static_cast(current->isAbstractValue()); + return static_cast(current->isUninterpretedSortValue()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: io_github_cvc5_api_Term - * Method: getAbstractValue + * Method: getUninterpretedSortValue * Signature: (J)Ljava/lang/String; */ -JNIEXPORT jstring JNICALL Java_io_github_cvc5_api_Term_getAbstractValue( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jstring JNICALL +Java_io_github_cvc5_api_Term_getUninterpretedSortValue(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Term* current = reinterpret_cast(pointer); - std::string ret = current->getAbstractValue(); + std::string ret = current->getUninterpretedSortValue(); return env->NewStringUTF(ret.c_str()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } @@ -872,58 +877,6 @@ JNIEXPORT jlongArray JNICALL Java_io_github_cvc5_api_Term_getSequenceValue( CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); } -/* - * Class: io_github_cvc5_api_Term - * Method: isUninterpretedValue - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_api_Term_isUninterpretedValue( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Term* current = reinterpret_cast(pointer); - return static_cast(current->isUninterpretedValue()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); -} - -/* - * Class: io_github_cvc5_api_Term - * Method: getUninterpretedValue - * Signature: (J)Lio/github/cvc5/api/Pair; - */ -JNIEXPORT jobject JNICALL Java_io_github_cvc5_api_Term_getUninterpretedValue( - JNIEnv* env, jobject, jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Term* current = reinterpret_cast(pointer); - std::pair value = current->getUninterpretedValue(); - - Sort* sort = new Sort(value.first); - jlong sortPointer = reinterpret_cast(sort); - - // Long longObject = new Long(pointer) - jclass longClass = env->FindClass("Ljava/lang/Long;"); - jmethodID longConstructor = env->GetMethodID(longClass, "", "(J)V"); - jobject longObject = env->NewObject(longClass, longConstructor, sortPointer); - - // Integer integerObject = new Integer(pair.second) - jclass integerClass = env->FindClass("Ljava/lang/Integer;"); - jmethodID integerConstructor = - env->GetMethodID(integerClass, "", "(I)V"); - jobject integerObject = env->NewObject( - integerClass, integerConstructor, static_cast(value.second)); - - // Pair pair = new Pair(jName, longObject) - jclass pairClass = env->FindClass("Lio/github/cvc5/api/Pair;"); - jmethodID pairConstructor = env->GetMethodID( - pairClass, "", "(Ljava/lang/Object;Ljava/lang/Object;)V"); - jobject pair = - env->NewObject(pairClass, pairConstructor, longObject, integerObject); - - return pair; - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, nullptr); -} - /* * Class: io_github_cvc5_api_Term * Method: iterator diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index e0e72638a..6518c61a4 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -241,7 +241,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": Term mkPosZero(uint32_t exp, uint32_t sig) except + Term mkNegZero(uint32_t exp, uint32_t sig) except + Term mkRoundingMode(RoundingMode rm) except + - Term mkUninterpretedConst(Sort sort, int32_t index) except + Term mkAbstractValue(const string& index) except + Term mkFloatingPoint(uint32_t exp, uint32_t sig, Term val) except + Term mkCardinalityConstraint(Sort sort, int32_t index) except + @@ -433,8 +432,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": string getRealValue() except + bint isBitVectorValue() except + string getBitVectorValue(uint32_t base) except + - bint isAbstractValue() except + - string getAbstractValue() except + + bint isUninterpretedSortValue() except + + string getUninterpretedSortValue() except + bint isFloatingPointPosZero() except + bint isFloatingPointNegZero() except + bint isFloatingPointPosInf() except + @@ -447,8 +446,6 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api": set[Term] getSetValue() except + bint isSequenceValue() except + vector[Term] getSequenceValue() except + - bint isUninterpretedValue() except + - pair[Sort, int32_t] getUninterpretedValue() except + bint isTupleValue() except + vector[Term] getTupleValue() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 2789e6594..d5aedd0a4 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1389,32 +1389,6 @@ cdef class Solver: term.cterm = self.csolver.mkRoundingMode( rm.crm) return term - def mkUninterpretedConst(self, Sort sort, int index): - """Create uninterpreted constant. - - :param sort: Sort of the constant - :param index: Index of the constant - """ - cdef Term term = Term(self) - term.cterm = self.csolver.mkUninterpretedConst(sort.csort, index) - return term - - def mkAbstractValue(self, index): - """ - Create an abstract value constant. - The given index needs to be positive. - - :param index: Index of the abstract value - """ - cdef Term term = Term(self) - try: - term.cterm = self.csolver.mkAbstractValue(str(index).encode()) - except: - raise ValueError( - "mkAbstractValue expects a str representing a number" - " or an int, but got{}".format(index)) - return term - def mkFloatingPoint(self, int exp, int sig, Term val): """Create a floating-point constant. @@ -3183,18 +3157,6 @@ cdef class Term: """ return int(self.cterm.getIntegerValue().decode()) - def isAbstractValue(self): - """:return: True iff this term is an abstract value.""" - return self.cterm.isAbstractValue() - - def getAbstractValue(self): - """ - Asserts :py:meth:`isAbstractValue()`. - - :return: the representation of an abstract value as a string. - """ - return self.cterm.getAbstractValue().decode() - def isFloatingPointPosZero(self): """:return: True iff the term is the floating-point value for positive zero.""" return self.cterm.isFloatingPointPosZero() @@ -3286,21 +3248,17 @@ cdef class Term: elems.append(term) return elems - def isUninterpretedValue(self): + def isUninterpretedSortValue(self): """:return: True iff this term is a value from an uninterpreted sort.""" - return self.cterm.isUninterpretedValue() + return self.cterm.isUninterpretedSortValue() - def getUninterpretedValue(self): + def getUninterpretedSortValue(self): """ - Asserts :py:meth:`isUninterpretedValue()`. + Asserts :py:meth:`isUninterpretedSortValue()`. :return: the representation of an uninterpreted value as a pair of its sort and its index. """ - cdef pair[c_Sort, int32_t] p = self.cterm.getUninterpretedValue() - cdef Sort sort = Sort(self.solver) - sort.csort = p.first - i = p.second - return (sort, i) + return self.cterm.getUninterpretedSortValue() def isTupleValue(self): """:return: True iff this term is a tuple value.""" diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index b65909403..ab66aa236 100644 --- a/src/expr/CMakeLists.txt +++ b/src/expr/CMakeLists.txt @@ -93,8 +93,6 @@ libcvc5_add_sources( subs.h sygus_datatype.cpp sygus_datatype.h - uninterpreted_constant.cpp - uninterpreted_constant.h variadic_trie.cpp variadic_trie.h ) diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 2345578c2..c62b1af5e 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -32,12 +32,11 @@ #include "expr/type_properties.h" #include "theory/bags/bag_make_op.h" #include "theory/sets/singleton_op.h" -#include "theory/type_enumerator.h" -#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/poly_util.h" #include "util/rational.h" #include "util/resource_manager.h" +#include "util/uninterpreted_sort_value.h" // clang-format off ${metakind_includes} @@ -1125,11 +1124,9 @@ Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) return bag; } -Node NodeManager::mkAbstractValue(const TypeNode& type) +Node NodeManager::mkUninterpretedSortValue(const TypeNode& type) { - Node n = mkConst(AbstractValue(++d_abstractValueCount)); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + Node n = mkConst(UninterpretedSortValue(type, ++d_abstractValueCount)); return n; } diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h index 245fc023e..83cb21cbb 100644 --- a/src/expr/node_manager_template.h +++ b/src/expr/node_manager_template.h @@ -686,8 +686,8 @@ class NodeManager /** Create a instantiation constant with the given type. */ Node mkInstConstant(const TypeNode& type); - /** Make a new abstract value with the given type. */ - Node mkAbstractValue(const TypeNode& type); + /** Make a new uninterpreted sort value with the given type. */ + Node mkUninterpretedSortValue(const TypeNode& type); /** make unique (per Type,Kind) variable. */ Node mkNullaryOperator(const TypeNode& type, Kind k); diff --git a/src/expr/skolem_manager.cpp b/src/expr/skolem_manager.cpp index f08ffc5f4..11617e14f 100644 --- a/src/expr/skolem_manager.cpp +++ b/src/expr/skolem_manager.cpp @@ -43,6 +43,11 @@ struct OriginalFormAttributeId }; typedef expr::Attribute OriginalFormAttribute; +struct AbstractValueId +{ +}; +using AbstractValueAttribute = expr::Attribute; + const char* toString(SkolemFunId id) { switch (id) @@ -290,6 +295,12 @@ ProofGenerator* SkolemManager::getProofGenerator(Node t) const return nullptr; } +bool SkolemManager::isAbstractValue(TNode n) const +{ + AbstractValueAttribute ava; + return n.getAttribute(ava); +} + Node SkolemManager::getWitnessForm(Node k) { Assert(k.getKind() == SKOLEM); @@ -424,6 +435,13 @@ Node SkolemManager::mkSkolemNode(const std::string& prefix, } n.setAttribute(expr::TypeAttr(), type); n.setAttribute(expr::TypeCheckedAttr(), true); + + if ((flags & SKOLEM_ABSTRACT_VALUE) != 0) + { + AbstractValueAttribute ava; + n.setAttribute(ava, true); + } + return n; } diff --git a/src/expr/skolem_manager.h b/src/expr/skolem_manager.h index cca28ccf0..97997cdc9 100644 --- a/src/expr/skolem_manager.h +++ b/src/expr/skolem_manager.h @@ -217,9 +217,14 @@ class SkolemManager */ enum SkolemFlags { - SKOLEM_DEFAULT = 0, /**< default behavior */ - SKOLEM_EXACT_NAME = 1, /**< do not make the name unique by adding the id */ - SKOLEM_BOOL_TERM_VAR = 2 /**< vars requiring kind BOOLEAN_TERM_VARIABLE */ + /** default behavior */ + SKOLEM_DEFAULT = 0, + /** do not make the name unique by adding the id */ + SKOLEM_EXACT_NAME = 1, + /** vars requiring kind BOOLEAN_TERM_VARIABLE */ + SKOLEM_BOOL_TERM_VAR = 2, + /** a skolem that stands for an abstract value (used for printing) */ + SKOLEM_ABSTRACT_VALUE = 4, }; /** * This makes a skolem of same type as bound variable v, (say its type is T), @@ -404,6 +409,10 @@ class SkolemManager * the proof generator that was provided in a call to mkSkolem above. */ ProofGenerator* getProofGenerator(Node q) const; + + /** Returns true if n is a skolem that stands for an abstract value */ + bool isAbstractValue(TNode n) const; + /** * Convert to witness form, which gets the witness form of a skolem k. * Notice this method is *not* recursive, instead, it is a simple attribute @@ -440,6 +449,7 @@ class SkolemManager * by this node manager. */ size_t d_skolemCounter; + /** Get or make skolem attribute for term w, which may be a witness term */ Node mkSkolemInternal(Node w, const std::string& prefix, diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp deleted file mode 100644 index 709ec112f..000000000 --- a/src/expr/uninterpreted_constant.cpp +++ /dev/null @@ -1,101 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Andrew Reynolds, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Representation of constants of uninterpreted sorts. - */ - -#include "expr/uninterpreted_constant.h" - -#include -#include -#include -#include - -#include "base/check.h" -#include "expr/type_node.h" - -using namespace std; - -namespace cvc5 { - -UninterpretedConstant::UninterpretedConstant(const TypeNode& type, - Integer index) - : d_type(new TypeNode(type)), d_index(index) -{ - PrettyCheckArgument(type.isSort(), - type, - "uninterpreted constants can only be created for " - "uninterpreted sorts, not `%s'", - type.toString().c_str()); - PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); -} - -UninterpretedConstant::~UninterpretedConstant() {} - -UninterpretedConstant::UninterpretedConstant(const UninterpretedConstant& other) - : d_type(new TypeNode(other.getType())), d_index(other.getIndex()) -{ -} - -const TypeNode& UninterpretedConstant::getType() const { return *d_type; } -const Integer& UninterpretedConstant::getIndex() const { return d_index; } -bool UninterpretedConstant::operator==(const UninterpretedConstant& uc) const -{ - return getType() == uc.getType() && d_index == uc.d_index; -} -bool UninterpretedConstant::operator!=(const UninterpretedConstant& uc) const -{ - return !(*this == uc); -} - -bool UninterpretedConstant::operator<(const UninterpretedConstant& uc) const -{ - return getType() < uc.getType() - || (getType() == uc.getType() && d_index < uc.d_index); -} -bool UninterpretedConstant::operator<=(const UninterpretedConstant& uc) const -{ - return getType() < uc.getType() - || (getType() == uc.getType() && d_index <= uc.d_index); -} -bool UninterpretedConstant::operator>(const UninterpretedConstant& uc) const -{ - return !(*this <= uc); -} -bool UninterpretedConstant::operator>=(const UninterpretedConstant& uc) const -{ - return !(*this < uc); -} - -std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { - std::stringstream ss; - ss << uc.getType(); - std::string st(ss.str()); - // must remove delimiting quotes from the name of the type - // this prevents us from printing symbols like |@uc_|T|_n| - std::string q("|"); - size_t pos; - while ((pos = st.find(q)) != std::string::npos) - { - st.replace(pos, 1, ""); - } - return out << "uc_" << st.c_str() << "_" << uc.getIndex(); -} - -size_t UninterpretedConstantHashFunction::operator()( - const UninterpretedConstant& uc) const -{ - return std::hash()(uc.getType()) - * IntegerHashFunction()(uc.getIndex()); -} - -} // namespace cvc5 diff --git a/src/expr/uninterpreted_constant.h b/src/expr/uninterpreted_constant.h deleted file mode 100644 index 4a86ba510..000000000 --- a/src/expr/uninterpreted_constant.h +++ /dev/null @@ -1,64 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Andres Noetzli, Morgan Deters, Tim King - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Representation of constants of uninterpreted sorts. - */ - -#include "cvc5_public.h" - -#ifndef CVC5__UNINTERPRETED_CONSTANT_H -#define CVC5__UNINTERPRETED_CONSTANT_H - -#include -#include - -#include "util/integer.h" - -namespace cvc5 { - -class TypeNode; - -class UninterpretedConstant -{ - public: - UninterpretedConstant(const TypeNode& type, Integer index); - ~UninterpretedConstant(); - - UninterpretedConstant(const UninterpretedConstant& other); - - const TypeNode& getType() const; - const Integer& getIndex() const; - bool operator==(const UninterpretedConstant& uc) const; - bool operator!=(const UninterpretedConstant& uc) const; - bool operator<(const UninterpretedConstant& uc) const; - bool operator<=(const UninterpretedConstant& uc) const; - bool operator>(const UninterpretedConstant& uc) const; - bool operator>=(const UninterpretedConstant& uc) const; - - private: - std::unique_ptr d_type; - const Integer d_index; -}; /* class UninterpretedConstant */ - -std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc); - -/** - * Hash function for the BitVector constants. - */ -struct UninterpretedConstantHashFunction -{ - size_t operator()(const UninterpretedConstant& uc) const; -}; /* struct UninterpretedConstantHashFunction */ - -} // namespace cvc5 - -#endif /* CVC5__UNINTERPRETED_CONSTANT_H */ diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index 1481d66fe..580c74f0f 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -750,18 +750,7 @@ void Parser::pushGetValueScope() std::vector elements = d_solver->getModelDomainElements(s); for (const api::Term& e : elements) { - // Uninterpreted constants are abstract values, which by SMT-LIB are - // required to be annotated with their type, e.g. (as @uc_Foo_0 Foo). - // Thus, the element is not printed simply as its name. - std::string en = e.toString(); - size_t index = en.find("(as "); - if (index == 0) - { - index = en.find(" ", 4); - en = en.substr(4, index - 4); - } - Trace("parser") << "Get value scope : " << en << " -> " << e << std::endl; - defineVar(en, e); + defineVar(e.getUninterpretedSortValue(), e); } } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index 9f847b702..634eb3655 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -327,16 +327,6 @@ bool Smt2::logicIsSet() { return d_logicSet; } -api::Term Smt2::getExpressionForNameAndType(const std::string& name, - api::Sort t) -{ - if (isAbstractValue(name)) - { - return mkAbstractValue(name); - } - return Parser::getExpressionForNameAndType(name, t); -} - bool Smt2::getTesterName(api::Term cons, std::string& name) { if ((v2_6() || sygus()) && strictModeEnabled()) @@ -828,13 +818,6 @@ bool Smt2::isAbstractValue(const std::string& name) && name.find_first_not_of("0123456789", 1) == std::string::npos; } -api::Term Smt2::mkAbstractValue(const std::string& name) -{ - Assert(isAbstractValue(name)); - // remove the '@' - return d_solver->mkAbstractValue(name.substr(1)); -} - void Smt2::parseOpApplyTypeAscription(ParseOp& p, api::Sort type) { Debug("parser") << "parseOpApplyTypeAscription : " << p << " " << type diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h index 6df62d787..fd6ea8df8 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -133,12 +133,6 @@ class Smt2 : public Parser */ api::Kind getIndexedOpKind(const std::string& name); - /** - * Returns the expression that name should be interpreted as. - */ - api::Term getExpressionForNameAndType(const std::string& name, - api::Sort t) override; - /** * If we are in a version < 2.6, this updates name to the tester name of cons, * e.g. "is-cons". @@ -296,9 +290,9 @@ class Smt2 : public Parser /** Make abstract value * * Abstract values are used for processing get-value calls. The argument - * name should be such that isAbstractValue(name) is true. + * name should be such that isUninterpretedSortValue(name) is true. */ - api::Term mkAbstractValue(const std::string& name); + api::Term mkUninterpretedSortValue(const std::string& name); /** * Smt2 parser provides its own checkDeclaration, which does the diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 08c0482da..eb1afb5c8 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -33,7 +33,7 @@ #include "expr/node_manager_attributes.h" #include "expr/node_visitor.h" #include "expr/sequence.h" -#include "expr/uninterpreted_constant.h" +#include "expr/skolem_manager.h" #include "options/bv_options.h" #include "options/language.h" #include "options/printer_options.h" @@ -55,6 +55,7 @@ #include "util/regexp.h" #include "util/smt2_quote_string.h" #include "util/string.h" +#include "util/uninterpreted_sort_value.h" using namespace std; @@ -322,11 +323,12 @@ void Smt2Printer::toStream(std::ostream& out, } break; } - - case kind::UNINTERPRETED_CONSTANT: { - const UninterpretedConstant& uc = n.getConst(); + + case kind::UNINTERPRETED_SORT_VALUE: + { + const UninterpretedSortValue& av = n.getConst(); std::stringstream ss; - ss << "(as @" << uc << " " << n.getType() << ")"; + ss << "(as " << av << " " << n.getType() << ")"; out << ss.str(); break; } @@ -522,7 +524,7 @@ void Smt2Printer::toStream(std::ostream& out, out << ")"; } } - else + else if (k != kind::UNINTERPRETED_SORT_VALUE) { // use type ascription out << "(as "; @@ -532,9 +534,17 @@ void Smt2Printer::toStream(std::ostream& out, return; } - // variable - if (n.isVar()) + if (n.getKind() == kind::SKOLEM && nm->getSkolemManager()->isAbstractValue(n)) + { + // abstract value + std::string s; + n.getAttribute(expr::VarNameAttr(), s); + out << "(as @" << cvc5::quoteSymbol(s) << " " << n.getType() << ")"; + return; + } + else if (n.isVar()) { + // variable string s; if (n.getAttribute(expr::VarNameAttr(), s)) { diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index 56cb643db..b5475efad 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -16,6 +16,7 @@ #include "smt/abstract_values.h" #include "expr/ascription_type.h" +#include "expr/skolem_manager.h" #include "options/smt_options.h" namespace cvc5 { @@ -44,13 +45,14 @@ Node AbstractValues::mkAbstractValue(TNode n) Node& val = d_abstractValues[n]; if (val.isNull()) { - val = d_nm->mkAbstractValue(n.getType()); + val = d_nm->getSkolemManager()->mkDummySkolem( + "a", + n.getType(), + "an abstract value", + SkolemManager::SKOLEM_ABSTRACT_VALUE); d_abstractValueMap.addSubstitution(val, n); } - // We are supposed to ascribe types to all abstract values that go out. - Node ascription = d_nm->mkConst(AscriptionType(n.getType())); - Node retval = d_nm->mkNode(kind::APPLY_TYPE_ASCRIPTION, ascription, val); - return retval; + return val; } } // namespace smt diff --git a/src/smt/abstract_values.h b/src/smt/abstract_values.h index 354b8691f..de7ef8587 100644 --- a/src/smt/abstract_values.h +++ b/src/smt/abstract_values.h @@ -15,8 +15,8 @@ #include "cvc5_private.h" -#ifndef CVC5__SMT__ABSTRACT_VALUES_H -#define CVC5__SMT__ABSTRACT_VALUES_H +#ifndef CVC5__SMT__UNINTERPRETED_SORT_VALUES_H +#define CVC5__SMT__UNINTERPRETED_SORT_VALUES_H #include diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index 381573a12..f1a9ce70a 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -265,24 +265,14 @@ well-founded SORT_TYPE \ "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" \ "theory/builtin/theory_builtin_type_rules.h" -constant UNINTERPRETED_CONSTANT \ +constant UNINTERPRETED_SORT_VALUE \ class \ - UninterpretedConstant \ - ::cvc5::UninterpretedConstantHashFunction \ - "expr/uninterpreted_constant.h" \ - "the kind of expressions representing uninterpreted constants; payload is an instance of the cvc5::UninterpretedConstant class (used in models)" -typerule UNINTERPRETED_CONSTANT ::cvc5::theory::builtin::UninterpretedConstantTypeRule -enumerator SORT_TYPE \ - ::cvc5::theory::builtin::UninterpretedSortEnumerator \ - "theory/builtin/type_enumerator.h" - -constant ABSTRACT_VALUE \ - class \ - AbstractValue \ - ::cvc5::AbstractValueHashFunction \ - "util/abstract_value.h" \ - "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the cvc5::AbstractValue class (used in models)" -typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule + UninterpretedSortValue \ + ::cvc5::UninterpretedSortValueHashFunction \ + "util/uninterpreted_sort_value.h" \ + "the kind of expressions representing uninterpreted sort values; payload is an instance of the cvc5::AbstractValue class (used in models)" +typerule UNINTERPRETED_SORT_VALUE ::cvc5::theory::builtin::UninterpretedSortValueTypeRule +enumerator SORT_TYPE ::cvc5::theory::builtin::UninterpretedSortEnumerator "theory/builtin/type_enumerator.h" # A kind representing "inlined" operators defined with OPERATOR # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp index 636952be5..b7207edcb 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,17 +17,17 @@ #include "expr/attribute.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" +#include "util/uninterpreted_sort_value.h" namespace cvc5 { namespace theory { namespace builtin { -TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) +TypeNode UninterpretedSortValueTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) { - return n.getConst().getType(); + return n.getConst().getType(); } /** diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 2117249c2..d31733840 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -90,21 +90,11 @@ class SExprTypeRule { } };/* class SExprTypeRule */ -class UninterpretedConstantTypeRule { +class UninterpretedSortValueTypeRule +{ public: static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); -};/* class UninterpretedConstantTypeRule */ - -class AbstractValueTypeRule { - public: - inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) { - // An UnknownTypeException means that this node has no type. For now, - // only abstract values are like this---and then, only if they are created - // by the user and don't actually correspond to one that the SolverEngine - // gave them previously. - throw UnknownTypeException(n); - } -};/* class AbstractValueTypeRule */ +}; /* class UninterpretedSortValueTypeRule */ class WitnessTypeRule { diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 2e919810b..1798d9f78 100644 --- a/src/theory/builtin/type_enumerator.cpp +++ b/src/theory/builtin/type_enumerator.cpp @@ -16,6 +16,7 @@ #include "theory/builtin/type_enumerator.h" #include "theory/builtin/theory_builtin_rewriter.h" +#include "util/uninterpreted_sort_value.h" namespace cvc5 { namespace theory { @@ -51,7 +52,7 @@ Node UninterpretedSortEnumerator::operator*() throw NoMoreValuesException(getType()); } return NodeManager::currentNM()->mkConst( - UninterpretedConstant(getType(), d_count)); + UninterpretedSortValue(getType(), d_count)); } UninterpretedSortEnumerator& UninterpretedSortEnumerator::operator++() diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 711752e23..e7b42edca 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -20,7 +20,6 @@ #include "expr/kind.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "theory/type_enumerator.h" #include "util/integer.h" diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index 93449b637..44ff5aa18 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -27,6 +27,7 @@ #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/datatypes/tuple_project_op.h" #include "util/rational.h" +#include "util/uninterpreted_sort_value.h" using namespace cvc5; using namespace cvc5::kind; diff --git a/src/theory/datatypes/type_enumerator.h b/src/theory/datatypes/type_enumerator.h index 9ea121be4..759c50db0 100644 --- a/src/theory/datatypes/type_enumerator.h +++ b/src/theory/datatypes/type_enumerator.h @@ -21,7 +21,6 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "theory/type_enumerator.h" diff --git a/src/theory/evaluator.cpp b/src/theory/evaluator.cpp index 9451f9995..3552d0a31 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -44,10 +44,7 @@ EvalResult::EvalResult(const EvalResult& other) new (&d_str) String; d_str = other.d_str; break; - case UCONST: - new (&d_uc) - UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex()); - break; + case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break; case INVALID: break; } } @@ -72,10 +69,7 @@ EvalResult& EvalResult::operator=(const EvalResult& other) new (&d_str) String; d_str = other.d_str; break; - case UCONST: - new (&d_uc) - UninterpretedConstant(other.d_uc.getType(), other.d_uc.getIndex()); - break; + case UVALUE: new (&d_av) UninterpretedSortValue(other.d_av); break; case INVALID: break; } } @@ -101,9 +95,9 @@ EvalResult::~EvalResult() d_str.~String(); break; } - case UCONST: + case UVALUE: { - d_uc.~UninterpretedConstant(); + d_av.~UninterpretedSortValue(); break; } default: break; @@ -119,7 +113,7 @@ Node EvalResult::toNode() const case EvalResult::BITVECTOR: return nm->mkConst(d_bv); case EvalResult::RATIONAL: return nm->mkConst(CONST_RATIONAL, d_rat); case EvalResult::STRING: return nm->mkConst(d_str); - case EvalResult::UCONST: return nm->mkConst(d_uc); + case EvalResult::UVALUE: return nm->mkConst(d_av); default: { Trace("evaluator") << "Missing conversion from " << d_tag << " to node" @@ -415,11 +409,11 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(r); break; } - case kind::UNINTERPRETED_CONSTANT: + case kind::UNINTERPRETED_SORT_VALUE: { - const UninterpretedConstant& uc = - currNodeVal.getConst(); - results[currNode] = EvalResult(uc); + const UninterpretedSortValue& av = + currNodeVal.getConst(); + results[currNode] = EvalResult(av); break; } case kind::PLUS: @@ -862,9 +856,9 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(lhs.d_str == rhs.d_str); break; } - case EvalResult::UCONST: + case EvalResult::UVALUE: { - results[currNode] = EvalResult(lhs.d_uc == rhs.d_uc); + results[currNode] = EvalResult(lhs.d_av == rhs.d_av); break; } diff --git a/src/theory/evaluator.h b/src/theory/evaluator.h index 8ccb4561d..bd10129e2 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -26,10 +26,10 @@ #include "base/output.h" #include "expr/node.h" -#include "expr/uninterpreted_constant.h" #include "util/bitvector.h" #include "util/rational.h" #include "util/string.h" +#include "util/uninterpreted_sort_value.h" namespace cvc5 { namespace theory { @@ -47,7 +47,7 @@ struct EvalResult BITVECTOR, RATIONAL, STRING, - UCONST, + UVALUE, INVALID } d_tag; @@ -58,7 +58,7 @@ struct EvalResult BitVector d_bv; Rational d_rat; String d_str; - UninterpretedConstant d_uc; + UninterpretedSortValue d_av; }; EvalResult(const EvalResult& other); @@ -67,7 +67,7 @@ struct EvalResult EvalResult(const BitVector& bv) : d_tag(BITVECTOR), d_bv(bv) {} EvalResult(const Rational& i) : d_tag(RATIONAL), d_rat(i) {} EvalResult(const String& str) : d_tag(STRING), d_str(str) {} - EvalResult(const UninterpretedConstant& u) : d_tag(UCONST), d_uc(u) {} + EvalResult(const UninterpretedSortValue& av) : d_tag(UVALUE), d_av(av) {} EvalResult& operator=(const EvalResult& other); diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp index a783ce2ca..13f52a12f 100644 --- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp +++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp @@ -439,8 +439,8 @@ void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type, { // generate constant array over the first element of the constituent type Node c = nm->mkGroundTerm(type); - // note that c should never contain an uninterpreted constant - Assert(!expr::hasSubtermKind(UNINTERPRETED_CONSTANT, c)); + // note that c should never contain an uninterpreted sort value + Assert(!expr::hasSubtermKind(UNINTERPRETED_SORT_VALUE, c)); ops.push_back(c); } else if (type.isRoundingMode()) diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 4f386c008..5bd22f986 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -214,9 +214,12 @@ int TermUtil::getTermDepth( Node n ) { bool TermUtil::containsUninterpretedConstant( Node n ) { if (!n.hasAttribute(ContainsUConstAttribute()) ){ bool ret = false; - if( n.getKind()==UNINTERPRETED_CONSTANT ){ + if (n.getKind() == UNINTERPRETED_SORT_VALUE && n.getType().isSort()) + { ret = true; - }else{ + } + else + { for( unsigned i=0; i().getIndex().toUnsignedInt(); + v.getConst().getIndex().toUnsignedInt(); Trace("model-builder-debug") << " Index is " << index << std::endl; return index > 0 && index >= card; } diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index b6d789773..9058a57f3 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -294,17 +294,17 @@ void TheoryUF::preRegisterTerm(TNode node) case kind::COMBINED_CARDINALITY_CONSTRAINT: //do nothing break; - case kind::UNINTERPRETED_CONSTANT: + case kind::UNINTERPRETED_SORT_VALUE: { - // Uninterpreted constants should only appear in models, and should - // never appear in constraints. They are unallowed to ever appear in - // constraints since the cardinality of an uninterpreted sort may have - // an upper bound, e.g. if (forall ((x U) (y U)) (= x y)) holds, then - // @uc_U_2 is a ill-formed term, as its existence cannot be assumed. - // The parser prevents the user from ever constructing uninterpreted - // constants. However, they may be exported via models to API users. - // It is thus possible that these uninterpreted constants are asserted - // back in constraints, hence this check is necessary. + // Uninterpreted sort values should only appear in models, and should never + // appear in constraints. They are unallowed to ever appear in constraints + // since the cardinality of an uninterpreted sort may have an upper bound, + // e.g. if (forall ((x U) (y U)) (= x y)) holds, then @uc_U_2 is a + // ill-formed term, as its existence cannot be assumed. The parser + // prevents the user from ever constructing uninterpreted sort values. + // However, they may be exported via models to API users. It is thus + // possible that these uninterpreted sort values are asserted back in + // constraints, hence this check is necessary. throw LogicException( "An uninterpreted constant was preregistered to the UF theory."); } diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 2ac529565..f711fa824 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -18,8 +18,6 @@ configure_file(integer.h.in integer.h) configure_file(real_algebraic_number.h.in real_algebraic_number.h) libcvc5_add_sources( - abstract_value.cpp - abstract_value.h bin_heap.h bitvector.cpp bitvector.h @@ -76,6 +74,8 @@ libcvc5_add_sources( statistics_value.h string.cpp string.h + uninterpreted_sort_value.cpp + uninterpreted_sort_value.h unsafe_interrupt_exception.h utility.cpp utility.h diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp deleted file mode 100644 index 556ce6eb0..000000000 --- a/src/util/abstract_value.cpp +++ /dev/null @@ -1,40 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Tim King, Morgan Deters - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Representation of abstract values. - */ - -#include "util/abstract_value.h" - -#include -#include -#include - -#include "base/check.h" - -using namespace std; - -namespace cvc5 { - -std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { - return out << "@" << val.getIndex(); -} - -AbstractValue::AbstractValue(Integer index) : d_index(index) -{ - PrettyCheckArgument(index >= 1, - index, - "index >= 1 required for abstract value, not `%s'", - index.toString().c_str()); -} - -} // namespace cvc5 diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h deleted file mode 100644 index 2ebc01061..000000000 --- a/src/util/abstract_value.h +++ /dev/null @@ -1,63 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Morgan Deters, Tim King, Mathias Preiner - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS - * in the top-level source directory and their institutional affiliations. - * All rights reserved. See the file COPYING in the top-level source - * directory for licensing information. - * **************************************************************************** - * - * Representation of abstract values. - */ - -#include "cvc5_public.h" - -#pragma once - -#include - -#include "util/integer.h" - -namespace cvc5 { - -class AbstractValue -{ - const Integer d_index; - - public: - AbstractValue(Integer index); - - const Integer& getIndex() const { return d_index; } - bool operator==(const AbstractValue& val) const - { - return d_index == val.d_index; - } - bool operator!=(const AbstractValue& val) const { return !(*this == val); } - bool operator<(const AbstractValue& val) const - { - return d_index < val.d_index; - } - bool operator<=(const AbstractValue& val) const - { - return d_index <= val.d_index; - } - bool operator>(const AbstractValue& val) const { return !(*this <= val); } - bool operator>=(const AbstractValue& val) const { return !(*this < val); } -}; /* class AbstractValue */ - -std::ostream& operator<<(std::ostream& out, const AbstractValue& val); - -/** - * Hash function for the BitVector constants. - */ -struct AbstractValueHashFunction -{ - inline size_t operator()(const AbstractValue& val) const { - return IntegerHashFunction()(val.getIndex()); - } -}; /* struct AbstractValueHashFunction */ - -} // namespace cvc5 diff --git a/src/util/uninterpreted_sort_value.cpp b/src/util/uninterpreted_sort_value.cpp new file mode 100644 index 000000000..e635a4b77 --- /dev/null +++ b/src/util/uninterpreted_sort_value.cpp @@ -0,0 +1,76 @@ +/****************************************************************************** + * Top contributors (to current version): + * Tim King, Morgan Deters + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representation of abstract values. + */ + +#include "util/uninterpreted_sort_value.h" + +#include +#include +#include + +#include "base/check.h" +#include "expr/type_node.h" + +using namespace std; + +namespace cvc5 { + +std::ostream& operator<<(std::ostream& out, const UninterpretedSortValue& val) +{ + return out << "@a" << val.getIndex(); +} + +UninterpretedSortValue::UninterpretedSortValue(const TypeNode& type, + const Integer& index) + : d_type(new TypeNode(type)), d_index(index) +{ + PrettyCheckArgument(type.isSort(), + type, + "uninterpreted constants can only be created for " + "uninterpreted sorts, not `%s'", + type.toString().c_str()); + PrettyCheckArgument(index >= 0, + index, + "index >= 0 required for abstract value, not `%s'", + index.toString().c_str()); +} + +UninterpretedSortValue::UninterpretedSortValue( + const UninterpretedSortValue& val) + : d_type(new TypeNode(*val.d_type)), d_index(val.d_index) +{ +} + +UninterpretedSortValue::~UninterpretedSortValue() {} + +const TypeNode& UninterpretedSortValue::getType() const { return *d_type; } + +bool UninterpretedSortValue::operator==(const UninterpretedSortValue& val) const +{ + return getType() == val.getType() && d_index == val.d_index; +} + +bool UninterpretedSortValue::operator<(const UninterpretedSortValue& val) const +{ + return getType() < val.getType() + || (getType() == val.getType() && d_index < val.d_index); +} + +bool UninterpretedSortValue::operator<=(const UninterpretedSortValue& val) const +{ + return getType() <= val.getType() + || (getType() == val.getType() && d_index <= val.d_index); +} + +} // namespace cvc5 diff --git a/src/util/uninterpreted_sort_value.h b/src/util/uninterpreted_sort_value.h new file mode 100644 index 000000000..e9fa8a24a --- /dev/null +++ b/src/util/uninterpreted_sort_value.h @@ -0,0 +1,75 @@ +/****************************************************************************** + * Top contributors (to current version): + * Morgan Deters, Tim King, Mathias Preiner + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS + * in the top-level source directory and their institutional affiliations. + * All rights reserved. See the file COPYING in the top-level source + * directory for licensing information. + * **************************************************************************** + * + * Representation of abstract values. + */ + +#include "cvc5_public.h" + +#pragma once + +#include +#include + +#include "util/integer.h" + +namespace cvc5 { + +class TypeNode; + +class UninterpretedSortValue +{ + public: + UninterpretedSortValue(const TypeNode& type, const Integer& index); + UninterpretedSortValue(const UninterpretedSortValue& val); + ~UninterpretedSortValue(); + + const Integer& getIndex() const { return d_index; } + const TypeNode& getType() const; + + bool operator==(const UninterpretedSortValue& val) const; + bool operator!=(const UninterpretedSortValue& val) const + { + return !(*this == val); + } + bool operator<(const UninterpretedSortValue& val) const; + bool operator<=(const UninterpretedSortValue& val) const; + bool operator>(const UninterpretedSortValue& val) const + { + return !(*this <= val); + } + bool operator>=(const UninterpretedSortValue& val) const + { + return !(*this < val); + } + + private: + /** The type of the abstract value */ + std::unique_ptr d_type; + /** The index of the abstract value */ + const Integer d_index; +}; /* class UninterpretedSortValue */ + +std::ostream& operator<<(std::ostream& out, const UninterpretedSortValue& val); + +/** + * Hash function for abstract values. + */ +struct UninterpretedSortValueHashFunction +{ + inline size_t operator()(const UninterpretedSortValue& val) const + { + return IntegerHashFunction()(val.getIndex()); + } +}; /* struct UninterpretedSortValueHashFunction */ + +} // namespace cvc5 diff --git a/test/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2 index fd7b4a7cc..f011638fb 100644 --- a/test/regress/regress0/bug421.smt2 +++ b/test/regress/regress0/bug421.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --incremental --abstract-values ; EXPECT: sat -; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) +; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/bug421b.smt2 b/test/regress/regress0/bug421b.smt2 index aed7f7c05..e8d214fad 100644 --- a/test/regress/regress0/bug421b.smt2 +++ b/test/regress/regress0/bug421b.smt2 @@ -4,7 +4,7 @@ ; ; COMMAND-LINE: --incremental --abstract-values --check-models ; EXPECT: sat -; EXPECT: ((a (as @1 (Array Int Int))) (b (as @2 (Array Int Int)))) +; EXPECT: ((a (as @a_2 (Array Int Int))) (b (as @a_3 (Array Int Int)))) (set-logic QF_AUFLIA) (set-option :produce-models true) (declare-fun a () (Array Int Int)) diff --git a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 index b6825fe27..ab7615809 100644 --- a/test/regress/regress0/parser/issue6908-get-value-uc.smt2 +++ b/test/regress/regress0/parser/issue6908-get-value-uc.smt2 @@ -1,10 +1,10 @@ ; COMMAND-LINE: --produce-models ; EXPECT: sat -; EXPECT: (((f (as @uc_Foo_0 Foo)) 3)) +; EXPECT: (((f (as @a0 Foo)) 3)) (set-logic ALL) (set-option :produce-models true) (declare-sort Foo 0) (declare-fun f (Foo) Int) (assert (exists ((x Foo)) (= (f x) 3))) (check-sat) -(get-value ((f @uc_Foo_0))) +(get-value ((f @a0))) diff --git a/test/unit/api/cpp/solver_black.cpp b/test/unit/api/cpp/solver_black.cpp index ff7c7cb42..19a87f709 100644 --- a/test/unit/api/cpp/solver_black.cpp +++ b/test/unit/api/cpp/solver_black.cpp @@ -454,24 +454,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkAbstractValue) -{ - ASSERT_NO_THROW(d_solver.mkAbstractValue(std::string("1"))); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("0")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("-1")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue(std::string("1.2")), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("1/2"), CVC5ApiException); - ASSERT_THROW(d_solver.mkAbstractValue("asdf"), CVC5ApiException); - - ASSERT_NO_THROW(d_solver.mkAbstractValue((uint32_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((uint64_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int32_t)-1)); - ASSERT_NO_THROW(d_solver.mkAbstractValue((int64_t)-1)); - ASSERT_THROW(d_solver.mkAbstractValue(0), CVC5ApiException); -} - TEST_F(TestApiBlackSolver, mkFloatingPoint) { Term t1 = d_solver.mkBitVector(8); diff --git a/test/unit/api/cpp/term_black.cpp b/test/unit/api/cpp/term_black.cpp index dc0d5fd43..975cd7d79 100644 --- a/test/unit/api/cpp/term_black.cpp +++ b/test/unit/api/cpp/term_black.cpp @@ -903,18 +903,19 @@ TEST_F(TestApiBlackTerm, getBitVector) ASSERT_EQ("f", b7.getBitVectorValue(16)); } -TEST_F(TestApiBlackTerm, getAbstractValue) +TEST_F(TestApiBlackTerm, getUninterpretedSortValue) { - Term v1 = d_solver.mkAbstractValue(1); - Term v2 = d_solver.mkAbstractValue("15"); - Term v3 = d_solver.mkAbstractValue("18446744073709551617"); - - ASSERT_TRUE(v1.isAbstractValue()); - ASSERT_TRUE(v2.isAbstractValue()); - ASSERT_TRUE(v3.isAbstractValue()); - ASSERT_EQ("1", v1.getAbstractValue()); - ASSERT_EQ("15", v2.getAbstractValue()); - ASSERT_EQ("18446744073709551617", v3.getAbstractValue()); + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + ASSERT_TRUE(d_solver.checkSat().isSat()); + Term vx = d_solver.getValue(x); + Term vy = d_solver.getValue(y); + ASSERT_TRUE(vx.isUninterpretedSortValue()); + ASSERT_TRUE(vy.isUninterpretedSortValue()); + ASSERT_EQ(vx.getUninterpretedSortValue(), vy.getUninterpretedSortValue()); } TEST_F(TestApiBlackTerm, getTuple) @@ -1014,19 +1015,6 @@ TEST_F(TestApiBlackTerm, getSequence) ASSERT_EQ(std::vector({i1, i1, i2}), s5.getSequenceValue()); } -TEST_F(TestApiBlackTerm, getUninterpretedConst) -{ - Sort s = d_solver.mkUninterpretedSort("test"); - Term t1 = d_solver.mkUninterpretedConst(s, 3); - Term t2 = d_solver.mkUninterpretedConst(s, 5); - - ASSERT_TRUE(t1.isUninterpretedValue()); - ASSERT_TRUE(t2.isUninterpretedValue()); - - ASSERT_EQ(std::make_pair(s, 3), t1.getUninterpretedValue()); - ASSERT_EQ(std::make_pair(s, 5), t2.getUninterpretedValue()); -} - TEST_F(TestApiBlackTerm, substitute) { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java index 2de49dfb4..c47332092 100644 --- a/test/unit/api/java/SolverTest.java +++ b/test/unit/api/java/SolverTest.java @@ -433,25 +433,6 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO)); } - @Test void mkAbstractValue() throws CVC5ApiException - { - assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2"))); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2")); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf")); - - assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1)); - assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1)); - // java does not have specific types for unsigned integers, therefore the two lines below do not - // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1)); - // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1)); - assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0)); - } - @Test void mkFloatingPoint() throws CVC5ApiException { Term t1 = d_solver.mkBitVector(8); diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java index ad84bb18d..684aa1ec7 100644 --- a/test/unit/api/java/TermTest.java +++ b/test/unit/api/java/TermTest.java @@ -855,18 +855,19 @@ class TermTest assertEquals("f", b7.getBitVectorValue(16)); } - @Test void getAbstractValue() throws CVC5ApiException + @Test void getUninterpretedSortValue() throws CVC5ApiException { - Term v1 = d_solver.mkAbstractValue(1); - Term v2 = d_solver.mkAbstractValue("15"); - Term v3 = d_solver.mkAbstractValue("18446744073709551617"); - - assertTrue(v1.isAbstractValue()); - assertTrue(v2.isAbstractValue()); - assertTrue(v3.isAbstractValue()); - assertEquals("1", v1.getAbstractValue()); - assertEquals("15", v2.getAbstractValue()); - assertEquals("18446744073709551617", v3.getAbstractValue()); + d_solver.setOption("produce-models", "true"); + Sort uSort = d_solver.mkUninterpretedSort("u"); + Term x = d_solver.mkConst(uSort, "x"); + Term y = d_solver.mkConst(uSort, "y"); + d_solver.assertFormula(d_solver.mkTerm(EQUAL, x, y)); + assertTrue(d_solver.checkSat().isSat()); + Term vx = d_solver.getValue(x); + Term vy = d_solver.getValue(y); + assertEquals(vx.isUninterpretedSortValue(), vy.isUninterpretedSortValue()); + assertDoesNotThrow(() -> vx.getUninterpretedSortValue()); + assertDoesNotThrow(() -> vy.getUninterpretedSortValue()); } @Test void getTuple() @@ -971,19 +972,6 @@ class TermTest assertEquals(Arrays.asList(new Term[] {i1, i1, i2}), Arrays.asList(s5.getSequenceValue())); } - @Test void getUninterpretedConst() throws CVC5ApiException - { - Sort s = d_solver.mkUninterpretedSort("test"); - Term t1 = d_solver.mkUninterpretedConst(s, 3); - Term t2 = d_solver.mkUninterpretedConst(s, 5); - - assertTrue(t1.isUninterpretedValue()); - assertTrue(t2.isUninterpretedValue()); - - assertEquals(new Pair(s, 3), t1.getUninterpretedValue()); - assertEquals(new Pair(s, 5), t2.getUninterpretedValue()); - } - @Test void substitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py index b73b691c4..7d3504501 100644 --- a/test/unit/api/python/test_solver.py +++ b/test/unit/api/python/test_solver.py @@ -410,26 +410,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_abstract_value(solver): - solver.mkAbstractValue("1") - with pytest.raises(ValueError): - solver.mkAbstractValue("0") - with pytest.raises(ValueError): - solver.mkAbstractValue("-1") - with pytest.raises(ValueError): - solver.mkAbstractValue("1.2") - with pytest.raises(ValueError): - solver.mkAbstractValue("1/2") - with pytest.raises(ValueError): - solver.mkAbstractValue("asdf") - - solver.mkAbstractValue(1) - with pytest.raises(ValueError): - solver.mkAbstractValue(-1) - with pytest.raises(ValueError): - solver.mkAbstractValue(0) - - def test_mk_floating_point(solver): t1 = solver.mkBitVector(8) t2 = solver.mkBitVector(4) diff --git a/test/unit/api/python/test_term.py b/test/unit/api/python/test_term.py index cc15a3181..b810f35b4 100644 --- a/test/unit/api/python/test_term.py +++ b/test/unit/api/python/test_term.py @@ -958,17 +958,18 @@ def test_get_const_array_base(solver): assert one == constarr.getConstArrayBase() -def test_get_abstract_value(solver): - v1 = solver.mkAbstractValue(1) - v2 = solver.mkAbstractValue("15") - v3 = solver.mkAbstractValue("18446744073709551617") - - assert v1.isAbstractValue() - assert v2.isAbstractValue() - assert v3.isAbstractValue() - assert "1" == v1.getAbstractValue() - assert "15" == v2.getAbstractValue() - assert "18446744073709551617" == v3.getAbstractValue() +def test_get_uninterpreted_sort_value(solver): + solver.setOption("produce-models", "true") + uSort = solver.mkUninterpretedSort("u") + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + solver.assertFormula(solver.mkTerm(Kind.Equal, x, y)) + assert solver.checkSat().isSat() + vx = solver.getValue(x) + vy = solver.getValue(y) + assert vx.isUninterpretedSortValue() + assert vy.isUninterpretedSortValue() + assert vx.getUninterpretedSortValue() == vy.getUninterpretedSortValue() def test_get_tuple(solver): @@ -1045,18 +1046,6 @@ def test_get_sequence(solver): assert [i1, i1, i2] == s5.getSequenceValue() -def test_get_uninterpreted_const(solver): - s = solver.mkUninterpretedSort("test") - t1 = solver.mkUninterpretedConst(s, 3) - t2 = solver.mkUninterpretedConst(s, 5) - - assert t1.isUninterpretedValue() - assert t2.isUninterpretedValue() - - assert (s, 3) == t1.getUninterpretedValue() - assert (s, 5) == t2.getUninterpretedValue() - - def test_get_floating_point(solver): bvval = solver.mkBitVector(16, "0000110000000011", 2) fp = solver.mkFloatingPoint(5, 11, bvval) diff --git a/test/unit/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index ac7472560..a84cad193 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,12 +22,12 @@ #include "expr/dtype.h" #include "expr/kind.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "options/language.h" #include "test_smt.h" #include "theory/type_enumerator.h" #include "util/bitvector.h" #include "util/rational.h" +#include "util/uninterpreted_sort_value.h" namespace cvc5 { @@ -61,13 +61,13 @@ TEST_F(TestTheoryWhiteTypeEnumerator, uf) TypeNode sort = d_nodeManager->mkSort("T"); TypeNode sort2 = d_nodeManager->mkSort("U"); TypeEnumerator te(sort); - ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, 0))); + ASSERT_EQ(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, 0))); for (size_t i = 1; i < 100; ++i) { - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort2, i))); - ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedConstant(sort, i))); - ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedConstant(sort, i + 2))); + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort2, i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(UninterpretedSortValue(sort, i + 2))); } } diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 887a214dd..284d686a9 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,9 +14,9 @@ */ #include "expr/array_store_all.h" -#include "expr/uninterpreted_constant.h" #include "test_smt.h" #include "util/rational.h" +#include "util/uninterpreted_sort_value.h" using namespace cvc5::kind; @@ -34,7 +34,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) d_nodeManager->realType()), d_nodeManager->mkConst(CONST_RATIONAL, Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), - d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); + d_nodeManager->mkConst(UninterpretedSortValue(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), d_nodeManager->mkConst(CONST_RATIONAL, Rational(0))); @@ -46,7 +46,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TEST_F(TestUtilWhiteArrayStoreAll, type_errors) { ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(UninterpretedConstant( + d_nodeManager->mkConst(UninterpretedSortValue( d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); ASSERT_THROW(