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;
}
/* 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> Sort::getConstructorDomainSorts() const
+std::vector<Sort> 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();
////////
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
*/
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<Sort> getConstructorDomainSorts() const;
+ std::vector<Sort> 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 ------------------------------------------------------- */
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?
/* 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 ------------------------------------------------------- */
/*
* 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<Sort*>(pointer);
- return static_cast<jboolean>(current->isConstructor());
+ return static_cast<jboolean>(current->isDatatypeConstructor());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Sort*>(pointer);
- return static_cast<jboolean>(current->isSelector());
+ return static_cast<jboolean>(current->isDatatypeSelector());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Sort*>(pointer);
- return static_cast<jboolean>(current->isTester());
+ return static_cast<jboolean>(current->isDatatypeTester());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(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<Sort*>(pointer);
- return static_cast<jboolean>(current->isUpdater());
+ return static_cast<jboolean>(current->isDatatypeUpdater());
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, static_cast<jboolean>(false));
}
/*
* 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<Sort*>(pointer);
- return static_cast<jint>(current->getConstructorArity());
+ return static_cast<jint>(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<Sort*>(pointer);
- std::vector<Sort> sorts = current->getConstructorDomainSorts();
+ std::vector<Sort> sorts = current->getDatatypeConstructorDomainSorts();
std::vector<jlong> sortPointers(sorts.size());
for (size_t i = 0; i < sorts.size(); i++)
{
/*
* 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<Sort*>(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<Sort*>(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<Sort*>(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<Sort*>(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<Sort*>(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);
}
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 +
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 +
"""
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):
"""
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):
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);
}
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)
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,
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()))
{
}
}
// otherwise, check shared selector
- TypeNode domainType = sel.getType().getSelectorDomainType();
+ TypeNode domainType = sel.getType().getDatatypeSelectorDomainType();
computeSharedSelectors(domainType);
std::map<Node, unsigned>::iterator its =
d_sharedSelectorIndex[domainType].find(sel);
{
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);
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<DTypeSelector> sel : d_args)
{
{
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";
{
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
{
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;
}
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];
// 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
return false;
}
-TypeNode TypeNode::getTesterDomainType() const
+TypeNode TypeNode::getDatatypeTesterDomainType() const
{
- Assert(isTester());
+ Assert(isDatatypeTester());
return (*this)[0];
}
std::vector<TypeNode> TypeNode::getArgTypes() const {
vector<TypeNode> 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]);
}
}
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
{
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];
}
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;
/** 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;
/**
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];
}
// 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});
{
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;
}
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. */
}
// !!! 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
}
// 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
// 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
// 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] {
{
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.");
}
// 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());
}
| 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());
{
// 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
// 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);
}
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;
{
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();
}
}
}
- return consType.getConstructorRangeType();
+ return consType.getDatatypeConstructorRangeType();
}
}
TypeMatcher m;
if (childType.getKind() == kind::CONSTRUCTOR_TYPE)
{
- m.addTypesFromDatatype(childType.getConstructorRangeType());
+ m.addTypesFromDatatype(childType.getDatatypeConstructorRangeType());
}
else if (childType.getKind() == kind::DATATYPE_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)
{
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.
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.
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)
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)
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)
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)
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<Sort> consDomSorts = consSort.getConstructorDomainSorts();
+ ASSERT_TRUE(consSort.isDatatypeConstructor());
+ ASSERT_FALSE(consSort.isDatatypeTester());
+ ASSERT_FALSE(consSort.isDatatypeSelector());
+ ASSERT_EQ(consSort.getDatatypeConstructorArity(), 2);
+ std::vector<Sort> 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)
}
@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
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
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):
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(),
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):
projects / cvc5.git / commitdiff