From: Aina Niemetz Date: Thu, 31 Mar 2022 20:50:45 +0000 (-0700) Subject: Sort, TypeNode: Rename functions related to datatypes. (#8472) X-Git-Tag: cvc5-1.0.0~85 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=27fbec71eec8ad76ce7217301595961262c319cd;p=cvc5.git Sort, TypeNode: Rename functions related to datatypes. (#8472) --- diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp index 1bb4d8c26..2d10f8e92 100644 --- a/src/api/cpp/cvc5.cpp +++ b/src/api/cpp/cvc5.cpp @@ -1258,38 +1258,38 @@ bool Sort::isDatatype() const CVC5_API_TRY_CATCH_END; } -bool Sort::isConstructor() const +bool Sort::isDatatypeConstructor() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isConstructor(); + return d_type->isDatatypeConstructor(); //////// CVC5_API_TRY_CATCH_END; } -bool Sort::isSelector() const +bool Sort::isDatatypeSelector() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isSelector(); + return d_type->isDatatypeSelector(); //////// CVC5_API_TRY_CATCH_END; } -bool Sort::isTester() const +bool Sort::isDatatypeTester() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isTester(); + return d_type->isDatatypeTester(); //////// CVC5_API_TRY_CATCH_END; } -bool Sort::isUpdater() const +bool Sort::isDatatypeUpdater() const { CVC5_API_TRY_CATCH_BEGIN; //////// all checks before this line - return d_type->isUpdater(); + return d_type->isDatatypeUpdater(); //////// CVC5_API_TRY_CATCH_END; } @@ -1499,81 +1499,88 @@ const internal::TypeNode& Sort::getTypeNode(void) const { return *d_type; } /* Constructor sort ------------------------------------------------------- */ -size_t Sort::getConstructorArity() const +size_t Sort::getDatatypeConstructorArity() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeConstructor()) + << "Not a constructor sort: " << (*this); //////// all checks before this line return d_type->getNumChildren() - 1; //////// CVC5_API_TRY_CATCH_END; } -std::vector Sort::getConstructorDomainSorts() const +std::vector Sort::getDatatypeConstructorDomainSorts() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeConstructor()) + << "Not a constructor sort: " << (*this); //////// all checks before this line return typeNodeVectorToSorts(d_solver, d_type->getArgTypes()); //////// CVC5_API_TRY_CATCH_END; } -Sort Sort::getConstructorCodomainSort() const +Sort Sort::getDatatypeConstructorCodomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isConstructor()) << "Not a constructor sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeConstructor()) + << "Not a constructor sort: " << (*this); //////// all checks before this line - return Sort(d_solver, d_type->getConstructorRangeType()); + return Sort(d_solver, d_type->getDatatypeConstructorRangeType()); //////// CVC5_API_TRY_CATCH_END; } /* Selector sort ------------------------------------------------------- */ -Sort Sort::getSelectorDomainSort() const +Sort Sort::getDatatypeSelectorDomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeSelector()) + << "Not a selector sort: " << (*this); //////// all checks before this line - return Sort(d_solver, d_type->getSelectorDomainType()); + return Sort(d_solver, d_type->getDatatypeSelectorDomainType()); //////// CVC5_API_TRY_CATCH_END; } -Sort Sort::getSelectorCodomainSort() const +Sort Sort::getDatatypeSelectorCodomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isSelector()) << "Not a selector sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeSelector()) + << "Not a selector sort: " << (*this); //////// all checks before this line - return Sort(d_solver, d_type->getSelectorRangeType()); + return Sort(d_solver, d_type->getDatatypeSelectorRangeType()); //////// CVC5_API_TRY_CATCH_END; } /* Tester sort ------------------------------------------------------- */ -Sort Sort::getTesterDomainSort() const +Sort Sort::getDatatypeTesterDomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeTester()) + << "Not a tester sort: " << (*this); //////// all checks before this line - return Sort(d_solver, d_type->getTesterDomainType()); + return Sort(d_solver, d_type->getDatatypeTesterDomainType()); //////// CVC5_API_TRY_CATCH_END; } -Sort Sort::getTesterCodomainSort() const +Sort Sort::getDatatypeTesterCodomainSort() const { CVC5_API_TRY_CATCH_BEGIN; CVC5_API_CHECK_NOT_NULL; - CVC5_API_CHECK(isTester()) << "Not a tester sort: " << (*this); + CVC5_API_CHECK(d_type->isDatatypeTester()) + << "Not a tester sort: " << (*this); //////// all checks before this line return d_solver->getBooleanSort(); //////// diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index 9882ede79..3c8de6c18 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -485,27 +485,27 @@ class CVC5_EXPORT Sort bool isDatatype() const; /** - * Is this a constructor sort? - * @return true if the sort is a constructor sort + * Is this a datatype constructor sort? + * @return true if the sort is a datatype constructor sort */ - bool isConstructor() const; + bool isDatatypeConstructor() const; /** - * Is this a selector sort? - * @return true if the sort is a selector sort + * Is this a datatype selector sort? + * @return true if the sort is a datatype selector sort */ - bool isSelector() const; + bool isDatatypeSelector() const; /** - * Is this a tester sort? - * @return true if the sort is a tester sort + * Is this a datatype tester sort? + * @return true if the sort is a datatype tester sort */ - bool isTester() const; + bool isDatatypeTester() const; /** * Is this a datatype updater sort? * @return true if the sort is a datatype updater sort */ - bool isUpdater() const; + bool isDatatypeUpdater() const; /** * Is this a function sort? * @return true if the sort is a function sort @@ -663,49 +663,50 @@ class CVC5_EXPORT Sort */ std::string toString() const; - /* Constructor sort ------------------------------------------------------- */ + /* Datatype constructor sort ------------------------------------------- */ /** - * @return the arity of a constructor sort + * @return the arity of a datatype constructor sort */ - size_t getConstructorArity() const; + size_t getDatatypeConstructorArity() const; /** - * @return the domain sorts of a constructor sort + * @return the domain sorts of a datatype constructor sort */ - std::vector getConstructorDomainSorts() const; + std::vector getDatatypeConstructorDomainSorts() const; /** * @return the codomain sort of a constructor sort */ - Sort getConstructorCodomainSort() const; + Sort getDatatypeConstructorCodomainSort() const; /* Selector sort ------------------------------------------------------- */ /** - * @return the domain sort of a selector sort + * @return the domain sort of a datatype selector sort */ - Sort getSelectorDomainSort() const; + Sort getDatatypeSelectorDomainSort() const; /** - * @return the codomain sort of a selector sort + * @return the codomain sort of a datatype selector sort */ - Sort getSelectorCodomainSort() const; + Sort getDatatypeSelectorCodomainSort() const; /* Tester sort ------------------------------------------------------- */ /** - * @return the domain sort of a tester sort + * @return the domain sort of a datatype tester sort */ - Sort getTesterDomainSort() const; + Sort getDatatypeTesterDomainSort() const; /** - * @return the codomain sort of a tester sort, which is the Boolean sort + * @return the codomain sort of a datatype tester sort, which is the Boolean + * sort * * @note We mainly need this for the symbol table, which doesn't have * access to the solver object. */ - Sort getTesterCodomainSort() const; + Sort getDatatypeTesterCodomainSort() const; /* Function sort ------------------------------------------------------- */ diff --git a/src/api/java/io/github/cvc5/Sort.java b/src/api/java/io/github/cvc5/Sort.java index d42313751..64fcbb56b 100644 --- a/src/api/java/io/github/cvc5/Sort.java +++ b/src/api/java/io/github/cvc5/Sort.java @@ -202,48 +202,48 @@ public class Sort extends AbstractPointer implements Comparable private native boolean isDatatype(long pointer); /** - * Is this a constructor sort? - * @return true if the sort is a constructor sort + * Is this a datatype constructor sort? + * @return true if the sort is a datatype constructor sort */ - public boolean isConstructor() + public boolean isDatatypeConstructor() { - return isConstructor(pointer); + return isDatatypeConstructor(pointer); } - private native boolean isConstructor(long pointer); + private native boolean isDatatypeConstructor(long pointer); /** - * Is this a selector sort? - * @return true if the sort is a selector sort + * Is this a datatype selector sort? + * @return true if the sort is a datatype selector sort */ - public boolean isSelector() + public boolean isDatatypeSelector() { - return isSelector(pointer); + return isDatatypeSelector(pointer); } - private native boolean isSelector(long pointer); + private native boolean isDatatypeSelector(long pointer); /** - * Is this a tester sort? - * @return true if the sort is a tester sort + * Is this a datatype tester sort? + * @return true if the sort is a datatype tester sort */ - public boolean isTester() + public boolean isDatatypeTester() { - return isTester(pointer); + return isDatatypeTester(pointer); } - private native boolean isTester(long pointer); + private native boolean isDatatypeTester(long pointer); /** * Is this a datatype updater sort? * @return true if the sort is a datatype updater sort */ - public boolean isUpdater() + public boolean isDatatypeUpdater() { - return isUpdater(pointer); + return isDatatypeUpdater(pointer); } - private native boolean isUpdater(long pointer); + private native boolean isDatatypeUpdater(long pointer); /** * Is this a function sort? @@ -516,84 +516,85 @@ public class Sort extends AbstractPointer implements Comparable /* Constructor sort ------------------------------------------------------- */ /** - * @return the arity of a constructor sort + * @return the arity of a datatype constructor sort */ - public int getConstructorArity() + public int getDatatypeConstructorArity() { - return getConstructorArity(pointer); + return getDatatypeConstructorArity(pointer); } - private native int getConstructorArity(long pointer); + private native int getDatatypeConstructorArity(long pointer); /** - * @return the domain sorts of a constructor sort + * @return the domain sorts of a datatype constructor sort */ - public Sort[] getConstructorDomainSorts() + public Sort[] getDatatypeConstructorDomainSorts() { - long[] pointers = getConstructorDomainSorts(pointer); + long[] pointers = getDatatypeConstructorDomainSorts(pointer); return Utils.getSorts(solver, pointers); } - private native long[] getConstructorDomainSorts(long pointer); + private native long[] getDatatypeConstructorDomainSorts(long pointer); /** - * @return the codomain sort of a constructor sort + * @return the codomain sort of a datatype constructor sort */ - public Sort getConstructorCodomainSort() + public Sort getDatatypeConstructorCodomainSort() { - long sortPointer = getConstructorCodomainSort(pointer); + long sortPointer = getDatatypeConstructorCodomainSort(pointer); return new Sort(solver, sortPointer); } - private native long getConstructorCodomainSort(long pointer); + private native long getDatatypeConstructorCodomainSort(long pointer); /* Selector sort ------------------------------------------------------- */ /** - * @return the domain sort of a selector sort + * @return the domain sort of a datatype selector sort */ - public Sort getSelectorDomainSort() + public Sort getDatatypeSelectorDomainSort() { - long sortPointer = getSelectorDomainSort(pointer); + long sortPointer = getDatatypeSelectorDomainSort(pointer); return new Sort(solver, sortPointer); } - private native long getSelectorDomainSort(long pointer); + private native long getDatatypeSelectorDomainSort(long pointer); /** - * @return the codomain sort of a selector sort + * @return the codomain sort of a datatype selector sort */ - public Sort getSelectorCodomainSort() + public Sort getDatatypeSelectorCodomainSort() { - long sortPointer = getSelectorCodomainSort(pointer); + long sortPointer = getDatatypeSelectorCodomainSort(pointer); return new Sort(solver, sortPointer); } - private native long getSelectorCodomainSort(long pointer); + private native long getDatatypeSelectorCodomainSort(long pointer); /* Tester sort ------------------------------------------------------- */ /** - * @return the domain sort of a tester sort + * @return the domain sort of a datatype tester sort */ - public Sort getTesterDomainSort() + public Sort getDatatypeTesterDomainSort() { - long sortPointer = getTesterDomainSort(pointer); + long sortPointer = getDatatypeTesterDomainSort(pointer); return new Sort(solver, sortPointer); } - private native long getTesterDomainSort(long pointer); + private native long getDatatypeTesterDomainSort(long pointer); /** - * @return the codomain sort of a tester sort, which is the Boolean sort + * @return the codomain sort of a datatype tester sort, which is the Boolean + * sort */ - public Sort getTesterCodomainSort() + public Sort getDatatypeTesterCodomainSort() { - long sortPointer = getTesterCodomainSort(pointer); + long sortPointer = getDatatypeTesterCodomainSort(pointer); return new Sort(solver, sortPointer); } - private native long getTesterCodomainSort(long pointer); + private native long getDatatypeTesterCodomainSort(long pointer); /* Function sort ------------------------------------------------------- */ diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp index f6a8c0c2a..af8ae2b9e 100644 --- a/src/api/java/jni/sort.cpp +++ b/src/api/java/jni/sort.cpp @@ -251,59 +251,57 @@ Java_io_github_cvc5_Sort_isDatatype(JNIEnv* env, jobject, jlong pointer) /* * Class: io_github_cvc5_Sort - * Method: isConstructor + * Method: isDatatypeConstructor * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_Sort_isConstructor(JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Sort_isDatatypeConstructor( + JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->isConstructor()); + return static_cast(current->isDatatypeConstructor()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: io_github_cvc5_Sort - * Method: isSelector + * Method: isDatatypeSelector * Signature: (J)Z */ JNIEXPORT jboolean JNICALL -Java_io_github_cvc5_Sort_isSelector(JNIEnv* env, jobject, jlong pointer) +Java_io_github_cvc5_Sort_isDatatypeSelector(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->isSelector()); + return static_cast(current->isDatatypeSelector()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: io_github_cvc5_Sort - * Method: isTester + * Method: isDatatypeTester * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Sort_isTester(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_Sort_isDatatypeTester(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->isTester()); + return static_cast(current->isDatatypeTester()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } /* * Class: io_github_cvc5_Sort - * Method: isUpdater + * Method: isDatatypeUpdater * Signature: (J)Z */ -JNIEXPORT jboolean JNICALL Java_io_github_cvc5_Sort_isUpdater(JNIEnv* env, - jobject, - jlong pointer) +JNIEXPORT jboolean JNICALL +Java_io_github_cvc5_Sort_isDatatypeUpdater(JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->isUpdater()); + return static_cast(current->isDatatypeUpdater()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast(false)); } @@ -642,31 +640,31 @@ JNIEXPORT jstring JNICALL Java_io_github_cvc5_Sort_toString(JNIEnv* env, /* * Class: io_github_cvc5_Sort - * Method: getConstructorArity + * Method: getDatatypeConstructorArity * Signature: (J)I */ -JNIEXPORT jint JNICALL Java_io_github_cvc5_Sort_getConstructorArity( +JNIEXPORT jint JNICALL Java_io_github_cvc5_Sort_getDatatypeConstructorArity( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - return static_cast(current->getConstructorArity()); + return static_cast(current->getDatatypeConstructorArity()); CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_Sort - * Method: getConstructorDomainSorts + * Method: getDatatypeConstructorDomainSorts * Signature: (J)[J */ JNIEXPORT jlongArray JNICALL -Java_io_github_cvc5_Sort_getConstructorDomainSorts(JNIEnv* env, - jobject, - jlong pointer) +Java_io_github_cvc5_Sort_getDatatypeConstructorDomainSorts(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - std::vector sorts = current->getConstructorDomainSorts(); + std::vector sorts = current->getDatatypeConstructorDomainSorts(); std::vector sortPointers(sorts.size()); for (size_t i = 0; i < sorts.size(); i++) { @@ -680,75 +678,79 @@ Java_io_github_cvc5_Sort_getConstructorDomainSorts(JNIEnv* env, /* * Class: io_github_cvc5_Sort - * Method: getConstructorCodomainSort + * Method: getDatatypeConstructorCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getConstructorCodomainSort( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_Sort_getDatatypeConstructorCodomainSort(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - Sort* retPointer = new Sort(current->getConstructorCodomainSort()); + Sort* retPointer = new Sort(current->getDatatypeConstructorCodomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_Sort - * Method: getSelectorDomainSort + * Method: getDatatypeSelectorDomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getSelectorDomainSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getDatatypeSelectorDomainSort( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - Sort* retPointer = new Sort(current->getSelectorDomainSort()); + Sort* retPointer = new Sort(current->getDatatypeSelectorDomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_Sort - * Method: getSelectorCodomainSort + * Method: getDatatypeSelectorCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getSelectorCodomainSort( - JNIEnv* env, jobject, jlong pointer) +JNIEXPORT jlong JNICALL +Java_io_github_cvc5_Sort_getDatatypeSelectorCodomainSort(JNIEnv* env, + jobject, + jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - Sort* retPointer = new Sort(current->getSelectorCodomainSort()); + Sort* retPointer = new Sort(current->getDatatypeSelectorCodomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_Sort - * Method: getTesterDomainSort + * Method: getDatatypeTesterDomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getTesterDomainSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getDatatypeTesterDomainSort( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - Sort* retPointer = new Sort(current->getTesterDomainSort()); + Sort* retPointer = new Sort(current->getDatatypeTesterDomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } /* * Class: io_github_cvc5_Sort - * Method: getTesterCodomainSort + * Method: getDatatypeTesterCodomainSort * Signature: (J)J */ -JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getTesterCodomainSort( +JNIEXPORT jlong JNICALL Java_io_github_cvc5_Sort_getDatatypeTesterCodomainSort( JNIEnv* env, jobject, jlong pointer) { CVC5_JAVA_API_TRY_CATCH_BEGIN; Sort* current = reinterpret_cast(pointer); - Sort* retPointer = new Sort(current->getTesterCodomainSort()); + Sort* retPointer = new Sort(current->getDatatypeTesterCodomainSort()); return (jlong)retPointer; CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0); } diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd index 40a7b613f..7c40ce3af 100644 --- a/src/api/python/cvc5.pxd +++ b/src/api/python/cvc5.pxd @@ -383,10 +383,10 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": bint isBitVector() except + bint isFloatingPoint() except + bint isDatatype() except + - bint isConstructor() except + - bint isSelector() except + - bint isTester() except + - bint isUpdater() except + + bint isDatatypeConstructor() except + + bint isDatatypeSelector() except + + bint isDatatypeTester() except + + bint isDatatypeUpdater() except + bint isFunction() except + bint isPredicate() except + bint isTuple() except + @@ -403,13 +403,13 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5": Sort instantiate(const vector[Sort]& params) except + vector[Sort] getInstantiatedParameters() except + Sort substitute(const vector[Sort] & es, const vector[Sort] & reps) except + - size_t getConstructorArity() except + - vector[Sort] getConstructorDomainSorts() except + - Sort getConstructorCodomainSort() except + - Sort getSelectorDomainSort() except + - Sort getSelectorCodomainSort() except + - Sort getTesterDomainSort() except + - Sort getTesterCodomainSort() except + + size_t getDatatypeConstructorArity() except + + vector[Sort] getDatatypeConstructorDomainSorts() except + + Sort getDatatypeConstructorCodomainSort() except + + Sort getDatatypeSelectorDomainSort() except + + Sort getDatatypeSelectorCodomainSort() except + + Sort getDatatypeTesterDomainSort() except + + Sort getDatatypeTesterCodomainSort() except + size_t getFunctionArity() except + vector[Sort] getFunctionDomainSorts() except + Sort getFunctionCodomainSort() except + diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 46d2a284a..ce4c99439 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -2786,37 +2786,37 @@ cdef class Sort: """ return self.csort.isDatatype() - def isConstructor(self): + def isDatatypeConstructor(self): """ - Is this a constructor sort? + Is this a datatype constructor sort? - :return: True if the sort is a constructor sort. + :return: True if the sort is a datatype constructor sort. """ - return self.csort.isConstructor() + return self.csort.isDatatypeConstructor() - def isSelector(self): + def isDatatypeSelector(self): """ - Is this a selector sort? + Is this a datatype selector sort? - :return: True if the sort is a selector sort. + :return: True if the sort is a datatype selector sort. """ - return self.csort.isSelector() + return self.csort.isDatatypeSelector() - def isTester(self): + def isDatatypeTester(self): """ Is this a tester sort? :return: True if the sort is a selector sort. """ - return self.csort.isTester() + return self.csort.isDatatypeTester() - def isUpdater(self): + def isDatatypeUpdater(self): """ Is this a datatype updater sort? :return: True if the sort is a datatype updater sort. """ - return self.csort.isUpdater() + return self.csort.isDatatypeUpdater() def isFunction(self): """ @@ -3020,61 +3020,62 @@ cdef class Sort: return sort - def getConstructorArity(self): + def getDatatypeConstructorArity(self): """ - :return: the arity of a constructor sort. + :return: the arity of a datatype constructor sort. """ - return self.csort.getConstructorArity() + return self.csort.getDatatypeConstructorArity() - def getConstructorDomainSorts(self): + def getDatatypeConstructorDomainSorts(self): """ - :return: the domain sorts of a constructor sort + :return: the domain sorts of a datatype constructor sort """ domain_sorts = [] - for s in self.csort.getConstructorDomainSorts(): + for s in self.csort.getDatatypeConstructorDomainSorts(): sort = Sort(self.solver) sort.csort = s domain_sorts.append(sort) return domain_sorts - def getConstructorCodomainSort(self): + def getDatatypeConstructorCodomainSort(self): """ - :return: the codomain sort of a constructor sort + :return: the codomain sort of a datatype constructor sort """ cdef Sort sort = Sort(self.solver) - sort.csort = self.csort.getConstructorCodomainSort() + sort.csort = self.csort.getDatatypeConstructorCodomainSort() return sort - def getSelectorDomainSort(self): + def getDatatypeSelectorDomainSort(self): """ - :return: the domain sort of a selector sort + :return: the domain sort of a datatype selector sort """ cdef Sort sort = Sort(self.solver) - sort.csort = self.csort.getSelectorDomainSort() + sort.csort = self.csort.getDatatypeSelectorDomainSort() return sort - def getSelectorCodomainSort(self): + def getDatatypeSelectorCodomainSort(self): """ - :return: the codomain sort of a selector sort + :return: the codomain sort of a datatype selector sort """ cdef Sort sort = Sort(self.solver) - sort.csort = self.csort.getSelectorCodomainSort() + sort.csort = self.csort.getDatatypeSelectorCodomainSort() return sort - def getTesterDomainSort(self): + def getDatatypeTesterDomainSort(self): """ - :return: the domain sort of a tester sort + :return: the domain sort of a datatype tester sort """ cdef Sort sort = Sort(self.solver) - sort.csort = self.csort.getTesterDomainSort() + sort.csort = self.csort.getDatatypeTesterDomainSort() return sort - def getTesterCodomainSort(self): + def getDatatypeTesterCodomainSort(self): """ - :return: the codomain sort of a tester sort, which is the Boolean sort + :return: the codomain sort of a datatype tester sort, which is the + Boolean sort """ cdef Sort sort = Sort(self.solver) - sort.csort = self.csort.getTesterCodomainSort() + sort.csort = self.csort.getDatatypeTesterCodomainSort() return sort def getFunctionArity(self): diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp index fa332f2d4..f2329ed2e 100644 --- a/src/expr/dtype.cpp +++ b/src/expr/dtype.cpp @@ -110,8 +110,10 @@ const DType& DType::datatypeOf(Node item) size_t DType::indexOf(Node item) { - Assert(item.getType().isConstructor() || item.getType().isTester() - || item.getType().isSelector() || item.getType().isUpdater()); + Assert(item.getType().isDatatypeConstructor() + || item.getType().isDatatypeTester() + || item.getType().isDatatypeSelector() + || item.getType().isDatatypeUpdater()); return indexOfInternal(item); } @@ -127,7 +129,8 @@ size_t DType::indexOfInternal(Node item) size_t DType::cindexOf(Node item) { - Assert(item.getType().isSelector() || item.getType().isUpdater()); + Assert(item.getType().isDatatypeSelector() + || item.getType().isDatatypeUpdater()); return cindexOfInternal(item); } size_t DType::cindexOfInternal(Node item) diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp index b19deea0e..287dc0f2a 100644 --- a/src/expr/dtype_cons.cpp +++ b/src/expr/dtype_cons.cpp @@ -237,7 +237,7 @@ const DTypeSelector& DTypeConstructor::operator[](size_t index) const TypeNode DTypeConstructor::getArgType(size_t index) const { Assert(index < getNumArgs()); - return (*this)[index].getType().getSelectorRangeType(); + return (*this)[index].getType().getDatatypeSelectorRangeType(); } Node DTypeConstructor::getSelectorInternal(TypeNode domainType, @@ -260,7 +260,7 @@ Node DTypeConstructor::getSelectorInternal(TypeNode domainType, int DTypeConstructor::getSelectorIndexInternal(Node sel) const { Assert(isResolved()); - Assert(sel.getType().isSelector()); + Assert(sel.getType().isDatatypeSelector()); // might be a builtin selector if (sel.hasAttribute(DTypeIndexAttr())) { @@ -271,7 +271,7 @@ int DTypeConstructor::getSelectorIndexInternal(Node sel) const } } // otherwise, check shared selector - TypeNode domainType = sel.getType().getSelectorDomainType(); + TypeNode domainType = sel.getType().getDatatypeSelectorDomainType(); computeSharedSelectors(domainType); std::map::iterator its = d_sharedSelectorIndex[domainType].find(sel); @@ -471,7 +471,7 @@ void DTypeConstructor::computeSharedSelectors(TypeNode domainType) const { ctype = d_constructor.getType(); } - Assert(ctype.isConstructor()); + Assert(ctype.isDatatypeConstructor()); Assert(ctype.getNumChildren() - 1 == getNumArgs()); // compute the shared selectors const DType& dt = DType::datatypeOf(d_constructor); @@ -614,7 +614,7 @@ bool DTypeConstructor::resolve( nm->mkConstructorType(argTypes, self), "is a constructor", SkolemManager::SKOLEM_EXACT_NAME); - Assert(d_constructor.getType().isConstructor()); + Assert(d_constructor.getType().isDatatypeConstructor()); // associate constructor with all selectors for (std::shared_ptr sel : d_args) { diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 6bd665f26..7ab63bc78 100644 --- a/src/expr/node_manager_template.cpp +++ b/src/expr/node_manager_template.cpp @@ -675,10 +675,11 @@ std::vector NodeManager::mkMutualDatatypeTypes( { const DTypeConstructor& c = dt[i]; TypeNode testerType CVC5_UNUSED = c.getTester().getType(); - Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut) + Assert(c.isResolved() && testerType.isDatatypeTester() + && testerType[0] == ut) << "malformed tester in datatype post-resolution"; TypeNode ctorType CVC5_UNUSED = c.getConstructor().getType(); - Assert(ctorType.isConstructor() + Assert(ctorType.isDatatypeConstructor() && ctorType.getNumChildren() == c.getNumArgs() + 1 && ctorType.getRangeType() == ut) << "malformed constructor in datatype post-resolution"; @@ -687,7 +688,7 @@ std::vector NodeManager::mkMutualDatatypeTypes( { const DTypeSelector& a = c[j]; TypeNode selectorType = a.getType(); - Assert(a.isResolved() && selectorType.isSelector() + Assert(a.isResolved() && selectorType.isDatatypeSelector() && selectorType[0] == ut) << "malformed selector in datatype post-resolution"; // This next one's a "hard" check, performed in non-debug builds @@ -1258,15 +1259,15 @@ Kind NodeManager::getKindForFunction(TNode fun) { return kind::APPLY_UF; } - else if (tn.isConstructor()) + else if (tn.isDatatypeConstructor()) { return kind::APPLY_CONSTRUCTOR; } - else if (tn.isSelector()) + else if (tn.isDatatypeSelector()) { return kind::APPLY_SELECTOR; } - else if (tn.isTester()) + else if (tn.isDatatypeTester()) { return kind::APPLY_TESTER; } diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp index a765da157..ae5ef34f6 100644 --- a/src/expr/symbol_table.cpp +++ b/src/expr/symbol_table.cpp @@ -246,20 +246,20 @@ bool OverloadedTypeTrie::markOverloaded(const string& name, cvc5::Term obj) argTypes = t.getFunctionDomainSorts(); rangeType = t.getFunctionCodomainSort(); } - else if (t.isConstructor()) + else if (t.isDatatypeConstructor()) { - argTypes = t.getConstructorDomainSorts(); - rangeType = t.getConstructorCodomainSort(); + argTypes = t.getDatatypeConstructorDomainSorts(); + rangeType = t.getDatatypeConstructorCodomainSort(); } - else if (t.isTester()) + else if (t.isDatatypeTester()) { - argTypes.push_back(t.getTesterDomainSort()); - rangeType = t.getTesterCodomainSort(); + argTypes.push_back(t.getDatatypeTesterDomainSort()); + rangeType = t.getDatatypeTesterCodomainSort(); } - else if (t.isSelector()) + else if (t.isDatatypeSelector()) { - argTypes.push_back(t.getSelectorDomainSort()); - rangeType = t.getSelectorCodomainSort(); + argTypes.push_back(t.getDatatypeSelectorDomainSort()); + rangeType = t.getDatatypeSelectorCodomainSort(); } // add to the trie TypeArgTrie* tat = &d_overload_type_arg_trie[name]; diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index e84a7046d..d86f197e5 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -173,7 +173,7 @@ CardinalityClass TypeNode::getCardinalityClass() // else, function types whose range type is INFINITE, ONE, or // INTERPRETED_ONE have the same cardinality class as their range. } - else if (isConstructor()) + else if (isDatatypeConstructor()) { // notice that we require computing the cardinality class of the // constructor type, which is equivalent to asking how many @@ -321,9 +321,9 @@ bool TypeNode::isComparableTo(TypeNode t) const { return false; } -TypeNode TypeNode::getTesterDomainType() const +TypeNode TypeNode::getDatatypeTesterDomainType() const { - Assert(isTester()); + Assert(isDatatypeTester()); return (*this)[0]; } @@ -349,12 +349,16 @@ TypeNode TypeNode::getBaseType() const { std::vector TypeNode::getArgTypes() const { vector args; - if(isTester()) { + if (isDatatypeTester()) + { Assert(getNumChildren() == 1); args.push_back((*this)[0]); - } else { - Assert(isFunction() || isConstructor() || isSelector()); - for(unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) { + } + else + { + Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector()); + for (uint32_t i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) + { args.push_back((*this)[i]); } } @@ -610,16 +614,25 @@ bool TypeNode::isParametricDatatype() const return getKind() == kind::PARAMETRIC_DATATYPE; } -bool TypeNode::isConstructor() const +bool TypeNode::isDatatypeConstructor() const { return getKind() == kind::CONSTRUCTOR_TYPE; } -bool TypeNode::isSelector() const { return getKind() == kind::SELECTOR_TYPE; } +bool TypeNode::isDatatypeSelector() const +{ + return getKind() == kind::SELECTOR_TYPE; +} -bool TypeNode::isTester() const { return getKind() == kind::TESTER_TYPE; } +bool TypeNode::isDatatypeTester() const +{ + return getKind() == kind::TESTER_TYPE; +} -bool TypeNode::isUpdater() const { return getKind() == kind::UPDATER_TYPE; } +bool TypeNode::isDatatypeUpdater() const +{ + return getKind() == kind::UPDATER_TYPE; +} bool TypeNode::isCodatatype() const { @@ -681,11 +694,11 @@ uint32_t TypeNode::getBitVectorSize() const TypeNode TypeNode::getRangeType() const { - if (isTester()) + if (isDatatypeTester()) { return NodeManager::currentNM()->booleanType(); } - Assert(isFunction() || isConstructor() || isSelector()) + Assert(isFunction() || isDatatypeConstructor() || isDatatypeSelector()) << "Cannot get range type of " << *this; return (*this)[getNumChildren() - 1]; } diff --git a/src/expr/type_node.h b/src/expr/type_node.h index d8e7abd38..8f844dfb0 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -483,16 +483,16 @@ private: TypeNode getArrayConstituentType() const; /** Get the return type (for constructor types) */ - TypeNode getConstructorRangeType() const; + TypeNode getDatatypeConstructorRangeType() const; /** Get the domain type (for selector types) */ - TypeNode getSelectorDomainType() const; + TypeNode getDatatypeSelectorDomainType() const; /** Get the return type (for selector types) */ - TypeNode getSelectorRangeType() const; + TypeNode getDatatypeSelectorRangeType() const; /** Get the domain type (for tester types) */ - TypeNode getTesterDomainType() const; + TypeNode getDatatypeTesterDomainType() const; /** Get the element type (for set types) */ TypeNode getSetElementType() const; @@ -639,37 +639,37 @@ private: /** Is this an instantiated datatype parameter */ bool isParameterInstantiatedDatatype(size_t n) const; - /** Is this a constructor type */ - bool isConstructor() const; + /** Is this a datatype constructor type? */ + bool isDatatypeConstructor() const; - /** Is this a selector type */ - bool isSelector() const; + /** Is this a datatype selector type? */ + bool isDatatypeSelector() const; - /** Is this a tester type */ - bool isTester() const; + /** Is this a datatype tester type? */ + bool isDatatypeTester() const; - /** Is this a datatype updater type */ - bool isUpdater() const; + /** Is this a datatype updater type? */ + bool isDatatypeUpdater() const; - /** Get the internal Datatype specification from a datatype type */ + /** Get the internal Datatype specification from a datatype type. */ const DType& getDType() const; - /** Get the exponent size of this floating-point type */ + /** Get the exponent size of this floating-point type. */ unsigned getFloatingPointExponentSize() const; - /** Get the significand size of this floating-point type */ + /** Get the significand size of this floating-point type. */ unsigned getFloatingPointSignificandSize() const; - /** Get the size of this bit-vector type */ + /** Get the size of this bit-vector type. */ uint32_t getBitVectorSize() const; - /** Is this a sort kind */ + /** Is this a sort kind? */ bool isUninterpretedSort() const; - /** Is this a sort constructor kind */ + /** Is this a sort constructor kind? */ bool isUninterpretedSortConstructor() const; - /** Get sort constructor arity */ + /** Get sort constructor arity. */ uint64_t getUninterpretedSortConstructorArity() const; /** @@ -917,20 +917,21 @@ inline TypeNode TypeNode::getArrayConstituentType() const { return (*this)[1]; } -inline TypeNode TypeNode::getConstructorRangeType() const { - Assert(isConstructor()); +inline TypeNode TypeNode::getDatatypeConstructorRangeType() const +{ + Assert(isDatatypeConstructor()); return (*this)[getNumChildren()-1]; } -inline TypeNode TypeNode::getSelectorDomainType() const +inline TypeNode TypeNode::getDatatypeSelectorDomainType() const { - Assert(isSelector()); + Assert(isDatatypeSelector()); return (*this)[0]; } -inline TypeNode TypeNode::getSelectorRangeType() const +inline TypeNode TypeNode::getDatatypeSelectorRangeType() const { - Assert(isSelector()); + Assert(isDatatypeSelector()); return (*this)[1]; } diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp index ac93ca191..72a918259 100644 --- a/src/parser/parser.cpp +++ b/src/parser/parser.cpp @@ -119,7 +119,7 @@ cvc5::Term Parser::getExpressionForNameAndType(const std::string& name, // now, post-process the expression Assert(!expr.isNull()); cvc5::Sort te = expr.getSort(); - if (te.isConstructor() && te.getConstructorArity() == 0) + if (te.isDatatypeConstructor() && te.getDatatypeConstructorArity() == 0) { // nullary constructors have APPLY_CONSTRUCTOR kind with no children expr = d_solver->mkTerm(cvc5::APPLY_CONSTRUCTOR, {expr}); @@ -136,19 +136,19 @@ cvc5::Kind Parser::getKindForFunction(cvc5::Term fun) { return cvc5::APPLY_UF; } - else if (t.isConstructor()) + else if (t.isDatatypeConstructor()) { return cvc5::APPLY_CONSTRUCTOR; } - else if (t.isSelector()) + else if (t.isDatatypeSelector()) { return cvc5::APPLY_SELECTOR; } - else if (t.isTester()) + else if (t.isDatatypeTester()) { return cvc5::APPLY_TESTER; } - else if (t.isUpdater()) + else if (t.isDatatypeUpdater()) { return cvc5::APPLY_UPDATER; } @@ -190,8 +190,8 @@ bool Parser::isFunctionLike(cvc5::Term fun) return false; } cvc5::Sort type = fun.getSort(); - return type.isFunction() || type.isConstructor() || type.isTester() || - type.isSelector(); + return type.isFunction() || type.isDatatypeConstructor() + || type.isDatatypeTester() || type.isDatatypeSelector(); } /* Returns true if name is bound to a function returning boolean. */ @@ -567,12 +567,12 @@ cvc5::Term Parser::applyTypeAscription(cvc5::Term t, cvc5::Sort s) } // !!! temporary until datatypes are refactored in the new API cvc5::Sort etype = t.getSort(); - if (etype.isConstructor()) + if (etype.isDatatypeConstructor()) { // Type ascriptions only have an effect on the node structure if this is a // parametric datatype. // get the datatype that t belongs to - cvc5::Sort etyped = etype.getConstructorCodomainSort(); + cvc5::Sort etyped = etype.getDatatypeConstructorCodomainSort(); cvc5::Datatype d = etyped.getDatatype(); // Note that we check whether the datatype is parametric, and not whether // etyped is a parametric datatype, since e.g. the smt2 parser constructs @@ -588,7 +588,7 @@ cvc5::Term Parser::applyTypeAscription(cvc5::Term t, cvc5::Sort s) } // the type of t does not match the sort s by design (constructor type // vs datatype type), thus we use an alternative check here. - if (t.getSort().getConstructorCodomainSort() != s) + if (t.getSort().getDatatypeConstructorCodomainSort() != s) { std::stringstream ss; ss << "Type ascription on constructor not satisfied, term " << t diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g index 7361b70a0..419d54227 100644 --- a/src/parser/smt2/Smt2.g +++ b/src/parser/smt2/Smt2.g @@ -1370,11 +1370,12 @@ termNonVariable[cvc5::Term& expr, cvc5::Term& expr2] // f should be a constructor type = f.getSort(); Trace("parser-dt") << "Pattern head : " << f << " " << type << std::endl; - if (!type.isConstructor()) + if (!type.isDatatypeConstructor()) { PARSER_STATE->parseError("Pattern must be application of a constructor or a variable."); } - cvc5::Datatype dt = type.getConstructorCodomainSort().getDatatype(); + cvc5::Datatype dt = + type.getDatatypeConstructorCodomainSort().getDatatype(); if (dt.isParametric()) { // lookup constructor by name @@ -1383,7 +1384,7 @@ termNonVariable[cvc5::Term& expr, cvc5::Term& expr2] // take the type of the specialized constructor instead type = scons.getSort(); } - argTypes = type.getConstructorDomainSorts(); + argTypes = type.getDatatypeConstructorDomainSorts(); } // arguments of the pattern ( symbol[name,CHECK_NONE,SYM_VARIABLE] { @@ -1415,8 +1416,8 @@ termNonVariable[cvc5::Term& expr, cvc5::Term& expr2] { f = PARSER_STATE->getVariable(name); type = f.getSort(); - if (!type.isConstructor() || - !type.getConstructorDomainSorts().empty()) + if (!type.isDatatypeConstructor() || + !type.getDatatypeConstructorDomainSorts().empty()) { PARSER_STATE->parseError("Must apply constructors of arity greater than 0 to arguments in pattern."); } @@ -1609,13 +1610,13 @@ identifier[cvc5::ParseOp& p] // for nullary constructors, must get the operator f = f[0]; } - if (!f.getSort().isConstructor()) + if (!f.getSort().isDatatypeConstructor()) { PARSER_STATE->parseError( "Bad syntax for (_ is X), X must be a constructor."); } // get the datatype that f belongs to - cvc5::Sort sf = f.getSort().getConstructorCodomainSort(); + cvc5::Sort sf = f.getSort().getDatatypeConstructorCodomainSort(); cvc5::Datatype d = sf.getDatatype(); // lookup by name cvc5::DatatypeConstructor dc = d.getConstructor(f.toString()); @@ -1623,14 +1624,14 @@ identifier[cvc5::ParseOp& p] } | UPDATE_TOK term[f, f2] { - if (!f.getSort().isSelector()) + if (!f.getSort().isDatatypeSelector()) { PARSER_STATE->parseError( "Bad syntax for (_ update X), X must be a selector."); } std::string sname = f.toString(); // get the datatype that f belongs to - cvc5::Sort sf = f.getSort().getSelectorDomainSort(); + cvc5::Sort sf = f.getSort().getDatatypeSelectorDomainSort(); cvc5::Datatype d = sf.getDatatype(); // find the selector cvc5::DatatypeSelector ds = d.getSelector(f.toString()); diff --git a/src/proof/lfsc/lfsc_node_converter.cpp b/src/proof/lfsc/lfsc_node_converter.cpp index 4259dde07..c56aae9b9 100644 --- a/src/proof/lfsc/lfsc_node_converter.cpp +++ b/src/proof/lfsc/lfsc_node_converter.cpp @@ -118,8 +118,8 @@ Node LfscNodeConverter::postConvert(Node n) { // constructors/selectors are represented by skolems, which are defined // symbols - if (tn.isConstructor() || tn.isSelector() || tn.isTester() - || tn.isUpdater()) + if (tn.isDatatypeConstructor() || tn.isDatatypeSelector() + || tn.isDatatypeTester() || tn.isDatatypeUpdater()) { // note these are not converted to their user named (cvc.) symbols here, // to avoid type errors when constructing terms for postConvert @@ -728,12 +728,12 @@ Node LfscNodeConverter::maybeMkSkolemFun(Node k, bool macroApply) // a skolem corresponding to shared selector should print in // LFSC as (sel T n) where T is the type and n is the index of the // shared selector. - TypeNode fselt = nm->mkFunctionType(tn.getSelectorDomainType(), - tn.getSelectorRangeType()); + TypeNode fselt = nm->mkFunctionType(tn.getDatatypeSelectorDomainType(), + tn.getDatatypeSelectorRangeType()); TypeNode intType = nm->integerType(); TypeNode selt = nm->mkFunctionType({d_sortType, intType}, fselt); Node sel = getSymbolInternal(k.getKind(), selt, "sel"); - Node kn = typeAsNode(convertType(tn.getSelectorRangeType())); + Node kn = typeAsNode(convertType(tn.getDatatypeSelectorRangeType())); Assert(!cacheVal.isNull() && cacheVal.getKind() == CONST_RATIONAL); return nm->mkNode(APPLY_UF, sel, kn, cacheVal); } diff --git a/src/proof/lfsc/lfsc_printer.cpp b/src/proof/lfsc/lfsc_printer.cpp index bba0fad22..d412b8330 100644 --- a/src/proof/lfsc/lfsc_printer.cpp +++ b/src/proof/lfsc/lfsc_printer.cpp @@ -123,8 +123,8 @@ void LfscPrinter::print(std::ostream& out, for (const Node& s : syms) { TypeNode st = s.getType(); - if (st.isConstructor() || st.isSelector() || st.isTester() - || st.isUpdater()) + if (st.isDatatypeConstructor() || st.isDatatypeSelector() + || st.isDatatypeTester() || st.isDatatypeUpdater()) { // constructors, selector, testers, updaters are defined by the datatype continue; diff --git a/src/theory/datatypes/theory_datatypes_type_rules.cpp b/src/theory/datatypes/theory_datatypes_type_rules.cpp index 21bfb46b5..a7cacc7ca 100644 --- a/src/theory/datatypes/theory_datatypes_type_rules.cpp +++ b/src/theory/datatypes/theory_datatypes_type_rules.cpp @@ -36,11 +36,11 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager, { Assert(n.getKind() == kind::APPLY_CONSTRUCTOR); TypeNode consType = n.getOperator().getType(check); - if (!consType.isConstructor()) + if (!consType.isDatatypeConstructor()) { throw TypeCheckingExceptionPrivate(n, "expected constructor to apply"); } - TypeNode t = consType.getConstructorRangeType(); + TypeNode t = consType.getDatatypeConstructorRangeType(); Assert(t.isDatatype()); TNode::iterator child_it = n.begin(); TNode::iterator child_it_end = n.end(); @@ -96,7 +96,7 @@ TypeNode DatatypeConstructorTypeRule::computeType(NodeManager* nodeManager, } } } - return consType.getConstructorRangeType(); + return consType.getDatatypeConstructorRangeType(); } } @@ -262,7 +262,7 @@ TypeNode DatatypeAscriptionTypeRule::computeType(NodeManager* nodeManager, TypeMatcher m; if (childType.getKind() == kind::CONSTRUCTOR_TYPE) { - m.addTypesFromDatatype(childType.getConstructorRangeType()); + m.addTypesFromDatatype(childType.getDatatypeConstructorRangeType()); } else if (childType.getKind() == kind::DATATYPE_TYPE) { @@ -284,7 +284,7 @@ Cardinality ConstructorProperties::computeCardinality(TypeNode type) // Constructors aren't exactly functions, they're like // parameterized ground terms. So the cardinality is more like // that of a tuple than that of a function. - AssertArgument(type.isConstructor(), type); + AssertArgument(type.isDatatypeConstructor(), type); Cardinality c = 1; for (unsigned i = 0, i_end = type.getNumChildren(); i < i_end - 1; ++i) { diff --git a/src/theory/quantifiers/sygus/sygus_abduct.cpp b/src/theory/quantifiers/sygus/sygus_abduct.cpp index 07b849cd4..f2a065b1f 100644 --- a/src/theory/quantifiers/sygus/sygus_abduct.cpp +++ b/src/theory/quantifiers/sygus/sygus_abduct.cpp @@ -61,7 +61,8 @@ Node SygusAbduct::mkAbductionConjecture(const std::string& name, for (const Node& s : symset) { TypeNode tn = s.getType(); - if (tn.isConstructor() || tn.isSelector() || tn.isTester()) + if (tn.isDatatypeConstructor() || tn.isDatatypeSelector() + || tn.isDatatypeTester()) { // datatype symbols should be considered interpreted symbols here, not // (higher-order) variables. diff --git a/src/theory/quantifiers/sygus/sygus_interpol.cpp b/src/theory/quantifiers/sygus/sygus_interpol.cpp index e1c21c6b7..64ac9d49a 100644 --- a/src/theory/quantifiers/sygus/sygus_interpol.cpp +++ b/src/theory/quantifiers/sygus/sygus_interpol.cpp @@ -65,7 +65,8 @@ void SygusInterpol::createVariables(bool needsShared) for (const Node& s : d_syms) { TypeNode tn = s.getType(); - if (tn.isConstructor() || tn.isSelector() || tn.isTester()) + if (tn.isDatatypeConstructor() || tn.isDatatypeSelector() + || tn.isDatatypeTester()) { // datatype symbols should be considered interpreted symbols here, not // (higher-order) variables. diff --git a/test/unit/api/cpp/sort_black.cpp b/test/unit/api/cpp/sort_black.cpp index 759fd1543..3f02933db 100644 --- a/test/unit/api/cpp/sort_black.cpp +++ b/test/unit/api/cpp/sort_black.cpp @@ -147,8 +147,8 @@ TEST_F(TestApiBlackSort, isConstructor) Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort cons_sort = dt[0].getConstructorTerm().getSort(); - ASSERT_TRUE(cons_sort.isConstructor()); - ASSERT_NO_THROW(Sort().isConstructor()); + ASSERT_TRUE(cons_sort.isDatatypeConstructor()); + ASSERT_NO_THROW(Sort().isDatatypeConstructor()); } TEST_F(TestApiBlackSort, isSelector) @@ -156,8 +156,8 @@ TEST_F(TestApiBlackSort, isSelector) Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort cons_sort = dt[0][1].getSelectorTerm().getSort(); - ASSERT_TRUE(cons_sort.isSelector()); - ASSERT_NO_THROW(Sort().isSelector()); + ASSERT_TRUE(cons_sort.isDatatypeSelector()); + ASSERT_NO_THROW(Sort().isDatatypeSelector()); } TEST_F(TestApiBlackSort, isTester) @@ -165,8 +165,8 @@ TEST_F(TestApiBlackSort, isTester) Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort testerSort = dt[0].getTesterTerm().getSort(); - ASSERT_TRUE(testerSort.isTester()); - ASSERT_NO_THROW(Sort().isTester()); + ASSERT_TRUE(testerSort.isDatatypeTester()); + ASSERT_NO_THROW(Sort().isDatatypeTester()); } TEST_F(TestApiBlackSort, isUpdater) @@ -174,8 +174,8 @@ TEST_F(TestApiBlackSort, isUpdater) Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort updaterSort = dt[0][0].getUpdaterTerm().getSort(); - ASSERT_TRUE(updaterSort.isUpdater()); - ASSERT_NO_THROW(Sort().isUpdater()); + ASSERT_TRUE(updaterSort.isDatatypeUpdater()); + ASSERT_NO_THROW(Sort().isDatatypeUpdater()); } TEST_F(TestApiBlackSort, isFunction) @@ -265,41 +265,42 @@ TEST_F(TestApiBlackSort, datatypeSorts) Sort intSort = d_solver.getIntegerSort(); Sort dtypeSort = create_datatype_sort(); Datatype dt = dtypeSort.getDatatype(); - ASSERT_FALSE(dtypeSort.isConstructor()); - ASSERT_THROW(dtypeSort.getConstructorCodomainSort(), CVC5ApiException); - ASSERT_THROW(dtypeSort.getConstructorDomainSorts(), CVC5ApiException); - ASSERT_THROW(dtypeSort.getConstructorArity(), CVC5ApiException); + ASSERT_FALSE(dtypeSort.isDatatypeConstructor()); + ASSERT_THROW(dtypeSort.getDatatypeConstructorCodomainSort(), + CVC5ApiException); + ASSERT_THROW(dtypeSort.getDatatypeConstructorDomainSorts(), CVC5ApiException); + ASSERT_THROW(dtypeSort.getDatatypeConstructorArity(), CVC5ApiException); // get constructor DatatypeConstructor dcons = dt[0]; Term consTerm = dcons.getConstructorTerm(); Sort consSort = consTerm.getSort(); - ASSERT_TRUE(consSort.isConstructor()); - ASSERT_FALSE(consSort.isTester()); - ASSERT_FALSE(consSort.isSelector()); - ASSERT_EQ(consSort.getConstructorArity(), 2); - std::vector consDomSorts = consSort.getConstructorDomainSorts(); + ASSERT_TRUE(consSort.isDatatypeConstructor()); + ASSERT_FALSE(consSort.isDatatypeTester()); + ASSERT_FALSE(consSort.isDatatypeSelector()); + ASSERT_EQ(consSort.getDatatypeConstructorArity(), 2); + std::vector consDomSorts = consSort.getDatatypeConstructorDomainSorts(); ASSERT_EQ(consDomSorts[0], intSort); ASSERT_EQ(consDomSorts[1], dtypeSort); - ASSERT_EQ(consSort.getConstructorCodomainSort(), dtypeSort); + ASSERT_EQ(consSort.getDatatypeConstructorCodomainSort(), dtypeSort); // get tester Term isConsTerm = dcons.getTesterTerm(); - ASSERT_TRUE(isConsTerm.getSort().isTester()); - ASSERT_EQ(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); + ASSERT_TRUE(isConsTerm.getSort().isDatatypeTester()); + ASSERT_EQ(isConsTerm.getSort().getDatatypeTesterDomainSort(), dtypeSort); Sort booleanSort = d_solver.getBooleanSort(); - ASSERT_EQ(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); - ASSERT_THROW(booleanSort.getTesterDomainSort(), CVC5ApiException); - ASSERT_THROW(booleanSort.getTesterCodomainSort(), CVC5ApiException); + ASSERT_EQ(isConsTerm.getSort().getDatatypeTesterCodomainSort(), booleanSort); + ASSERT_THROW(booleanSort.getDatatypeTesterDomainSort(), CVC5ApiException); + ASSERT_THROW(booleanSort.getDatatypeTesterCodomainSort(), CVC5ApiException); // get selector DatatypeSelector dselTail = dcons[1]; Term tailTerm = dselTail.getSelectorTerm(); - ASSERT_TRUE(tailTerm.getSort().isSelector()); - ASSERT_EQ(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); - ASSERT_EQ(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); - ASSERT_THROW(booleanSort.getSelectorDomainSort(), CVC5ApiException); - ASSERT_THROW(booleanSort.getSelectorCodomainSort(), CVC5ApiException); + ASSERT_TRUE(tailTerm.getSort().isDatatypeSelector()); + ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort); + ASSERT_EQ(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort); + ASSERT_THROW(booleanSort.getDatatypeSelectorDomainSort(), CVC5ApiException); + ASSERT_THROW(booleanSort.getDatatypeSelectorCodomainSort(), CVC5ApiException); } TEST_F(TestApiBlackSort, instantiate) diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java index 15d3fb106..3884dc35b 100644 --- a/test/unit/api/java/SortTest.java +++ b/test/unit/api/java/SortTest.java @@ -161,33 +161,33 @@ class SortTest } @Test - void isConstructor() throws CVC5ApiException + void isDatatypeConstructor() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort cons_sort = dt.getConstructor(0).getConstructorTerm().getSort(); - assertTrue(cons_sort.isConstructor()); - assertDoesNotThrow(() -> d_solver.getNullSort().isConstructor()); + assertTrue(cons_sort.isDatatypeConstructor()); + assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeConstructor()); } @Test - void isSelector() throws CVC5ApiException + void isDatatypeSelector() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort cons_sort = dt.getConstructor(0).getSelector(1).getSelectorTerm().getSort(); - assertTrue(cons_sort.isSelector()); - assertDoesNotThrow(() -> d_solver.getNullSort().isSelector()); + assertTrue(cons_sort.isDatatypeSelector()); + assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeSelector()); } @Test - void isTester() throws CVC5ApiException + void isDatatypeTester() throws CVC5ApiException { Sort dt_sort = create_datatype_sort(); Datatype dt = dt_sort.getDatatype(); Sort cons_sort = dt.getConstructor(0).getTesterTerm().getSort(); - assertTrue(cons_sort.isTester()); - assertDoesNotThrow(() -> d_solver.getNullSort().isTester()); + assertTrue(cons_sort.isDatatypeTester()); + assertDoesNotThrow(() -> d_solver.getNullSort().isDatatypeTester()); } @Test @@ -287,41 +287,41 @@ class SortTest Sort intSort = d_solver.getIntegerSort(); Sort dtypeSort = create_datatype_sort(); Datatype dt = dtypeSort.getDatatype(); - assertFalse(dtypeSort.isConstructor()); - assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorCodomainSort()); - assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorDomainSorts()); - assertThrows(CVC5ApiException.class, () -> dtypeSort.getConstructorArity()); + assertFalse(dtypeSort.isDatatypeConstructor()); + assertThrows(CVC5ApiException.class, () -> dtypeSort.getDatatypeConstructorCodomainSort()); + assertThrows(CVC5ApiException.class, () -> dtypeSort.getDatatypeConstructorDomainSorts()); + assertThrows(CVC5ApiException.class, () -> dtypeSort.getDatatypeConstructorArity()); // get constructor DatatypeConstructor dcons = dt.getConstructor(0); Term consTerm = dcons.getConstructorTerm(); Sort consSort = consTerm.getSort(); - assertTrue(consSort.isConstructor()); - assertFalse(consSort.isTester()); - assertFalse(consSort.isSelector()); - assertEquals(consSort.getConstructorArity(), 2); - Sort[] consDomSorts = consSort.getConstructorDomainSorts(); + assertTrue(consSort.isDatatypeConstructor()); + assertFalse(consSort.isDatatypeTester()); + assertFalse(consSort.isDatatypeSelector()); + assertEquals(consSort.getDatatypeConstructorArity(), 2); + Sort[] consDomSorts = consSort.getDatatypeConstructorDomainSorts(); assertEquals(consDomSorts[0], intSort); assertEquals(consDomSorts[1], dtypeSort); - assertEquals(consSort.getConstructorCodomainSort(), dtypeSort); + assertEquals(consSort.getDatatypeConstructorCodomainSort(), dtypeSort); // get tester Term isConsTerm = dcons.getTesterTerm(); - assertTrue(isConsTerm.getSort().isTester()); - assertEquals(isConsTerm.getSort().getTesterDomainSort(), dtypeSort); + assertTrue(isConsTerm.getSort().isDatatypeTester()); + assertEquals(isConsTerm.getSort().getDatatypeTesterDomainSort(), dtypeSort); Sort booleanSort = d_solver.getBooleanSort(); - assertEquals(isConsTerm.getSort().getTesterCodomainSort(), booleanSort); - assertThrows(CVC5ApiException.class, () -> booleanSort.getTesterDomainSort()); - assertThrows(CVC5ApiException.class, () -> booleanSort.getTesterCodomainSort()); + assertEquals(isConsTerm.getSort().getDatatypeTesterCodomainSort(), booleanSort); + assertThrows(CVC5ApiException.class, () -> booleanSort.getDatatypeTesterDomainSort()); + assertThrows(CVC5ApiException.class, () -> booleanSort.getDatatypeTesterCodomainSort()); // get selector DatatypeSelector dselTail = dcons.getSelector(1); Term tailTerm = dselTail.getSelectorTerm(); - assertTrue(tailTerm.getSort().isSelector()); - assertEquals(tailTerm.getSort().getSelectorDomainSort(), dtypeSort); - assertEquals(tailTerm.getSort().getSelectorCodomainSort(), dtypeSort); - assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorDomainSort()); - assertThrows(CVC5ApiException.class, () -> booleanSort.getSelectorCodomainSort()); + assertTrue(tailTerm.getSort().isDatatypeSelector()); + assertEquals(tailTerm.getSort().getDatatypeSelectorDomainSort(), dtypeSort); + assertEquals(tailTerm.getSort().getDatatypeSelectorCodomainSort(), dtypeSort); + assertThrows(CVC5ApiException.class, () -> booleanSort.getDatatypeSelectorDomainSort()); + assertThrows(CVC5ApiException.class, () -> booleanSort.getDatatypeSelectorCodomainSort()); } @Test diff --git a/test/unit/api/python/test_sort.py b/test/unit/api/python/test_sort.py index ab2375059..941e948bb 100644 --- a/test/unit/api/python/test_sort.py +++ b/test/unit/api/python/test_sort.py @@ -137,8 +137,8 @@ def test_is_constructor(solver): dt_sort = create_datatype_sort(solver) dt = dt_sort.getDatatype() cons_sort = dt[0].getConstructorTerm().getSort() - assert cons_sort.isConstructor() - Sort(solver).isConstructor() + assert cons_sort.isDatatypeConstructor() + Sort(solver).isDatatypeConstructor() def test_is_selector(solver): @@ -147,23 +147,23 @@ def test_is_selector(solver): dt0 = dt[0] dt01 = dt0[1] cons_sort = dt01.getSelectorTerm().getSort() - assert cons_sort.isSelector() - Sort(solver).isSelector() + assert cons_sort.isDatatypeSelector() + Sort(solver).isDatatypeSelector() def test_is_tester(solver): dt_sort = create_datatype_sort(solver) dt = dt_sort.getDatatype() cons_sort = dt[0].getTesterTerm().getSort() - assert cons_sort.isTester() - Sort(solver).isTester() + assert cons_sort.isDatatypeTester() + Sort(solver).isDatatypeTester() def test_is_updater(solver): dt_sort = create_datatype_sort(solver) dt = dt_sort.getDatatype() updater_sort = dt[0][0].getUpdaterTerm().getSort() - assert updater_sort.isUpdater() - Sort(solver).isUpdater() + assert updater_sort.isDatatypeUpdater() + Sort(solver).isDatatypeUpdater() def test_is_function(solver): fun_sort = solver.mkFunctionSort(solver.getRealSort(), @@ -240,49 +240,49 @@ def test_datatype_sorts(solver): intSort = solver.getIntegerSort() dtypeSort = create_datatype_sort(solver) dt = dtypeSort.getDatatype() - assert not dtypeSort.isConstructor() + assert not dtypeSort.isDatatypeConstructor() with pytest.raises(RuntimeError): - dtypeSort.getConstructorCodomainSort() + dtypeSort.getDatatypeConstructorCodomainSort() with pytest.raises(RuntimeError): - dtypeSort.getConstructorDomainSorts() + dtypeSort.getDatatypeConstructorDomainSorts() with pytest.raises(RuntimeError): - dtypeSort.getConstructorArity() + dtypeSort.getDatatypeConstructorArity() # get constructor dcons = dt[0] consTerm = dcons.getConstructorTerm() consSort = consTerm.getSort() - assert consSort.isConstructor() - assert not consSort.isTester() - assert not consSort.isSelector() - assert consSort.getConstructorArity() == 2 - consDomSorts = consSort.getConstructorDomainSorts() + assert consSort.isDatatypeConstructor() + assert not consSort.isDatatypeTester() + assert not consSort.isDatatypeSelector() + assert consSort.getDatatypeConstructorArity() == 2 + consDomSorts = consSort.getDatatypeConstructorDomainSorts() assert consDomSorts[0] == intSort assert consDomSorts[1] == dtypeSort - assert consSort.getConstructorCodomainSort() == dtypeSort + assert consSort.getDatatypeConstructorCodomainSort() == dtypeSort # get tester isConsTerm = dcons.getTesterTerm() - assert isConsTerm.getSort().isTester() + assert isConsTerm.getSort().isDatatypeTester() booleanSort = solver.getBooleanSort() - assert isConsTerm.getSort().getTesterDomainSort() == dtypeSort - assert isConsTerm.getSort().getTesterCodomainSort() == booleanSort + assert isConsTerm.getSort().getDatatypeTesterDomainSort() == dtypeSort + assert isConsTerm.getSort().getDatatypeTesterCodomainSort() == booleanSort with pytest.raises(RuntimeError): - booleanSort.getTesterDomainSort() + booleanSort.getDatatypeTesterDomainSort() with pytest.raises(RuntimeError): - booleanSort.getTesterCodomainSort() + booleanSort.getDatatypeTesterCodomainSort() # get selector dselTail = dcons[1] tailTerm = dselTail.getSelectorTerm() - assert tailTerm.getSort().isSelector() - assert tailTerm.getSort().getSelectorDomainSort() == dtypeSort - assert tailTerm.getSort().getSelectorCodomainSort() == dtypeSort + assert tailTerm.getSort().isDatatypeSelector() + assert tailTerm.getSort().getDatatypeSelectorDomainSort() == dtypeSort + assert tailTerm.getSort().getDatatypeSelectorCodomainSort() == dtypeSort with pytest.raises(RuntimeError): - booleanSort.getSelectorDomainSort() + booleanSort.getDatatypeSelectorDomainSort() with pytest.raises(RuntimeError): - booleanSort.getSelectorCodomainSort() + booleanSort.getDatatypeSelectorCodomainSort() def test_instantiate(solver):