diff options
45 files changed, 162 insertions, 804 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 diff --git a/src/api/java/cvc5/Solver.java b/src/api/java/cvc5/Solver.java index b0bee500c..ad3111457 100644 --- a/src/api/java/cvc5/Solver.java +++ b/src/api/java/cvc5/Solver.java @@ -1118,45 +1118,6 @@ public class Solver implements IPointer 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 * @param sig Size of the significand diff --git a/src/api/java/cvc5/Term.java b/src/api/java/cvc5/Term.java index e2c719098..7dcf7663a 100644 --- a/src/api/java/cvc5/Term.java +++ b/src/api/java/cvc5/Term.java @@ -620,32 +620,6 @@ public class Term extends AbstractPointer implements Comparable<Term>, 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<Sort, Integer> getUninterpretedValue() - { - Pair<Long, Integer> pair = getUninterpretedValue(pointer); - Sort sort = new Sort(solver, pair.first); - return new Pair<Sort, Integer>(sort, pair.second); - } - - private native Pair<Long, Integer> getUninterpretedValue(long pointer); - public class ConstIterator implements Iterator<Term> { private int currentIndex; diff --git a/src/api/java/jni/cvc5_Solver.cpp b/src/api/java/jni/cvc5_Solver.cpp index c28ea412f..bcff5ebda 100644 --- a/src/api/java/jni/cvc5_Solver.cpp +++ b/src/api/java/jni/cvc5_Solver.cpp @@ -1277,58 +1277,6 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkRoundingMode(JNIEnv* env, /* * Class: cvc5_Solver - * Method: mkUninterpretedConst - * Signature: (JJI)J - */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkUninterpretedConst( - JNIEnv* env, jobject, jlong pointer, jlong sortPointer, jint index) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast<Solver*>(pointer); - Sort* sort = reinterpret_cast<Sort*>(sortPointer); - Term* retPointer = - new Term(solver->mkUninterpretedConst(*sort, (int32_t)index)); - return reinterpret_cast<jlong>(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: cvc5_Solver - * Method: mkAbstractValue - * Signature: (JLjava/lang/String;)J - */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JLjava_lang_String_2( - JNIEnv* env, jobject, jlong pointer, jstring jIndex) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast<Solver*>(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<jlong>(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: cvc5_Solver - * Method: mkAbstractValue - * Signature: (JJ)J - */ -JNIEXPORT jlong JNICALL Java_cvc5_Solver_mkAbstractValue__JJ(JNIEnv* env, - jobject, - jlong pointer, - jlong index) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Solver* solver = reinterpret_cast<Solver*>(pointer); - Term* retPointer = new Term(solver->mkAbstractValue((uint64_t)index)); - return reinterpret_cast<jlong>(retPointer); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -} - -/* - * Class: cvc5_Solver * Method: mkFloatingPoint * Signature: (JIIJ)J */ @@ -2591,4 +2539,4 @@ JNIEXPORT jlong JNICALL Java_cvc5_Solver_getNullDatatypeDecl(JNIEnv* env, DatatypeDecl* ret = new DatatypeDecl(); return reinterpret_cast<jlong>(ret); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); -}
\ No newline at end of file +} diff --git a/src/api/java/jni/cvc5_Term.cpp b/src/api/java/jni/cvc5_Term.cpp index 325a9c744..8e43d0afb 100644 --- a/src/api/java/jni/cvc5_Term.cpp +++ b/src/api/java/jni/cvc5_Term.cpp @@ -856,60 +856,6 @@ JNIEXPORT jlongArray JNICALL Java_cvc5_Term_getSequenceValue(JNIEnv* env, /* * Class: cvc5_Term - * Method: isUninterpretedValue - * Signature: (J)Z - */ -JNIEXPORT jboolean JNICALL Java_cvc5_Term_isUninterpretedValue(JNIEnv* env, - jobject, - jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Term* current = reinterpret_cast<Term*>(pointer); - return static_cast<jboolean>(current->isUninterpretedValue()); - CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false)); -} - -/* - * Class: cvc5_Term - * Method: getUninterpretedValue - * Signature: (J)Lcvc5/Pair; - */ -JNIEXPORT jobject JNICALL Java_cvc5_Term_getUninterpretedValue(JNIEnv* env, - jobject, - jlong pointer) -{ - CVC5_JAVA_API_TRY_CATCH_BEGIN; - Term* current = reinterpret_cast<Term*>(pointer); - std::pair<Sort, std::int32_t> value = current->getUninterpretedValue(); - - Sort* sort = new Sort(value.first); - jlong sortPointer = reinterpret_cast<jlong>(sort); - - // Long longObject = new Long(pointer) - jclass longClass = env->FindClass("Ljava/lang/Long;"); - jmethodID longConstructor = env->GetMethodID(longClass, "<init>", "(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, "<init>", "(I)V"); - jobject integerObject = env->NewObject( - integerClass, integerConstructor, static_cast<jint>(value.second)); - - // Pair<String, Long> pair = new Pair<String, Long>(jName, longObject) - jclass pairClass = env->FindClass("Lcvc5/Pair;"); - jmethodID pairConstructor = env->GetMethodID( - pairClass, "<init>", "(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: cvc5_Term * Method: iterator * Signature: (J)J */ diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index ef9971c20..99747f8b7 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -237,7 +237,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 mkConst(Sort sort, const string& symbol) except + @@ -430,8 +429,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 2a35363ea..c65c8e606 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -1345,32 +1345,6 @@ cdef class Solver: term.cterm = self.csolver.mkRoundingMode(<c_RoundingMode> 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. @@ -2642,16 +2616,6 @@ cdef class Term: elems.append(term) return elems - def isUninterpretedValue(self): - return self.cterm.isUninterpretedValue() - - def getUninterpretedValue(self): - 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) - def isTupleValue(self): return self.cterm.isTupleValue() diff --git a/src/expr/CMakeLists.txt b/src/expr/CMakeLists.txt index e73960676..90a01109d 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 ) libcvc5_add_sources(GENERATED diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index a9e5854b0..60f076057 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -1105,9 +1105,7 @@ Node NodeManager::mkBag(const TypeNode& t, const TNode n, const TNode m) } Node NodeManager::mkAbstractValue(const TypeNode& type) { - Node n = mkConst(AbstractValue(++d_abstractValueCount)); - n.setAttribute(TypeAttr(), type); - n.setAttribute(TypeCheckedAttr(), true); + Node n = mkConst(AbstractValue(type, ++d_abstractValueCount)); return n; } diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp deleted file mode 100644 index ef354568d..000000000 --- a/src/expr/uninterpreted_constant.cpp +++ /dev/null @@ -1,97 +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 <algorithm> -#include <iostream> -#include <sstream> -#include <string> - -#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<TypeNode>()(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 <iosfwd> -#include <memory> - -#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<TypeNode> 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 9f34b5647..ac4935a99 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -751,18 +751,7 @@ void Parser::pushGetValueScope() std::vector<api::Term> 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.getAbstractValue(), e); } } } diff --git a/src/parser/smt2/smt2.cpp b/src/parser/smt2/smt2.cpp index e1ce29b65..203be81b9 100644 --- a/src/parser/smt2/smt2.cpp +++ b/src/parser/smt2/smt2.cpp @@ -325,16 +325,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()) @@ -832,13 +822,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 8d8f8febe..07cb01423 100644 --- a/src/parser/smt2/smt2.h +++ b/src/parser/smt2/smt2.h @@ -130,12 +130,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". */ diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp index 1da2a3c7b..0d8b69acd 100644 --- a/src/printer/smt2/smt2_printer.cpp +++ b/src/printer/smt2/smt2_printer.cpp @@ -32,7 +32,6 @@ #include "expr/node_manager_attributes.h" #include "expr/node_visitor.h" #include "expr/sequence.h" -#include "expr/uninterpreted_constant.h" #include "options/bv_options.h" #include "options/language.h" #include "options/printer_options.h" @@ -48,6 +47,7 @@ #include "theory/datatypes/tuple_project_op.h" #include "theory/quantifiers/quantifiers_attributes.h" #include "theory/theory_model.h" +#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/divisible.h" #include "util/floatingpoint.h" @@ -323,11 +323,12 @@ void Smt2Printer::toStream(std::ostream& out, } break; } - - case kind::UNINTERPRETED_CONSTANT: { - const UninterpretedConstant& uc = n.getConst<UninterpretedConstant>(); + + case kind::ABSTRACT_VALUE: + { + const AbstractValue& av = n.getConst<AbstractValue>(); std::stringstream ss; - ss << "(as @" << uc << " " << n.getType() << ")"; + ss << "(as " << av << " " << n.getType() << ")"; out << ss.str(); break; } @@ -524,7 +525,7 @@ void Smt2Printer::toStream(std::ostream& out, out << ")"; } } - else + else if (k != kind::ABSTRACT_VALUE) { // use type ascription out << "(as "; diff --git a/src/smt/abstract_values.cpp b/src/smt/abstract_values.cpp index 56cb643db..fd62bf930 100644 --- a/src/smt/abstract_values.cpp +++ b/src/smt/abstract_values.cpp @@ -47,10 +47,7 @@ Node AbstractValues::mkAbstractValue(TNode n) val = d_nm->mkAbstractValue(n.getType()); 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/theory/builtin/kinds b/src/theory/builtin/kinds index d4a8782b5..a3b51bcd5 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -264,24 +264,14 @@ well-founded SORT_TYPE \ "::cvc5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \ "::cvc5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)" -constant UNINTERPRETED_CONSTANT \ - 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)" + "the kind of expressions representing abstract values; payload is an instance of the cvc5::AbstractValue class (used in models)" typerule ABSTRACT_VALUE ::cvc5::theory::builtin::AbstractValueTypeRule +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 f3c595720..7064a3142 100644 --- a/src/theory/builtin/theory_builtin_type_rules.cpp +++ b/src/theory/builtin/theory_builtin_type_rules.cpp @@ -17,18 +17,18 @@ #include "expr/attribute.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" +#include "util/abstract_value.h" #include "util/cardinality.h" namespace cvc5 { namespace theory { namespace builtin { -TypeNode UninterpretedConstantTypeRule::computeType(NodeManager* nodeManager, - TNode n, - bool check) +TypeNode AbstractValueTypeRule::computeType(NodeManager* nodeManager, + TNode n, + bool check) { - return n.getConst<UninterpretedConstant>().getType(); + return n.getConst<AbstractValue>().getType(); } /** diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 54139c433..e966aa5f8 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -91,20 +91,9 @@ class SExprTypeRule { } };/* class SExprTypeRule */ -class UninterpretedConstantTypeRule { - 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); - } + static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check); };/* class AbstractValueTypeRule */ class LambdaTypeRule { diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp index 0ef1d3ec7..7c521346c 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/abstract_value.h" namespace cvc5 { namespace theory { diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h index 980792f94..81ab2bf5c 100644 --- a/src/theory/builtin/type_enumerator.h +++ b/src/theory/builtin/type_enumerator.h @@ -20,8 +20,8 @@ #include "expr/kind.h" #include "expr/type_node.h" -#include "expr/uninterpreted_constant.h" #include "theory/type_enumerator.h" +#include "util/abstract_value.h" #include "util/integer.h" namespace cvc5 { @@ -58,8 +58,7 @@ class UninterpretedSortEnumerator : public TypeEnumeratorBase<UninterpretedSortE if(isFinished()) { throw NoMoreValuesException(getType()); } - return NodeManager::currentNM()->mkConst( - UninterpretedConstant(getType(), d_count)); + return NodeManager::currentNM()->mkConst(AbstractValue(getType(), d_count)); } UninterpretedSortEnumerator& operator++() override diff --git a/src/theory/datatypes/datatypes_rewriter.cpp b/src/theory/datatypes/datatypes_rewriter.cpp index c446504fd..8c9ef2ec1 100644 --- a/src/theory/datatypes/datatypes_rewriter.cpp +++ b/src/theory/datatypes/datatypes_rewriter.cpp @@ -21,11 +21,11 @@ #include "expr/node_algorithm.h" #include "expr/skolem_manager.h" #include "expr/sygus_datatype.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "theory/datatypes/sygus_datatype_utils.h" #include "theory/datatypes/theory_datatypes_utils.h" #include "theory/datatypes/tuple_project_op.h" +#include "util/abstract_value.h" #include "util/rational.h" using namespace cvc5; @@ -729,7 +729,7 @@ Node DatatypesRewriter::collectRef(Node n, else { // a loop - const Integer& i = n.getConst<UninterpretedConstant>().getIndex(); + const Integer& i = n.getConst<AbstractValue>().getIndex(); uint32_t index = i.toUnsignedInt(); if (index >= sk.size()) { @@ -771,7 +771,7 @@ Node DatatypesRewriter::normalizeCodatatypeConstantEqc( { int debruijn = depth - it->second - 1; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + AbstractValue(n.getType(), debruijn)); } std::vector<Node> children; bool childChanged = false; @@ -798,10 +798,9 @@ Node DatatypesRewriter::replaceDebruijn(Node n, TypeNode orig_tn, unsigned depth) { - if (n.getKind() == kind::UNINTERPRETED_CONSTANT && n.getType() == orig_tn) + if (n.getKind() == kind::ABSTRACT_VALUE && n.getType() == orig_tn) { - unsigned index = - n.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); + unsigned index = n.getConst<AbstractValue>().getIndex().toUnsignedInt(); if (index == depth) { return orig; diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c892ffc11..370b9cb9e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -22,7 +22,6 @@ #include "expr/dtype_cons.h" #include "expr/kind.h" #include "expr/skolem_manager.h" -#include "expr/uninterpreted_constant.h" #include "options/datatypes_options.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" @@ -1293,7 +1292,7 @@ Node TheoryDatatypes::getCodatatypesValue( Node n, std::map< Node, Node >& eqc_c if( itv!=vmap.end() ){ int debruijn = depth - 1 - itv->second; return NodeManager::currentNM()->mkConst( - UninterpretedConstant(n.getType(), debruijn)); + AbstractValue(n.getType(), debruijn)); }else if( n.getType().isDatatype() ){ Node nc = eqc_cons[n]; if( !nc.isNull() ){ diff --git a/src/theory/datatypes/type_enumerator.cpp b/src/theory/datatypes/type_enumerator.cpp index 39b48ece9..75489f698 100644 --- a/src/theory/datatypes/type_enumerator.cpp +++ b/src/theory/datatypes/type_enumerator.cpp @@ -109,7 +109,7 @@ Node DatatypesEnumerator::getTermEnum( TypeNode tn, unsigned i ){ if (d_child_enum) { ret = NodeManager::currentNM()->mkConst( - UninterpretedConstant(d_type, d_size_limit)); + AbstractValue(d_type, d_size_limit)); } else { 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 2d6c3de55..c4aaf0f63 100644 --- a/src/theory/evaluator.cpp +++ b/src/theory/evaluator.cpp @@ -42,10 +42,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 ABSTRACT: new (&d_av) AbstractValue(other.d_av); break; case INVALID: break; } } @@ -70,10 +67,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 ABSTRACT: new (&d_av) AbstractValue(other.d_av); break; case INVALID: break; } } @@ -99,9 +93,9 @@ EvalResult::~EvalResult() d_str.~String(); break; } - case UCONST: + case ABSTRACT: { - d_uc.~UninterpretedConstant(); + d_av.~AbstractValue(); break; } default: break; @@ -117,7 +111,7 @@ Node EvalResult::toNode() const case EvalResult::BITVECTOR: return nm->mkConst(d_bv); case EvalResult::RATIONAL: return nm->mkConst(d_rat); case EvalResult::STRING: return nm->mkConst(d_str); - case EvalResult::UCONST: return nm->mkConst(d_uc); + case EvalResult::ABSTRACT: return nm->mkConst(d_av); default: { Trace("evaluator") << "Missing conversion from " << d_tag << " to node" @@ -413,11 +407,10 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(r); break; } - case kind::UNINTERPRETED_CONSTANT: + case kind::ABSTRACT_VALUE: { - const UninterpretedConstant& uc = - currNodeVal.getConst<UninterpretedConstant>(); - results[currNode] = EvalResult(uc); + const AbstractValue& av = currNodeVal.getConst<AbstractValue>(); + results[currNode] = EvalResult(av); break; } case kind::PLUS: @@ -830,9 +823,9 @@ EvalResult Evaluator::evalInternal( results[currNode] = EvalResult(lhs.d_str == rhs.d_str); break; } - case EvalResult::UCONST: + case EvalResult::ABSTRACT: { - 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..33d495aa7 100644 --- a/src/theory/evaluator.h +++ b/src/theory/evaluator.h @@ -26,7 +26,7 @@ #include "base/output.h" #include "expr/node.h" -#include "expr/uninterpreted_constant.h" +#include "util/abstract_value.h" #include "util/bitvector.h" #include "util/rational.h" #include "util/string.h" @@ -47,7 +47,7 @@ struct EvalResult BITVECTOR, RATIONAL, STRING, - UCONST, + ABSTRACT, INVALID } d_tag; @@ -58,7 +58,7 @@ struct EvalResult BitVector d_bv; Rational d_rat; String d_str; - UninterpretedConstant d_uc; + AbstractValue 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 AbstractValue& av) : d_tag(ABSTRACT), d_av(av) {} EvalResult& operator=(const EvalResult& other); diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index c9fced3be..a5925631e 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -230,9 +230,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() == ABSTRACT_VALUE && n.getType().isSort()) + { ret = true; - }else{ + } + else + { for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( containsUninterpretedConstant( n[i] ) ){ ret = true; diff --git a/src/theory/theory_model_builder.cpp b/src/theory/theory_model_builder.cpp index 33dbe9ffa..de5e21abd 100644 --- a/src/theory/theory_model_builder.cpp +++ b/src/theory/theory_model_builder.cpp @@ -16,7 +16,6 @@ #include "expr/dtype.h" #include "expr/dtype_cons.h" -#include "expr/uninterpreted_constant.h" #include "options/quantifiers_options.h" #include "options/smt_options.h" #include "options/strings_options.h" @@ -25,6 +24,7 @@ #include "smt/env.h" #include "theory/rewriter.h" #include "theory/uf/theory_uf_model.h" +#include "util/abstract_value.h" using namespace std; using namespace cvc5::kind; @@ -224,7 +224,7 @@ bool TheoryEngineModelBuilder::isExcludedCdtValue( { Trace("model-builder-debug") << " ...matches with " << eqc << " -> " << eqc_m << std::endl; - if (eqc_m.getKind() == kind::UNINTERPRETED_CONSTANT) + if (eqc_m.getKind() == kind::ABSTRACT_VALUE) { Trace("model-builder-debug") << "*** " << val << " is excluded datatype for " << eqc @@ -318,8 +318,7 @@ bool TheoryEngineModelBuilder::isExcludedUSortValue( << tn << std::endl; unsigned card = eqc_usort_count[tn]; Trace("model-builder-debug") << " Cardinality is " << card << std::endl; - unsigned index = - v.getConst<UninterpretedConstant>().getIndex().toUnsignedInt(); + unsigned index = v.getConst<AbstractValue>().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 cd974d3e4..24ea16c9f 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -287,17 +287,16 @@ void TheoryUF::preRegisterTerm(TNode node) case kind::COMBINED_CARDINALITY_CONSTRAINT: //do nothing break; - case kind::UNINTERPRETED_CONSTANT: + case kind::ABSTRACT_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. + // Abstract 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 abstract values. However, they may be exported via + // models to API users. It is thus possible that these abstract 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/abstract_value.cpp b/src/util/abstract_value.cpp index 556ce6eb0..1441b58fb 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -20,21 +20,49 @@ #include <string> #include "base/check.h" +#include "expr/type_node.h" using namespace std; namespace cvc5 { std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { - return out << "@" << val.getIndex(); + return out << "@a" << val.getIndex(); } -AbstractValue::AbstractValue(Integer index) : d_index(index) +AbstractValue::AbstractValue(const TypeNode& type, const Integer& index) + : d_type(new TypeNode(type)), d_index(index) { - PrettyCheckArgument(index >= 1, + PrettyCheckArgument(index >= 0, index, - "index >= 1 required for abstract value, not `%s'", + "index >= 0 required for abstract value, not `%s'", index.toString().c_str()); } +AbstractValue::AbstractValue(const AbstractValue& val) + : d_type(new TypeNode(*val.d_type)), d_index(val.d_index) +{ +} + +AbstractValue::~AbstractValue() {} + +const TypeNode& AbstractValue::getType() const { return *d_type; } + +bool AbstractValue::operator==(const AbstractValue& val) const +{ + return getType() == val.getType() && d_index == val.d_index; +} + +bool AbstractValue::operator<(const AbstractValue& val) const +{ + return getType() < val.getType() + || (getType() == val.getType() && d_index < val.d_index); +} + +bool AbstractValue::operator<=(const AbstractValue& val) const +{ + return getType() <= val.getType() + || (getType() == val.getType() && d_index <= val.d_index); +} + } // namespace cvc5 diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index 2ebc01061..ee3234d69 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -18,40 +18,42 @@ #pragma once #include <iosfwd> +#include <memory> #include "util/integer.h" namespace cvc5 { +class TypeNode; + class AbstractValue { - const Integer d_index; - public: - AbstractValue(Integer index); + AbstractValue(const TypeNode& type, const Integer& index); + AbstractValue(const AbstractValue& val); + ~AbstractValue(); const Integer& getIndex() const { return d_index; } - bool operator==(const AbstractValue& val) const - { - return d_index == val.d_index; - } + const TypeNode& getType() const; + + bool operator==(const AbstractValue& val) const; 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; + bool operator<=(const AbstractValue& val) const; bool operator>(const AbstractValue& val) const { return !(*this <= val); } bool operator>=(const AbstractValue& val) const { return !(*this < val); } + + private: + /** The type of the abstract value */ + std::unique_ptr<TypeNode> d_type; + /** The index of the abstract value */ + const Integer d_index; }; /* class AbstractValue */ std::ostream& operator<<(std::ostream& out, const AbstractValue& val); /** - * Hash function for the BitVector constants. + * Hash function for abstract values. */ struct AbstractValueHashFunction { diff --git a/test/python/unit/api/test_solver.py b/test/python/unit/api/test_solver.py index db49f8bea..7627bc6e5 100644 --- a/test/python/unit/api/test_solver.py +++ b/test/python/unit/api/test_solver.py @@ -381,35 +381,6 @@ def test_mk_rounding_mode(solver): solver.mkRoundingMode(pycvc5.RoundTowardZero) -def test_mk_uninterpreted_const(solver): - solver.mkUninterpretedConst(solver.getBooleanSort(), 1) - with pytest.raises(RuntimeError): - solver.mkUninterpretedConst(pycvc5.Sort(solver), 1) - slv = pycvc5.Solver() - with pytest.raises(RuntimeError): - slv.mkUninterpretedConst(solver.getBooleanSort(), 1) - - -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/python/unit/api/test_term.py b/test/python/unit/api/test_term.py index e65299676..270c826b1 100644 --- a/test/python/unit/api/test_term.py +++ b/test/python/unit/api/test_term.py @@ -942,16 +942,17 @@ def test_get_const_array_base(solver): 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() + solver.setOption("produce-models", "true") + uSort = solver.mkUninterpretedSort("u") + x = solver.mkConst(uSort, "x") + y = solver.mkConst(uSort, "y") + solver.assertFormula(solver.mkTerm(kinds.Equal, x, y)) + assert solver.checkSat().isSat() + vx = solver.getValue(x) + vy = solver.getValue(y) + assert vx.isAbstractValue() + assert vy.isAbstractValue() + assert vx.getAbstractValue() == vy.getAbstractValue() def test_get_tuple(solver): @@ -1027,18 +1028,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/regress/regress0/bug421.smt2 b/test/regress/regress0/bug421.smt2 index fd7b4a7cc..9f0ad5b9c 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 @a1 (Array Int Int))) (b (as @a2 (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..c9e77fa31 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 @a1 (Array Int Int))) (b (as @a2 (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/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java index d153b8a91..9694510d9 100644 --- a/test/unit/api/java/cvc5/SolverTest.java +++ b/test/unit/api/java/cvc5/SolverTest.java @@ -386,35 +386,6 @@ class SolverTest assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO)); } - @Test void mkUninterpretedConst() throws CVC5ApiException - { - assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - assertThrows( - CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1)); - Solver slv = new Solver(); - assertThrows( - CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - } - - @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); @@ -2342,4 +2313,4 @@ class SolverTest + "\"Z\")))", projection.toString()); } -}
\ No newline at end of file +} diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java index 98f668006..a4b51ab1d 100644 --- a/test/unit/api/java/cvc5/TermTest.java +++ b/test/unit/api/java/cvc5/TermTest.java @@ -834,16 +834,17 @@ class TermTest @Test void getAbstractValue() 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.isAbstractValue(), vy.isAbstractValue()); + assertDoesNotThrow(() -> vx.getAbstractValue()); + assertDoesNotThrow(() -> vy.getAbstractValue()); } @Test void getTuple() @@ -948,19 +949,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<Sort, Integer>(s, 3), t1.getUninterpretedValue()); - assertEquals(new Pair<Sort, Integer>(s, 5), t2.getUninterpretedValue()); - } - @Test void substitute() { Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x"); diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp index 19113ae13..5669f9803 100644 --- a/test/unit/api/solver_black.cpp +++ b/test/unit/api/solver_black.cpp @@ -376,33 +376,6 @@ TEST_F(TestApiBlackSolver, mkRoundingMode) ASSERT_NO_THROW(d_solver.mkRoundingMode(RoundingMode::ROUND_TOWARD_ZERO)); } -TEST_F(TestApiBlackSolver, mkUninterpretedConst) -{ - ASSERT_NO_THROW(d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1)); - ASSERT_THROW(d_solver.mkUninterpretedConst(Sort(), 1), CVC5ApiException); - Solver slv; - ASSERT_THROW(slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1), - CVC5ApiException); -} - -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/term_black.cpp b/test/unit/api/term_black.cpp index 7cfbe2527..3c4493ac6 100644 --- a/test/unit/api/term_black.cpp +++ b/test/unit/api/term_black.cpp @@ -885,16 +885,17 @@ TEST_F(TestApiBlackTerm, getBitVector) TEST_F(TestApiBlackTerm, getAbstractValue) { - 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.isAbstractValue()); + ASSERT_TRUE(vy.isAbstractValue()); + ASSERT_EQ(vx.getAbstractValue(), vy.getAbstractValue()); } TEST_F(TestApiBlackTerm, getTuple) @@ -994,19 +995,6 @@ TEST_F(TestApiBlackTerm, getSequence) ASSERT_EQ(std::vector<Term>({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/theory/type_enumerator_white.cpp b/test/unit/theory/type_enumerator_white.cpp index bb7ef871c..f62fd7971 100644 --- a/test/unit/theory/type_enumerator_white.cpp +++ b/test/unit/theory/type_enumerator_white.cpp @@ -22,10 +22,10 @@ #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/abstract_value.h" #include "util/bitvector.h" #include "util/rational.h" @@ -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(AbstractValue(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(AbstractValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort2, i))); + ASSERT_EQ(*++te, d_nodeManager->mkConst(AbstractValue(sort, i))); + ASSERT_NE(*te, d_nodeManager->mkConst(AbstractValue(sort, i + 2))); } } diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp index 1272926db..d7bc4b412 100644 --- a/test/unit/util/array_store_all_white.cpp +++ b/test/unit/util/array_store_all_white.cpp @@ -14,8 +14,8 @@ */ #include "expr/array_store_all.h" -#include "expr/uninterpreted_constant.h" #include "test_smt.h" +#include "util/abstract_value.h" #include "util/rational.h" namespace cvc5 { @@ -32,7 +32,7 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) d_nodeManager->realType()), d_nodeManager->mkConst(Rational(9, 2))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkSort("U"), usort), - d_nodeManager->mkConst(UninterpretedConstant(usort, 0))); + d_nodeManager->mkConst(AbstractValue(usort, 0))); ArrayStoreAll(d_nodeManager->mkArrayType(d_nodeManager->mkBitVectorType(8), d_nodeManager->realType()), d_nodeManager->mkConst(Rational(0))); @@ -44,8 +44,8 @@ TEST_F(TestUtilWhiteArrayStoreAll, store_all) TEST_F(TestUtilWhiteArrayStoreAll, type_errors) { ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), - d_nodeManager->mkConst(UninterpretedConstant( - d_nodeManager->mkSort("U"), 0))), + d_nodeManager->mkConst( + AbstractValue(d_nodeManager->mkSort("U"), 0))), IllegalArgumentException); ASSERT_THROW(ArrayStoreAll(d_nodeManager->integerType(), d_nodeManager->mkConst(Rational(9, 2))), |