This is in line with the change for non-parametric constructors (getConstructorTerm -> getTerm).
Also adds documentation to make the use of constructors, selectors, testers, updaters more clear.
CVC5_API_TRY_CATCH_END;
}
-Term DatatypeConstructor::getInstantiatedConstructorTerm(
- const Sort& retSort) const
+Term DatatypeConstructor::getInstantiatedTerm(const Sort& retSort) const
{
CVC5_API_TRY_CATCH_BEGIN;
CVC5_API_CHECK_NOT_NULL;
std::string getName() const;
/**
- * Get the selector operator of this datatype selector.
+ * Get the selector term of this datatype selector.
+ *
+ * Selector terms are a class of function-like terms of selector
+ * sort (Sort::isDatatypeSelector()), and should be used as the first
+ * argument of Terms of kind #APPLY_SELECTOR.
+ *
* @return the selector term
*/
Term getTerm() const;
/**
- * Get the updater operator of this datatype selector.
+ * Get the updater term of this datatype selector.
+ *
+ * Similar to selectors, updater terms are a class of function-like terms of
+ * updater Sort (Sort::isDatatypeUpdater()), and should be used as the first
+ * argument of Terms of kind #APPLY_UPDATER.
+ *
* @return the updater term
*/
Term getUpdaterTerm() const;
std::string getName() const;
/**
- * Get the constructor operator of this datatype constructor.
+ * Get the constructor term of this datatype constructor.
+ *
+ * Datatype constructors are a special class of function-like terms whose sort
+ * is datatype constructor (Sort::isDatatypeConstructor()). All datatype
+ * constructors, including nullary ones, should be used as the
+ * first argument to Terms whose kind is #APPLY_CONSTRUCTOR. For example,
+ * the nil list can be constructed by
+ * `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})`, where `t` is the term returned
+ * by this method.
+ *
+ * @note This method should not be used for parametric datatypes. Instead,
+ * use the method DatatypeConstructor::getInstantiatedTerm() below.
+ *
* @return the constructor term
*/
Term getTerm() const;
/**
- * Get the constructor operator of this datatype constructor whose return
+ * Get the constructor term of this datatype constructor whose return
* type is retSort. This method is intended to be used on constructors of
* parametric datatypes and can be seen as returning the constructor
* term that has been explicitly cast to the given sort.
* DatatypeConstructor is the one corresponding to nil, and retSort is
* `(List Int)`.
*
- * @note the returned constructor term `t` is an operator, while
+ * @note the returned constructor term `t` is the constructor, while
* `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the
* above (nullary) application of nil.
*
* @param retSort the desired return sort of the constructor
* @return the constructor term
*/
- Term getInstantiatedConstructorTerm(const Sort& retSort) const;
+ Term getInstantiatedTerm(const Sort& retSort) const;
/**
- * Get the tester operator of this datatype constructor.
- * @return the tester operator
+ * Get the tester term of this datatype constructor.
+ *
+ * Similar to constructors, testers are a class of function-like terms of
+ * tester sort (Sort::isDatatypeConstructor()) which should be used as the
+ * first argument of Terms of kind #APPLY_TESTER.
+ *
+ * @return the tester term
*/
Term getTesterTerm() const;
private native String getName(long pointer);
/**
- * Get the constructor operator of this datatype constructor.
+ * Get the constructor term of this datatype constructor.
+ *
+ * Datatype constructors are a special class of function-like terms whose sort
+ * is datatype constructor ({@link Sort#isDatatypeConstructor()}). All datatype
+ * constructors, including nullary ones, should be used as the
+ * first argument to Terms whose kind is APPLY_CONSTRUCTOR. For example,
+ * the nil list is represented by the term (APPLY_CONSTRUCTOR nil), where
+ * nil is the term returned by this method.
+ *
+ * @api.note This method should not be used for parametric datatypes. Instead,
+ * use the method {@link DatatypeConstructor#getInstantiatedTerm(Sort)} below.
+ *
* @return the constructor term
*/
public Term getTerm()
private native long getTerm(long pointer);
/**
- * Get the constructor operator of this datatype constructor whose return
+ * Get the constructor term of this datatype constructor whose return
* type is retSort. This method is intended to be used on constructors of
* parametric datatypes and can be seen as returning the constructor
* term that has been explicitly cast to the given sort.
* DatatypeConstructor is the one corresponding to nil, and retSort is
* (List Int).
*
- * Furthermore note that the returned constructor term t is an operator,
+ * Furthermore note that the returned constructor term t is the constructor,
* while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
* (nullary) application of nil.
*
* @param retSort the desired return sort of the constructor
* @return the constructor term
*/
- public Term getInstantiatedConstructorTerm(Sort retSort)
+ public Term getInstantiatedTerm(Sort retSort)
{
- long termPointer = getInstantiatedConstructorTerm(pointer, retSort.getPointer());
+ long termPointer = getInstantiatedTerm(pointer, retSort.getPointer());
return new Term(solver, termPointer);
}
- private native long getInstantiatedConstructorTerm(long pointer, long retSortPointer);
+ private native long getInstantiatedTerm(long pointer, long retSortPointer);
/**
- * Get the tester operator of this datatype constructor.
- * @return the tester operator
+ * Get the tester term of this datatype constructor.
+ *
+ * Similar to constructors, testers are a class of function-like terms of
+ * tester sort ({@link Sort#isDatatypeTester()}), and should be used as the first
+ * argument of Terms of kind APPLY_TESTER.
+ *
+ * @return the tester term
*/
public Term getTesterTerm()
{
private native String getName(long pointer);
/**
- * Get the selector operator of this datatype selector.
+ * Get the selector term of this datatype selector.
+ *
+ * Selector terms are a class of function-like terms of selector
+ * sort (Sort::isDatatypeSelector), and should be used as the first
+ * argument of Terms of kind APPLY_SELECTOR.
+ *
* @return the selector term
*/
public Term getTerm()
private native long getTerm(long pointer);
/**
- * Get the upater operator of this datatype selector.
+ * Get the updater term of this datatype selector.
+ *
+ * Similar to selectors, updater terms are a class of function-like terms of
+ * updater Sort (Sort::isDatatypeUpdater), and should be used as the first
+ * argument of Terms of kind APPLY_UPDATER.
+ *
* @return the updater term
*/
public Term getUpdaterTerm()
/*
* Class: io_github_cvc5_DatatypeConstructor
- * Method: getInstantiatedConstructorTerm
+ * Method: getInstantiatedTerm
* Signature: (JJ)J
*/
JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_DatatypeConstructor_getInstantiatedConstructorTerm(
+Java_io_github_cvc5_DatatypeConstructor_getInstantiatedTerm(
JNIEnv* env, jobject, jlong pointer, jlong retSortPointer)
{
CVC5_JAVA_API_TRY_CATCH_BEGIN;
DatatypeConstructor* current = (DatatypeConstructor*)pointer;
Sort* sort = (Sort*)retSortPointer;
- Term* retPointer = new Term(current->getInstantiatedConstructorTerm(*sort));
+ Term* retPointer = new Term(current->getInstantiatedTerm(*sort));
return (jlong)retPointer;
CVC5_JAVA_API_TRY_CATCH_END_RETURN(env, 0);
}
DatatypeSelector operator[](const string& name) except +
string getName() except +
Term getTerm() except +
- Term getInstantiatedConstructorTerm(const Sort& retSort) except +
+ Term getInstantiatedTerm(const Sort& retSort) except +
Term getTesterTerm() except +
size_t getNumSelectors() except +
DatatypeSelector getSelector(const string& name) except +
return self.cdc.getName().decode()
def getTerm(self):
- """
- :return: The constructor operator as a term.
+ """
+ Get the constructor term of this datatype constructor.
+
+ Datatype constructors are a special class of function-like terms
+ whose sort is datatype constructor
+ (:py:meth:`Sort.isDatatypeConstructor()`). All datatype
+ constructors, including nullary ones, should be used as the first
+ argument to Terms whose kind is
+ :py:obj:`APPLY_CONSTRUCTOR <cvc5.Kind.APPLY_CONSTRUCTOR>`.
+ For example, the nil list can be constructed via
+ ``Solver.mkTerm(APPLY_CONSTRUCTOR, [nil])``, where nil is the Term
+ returned by this method.
+
+ .. note::
+
+ This method should not be used for parametric datatypes.
+ Instead, use the method
+ :py:meth:`DatatypeConstructor.getInstantiatedTerm()` below.
+
+ :return: The constructor term.
"""
cdef Term term = Term(self.solver)
term.cterm = self.cdc.getTerm()
return term
- def getInstantiatedConstructorTerm(self, Sort retSort):
+ def getInstantiatedTerm(self, Sort retSort):
"""
- Get the constructor operator of this datatype constructor whose
+ Get the constructor term of this datatype constructor whose
return type is retSort. This method is intended to be used on
constructors of parametric datatypes and can be seen as returning
the constructor term that has been explicitly cast to the given
.. note::
- The returned constructor term ``t`` is an operator, while
+ The returned constructor term ``t`` is the constructor, while
``Solver.mkTerm(APPLY_CONSTRUCTOR, [t])`` is used to construct
the above (nullary) application of nil.
versions.
:param retSort: The desired return sort of the constructor.
- :return: The constructor operator as a term.
+ :return: The constructor term.
"""
cdef Term term = Term(self.solver)
- term.cterm = self.cdc.getInstantiatedConstructorTerm(retSort.csort)
+ term.cterm = self.cdc.getInstantiatedTerm(retSort.csort)
return term
def getTesterTerm(self):
"""
- :return: The tester operator that is related to this constructor,
- as a term.
+ Get the tester term of this datatype constructor.
+
+ Similar to constructors, testers are a class of function-like terms
+ of tester sort (:py:meth:`Sort.isDatatypeTester`), and should
+ be used as the first argument of Terms of kind APPLY_TESTER.
+
+ :return: The tester term for this constructor.
"""
cdef Term term = Term(self.solver)
term.cterm = self.cdc.getTesterTerm()
def getTerm(self):
"""
- :return: The selector opeartor of this datatype selector as a term.
+ Get the selector term of this datatype selector.
+
+ Selector terms are a class of function-like terms of selector
+ sort (:py:meth:`Sort.isDatatypeSelector()`), and should be used as
+ the first argument of Terms of kind
+ :py:obj:`APPLY_SELECTOR <cvc5.Kind.APPLY_SELECTOR>`.
+
+ :return: The selector term of this datatype selector.
"""
cdef Term term = Term(self.solver)
term.cterm = self.cds.getTerm()
def getUpdaterTerm(self):
"""
- :return: The updater opeartor of this datatype selector as a term.
+ Get the updater term of this datatype selector.
+
+ Similar to selectors, updater terms are a class of function-like
+ terms of updater Sort (:py:meth:`Sort.isDatatypeUpdater()`), and
+ should be used as the first argument of Terms of kind
+ :py:ob:`APPLY_UPDATER <cvc5.Kind.APPLY_UPDATER>`.
+
+ :return: The updater term of this datatype selector.
"""
cdef Term term = Term(self.solver)
term.cterm = self.cds.getUpdaterTerm()
// lookup by name
cvc5::DatatypeConstructor dc = d.getConstructor(t.toString());
// ask the constructor for the specialized constructor term
- t = dc.getInstantiatedConstructorTerm(s);
+ t = dc.getInstantiatedTerm(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.
{
// lookup constructor by name
cvc5::DatatypeConstructor dc = dt.getConstructor(f.toString());
- cvc5::Term scons = dc.getInstantiatedConstructorTerm(expr.getSort());
+ cvc5::Term scons = dc.getInstantiatedTerm(expr.getSort());
// take the type of the specialized constructor instead
type = scons.getSort();
}
Term testConsTerm;
// get the specialized constructor term for list[Int]
- ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedConstructorTerm(listInt));
+ ASSERT_NO_THROW(testConsTerm = nilc.getInstantiatedTerm(listInt));
ASSERT_NE(testConsTerm, nilc.getTerm());
// error to get the specialized constructor term for Int
- ASSERT_THROW(nilc.getInstantiatedConstructorTerm(isort), CVC5ApiException);
+ ASSERT_THROW(nilc.getInstantiatedTerm(isort), CVC5ApiException);
}
} // namespace test
} // namespace cvc5::internal
Term t53 = d_solver.mkTerm(MATCH_BIND_CASE,
{d_solver.mkTerm(VARIABLE_LIST, {t52}), t52, t18});
Term t73 = d_solver.mkVar(s1, "_x78");
- Term t81 =
- d_solver.mkTerm(MATCH_BIND_CASE,
- {d_solver.mkTerm(VARIABLE_LIST, {t73}),
- d_solver.mkTerm(APPLY_CONSTRUCTOR,
- {s6.getDatatype()
- .getConstructor("_x20")
- .getInstantiatedConstructorTerm(s6),
- t73}),
- t18});
+ Term t81 = d_solver.mkTerm(
+ MATCH_BIND_CASE,
+ {d_solver.mkTerm(VARIABLE_LIST, {t73}),
+ d_solver.mkTerm(
+ APPLY_CONSTRUCTOR,
+ {s6.getDatatype().getConstructor("_x20").getInstantiatedTerm(s6),
+ t73}),
+ t18});
Term t82 = d_solver.mkTerm(MATCH, {t13, t53, t53, t53, t81});
Term t325 = d_solver.mkTerm(
APPLY_SELECTOR,
AtomicReference<Term> atomicTerm = new AtomicReference<>();
// get the specialized constructor term for list[Int]
- assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedConstructorTerm(listInt)));
+ assertDoesNotThrow(() -> atomicTerm.set(nilc.getInstantiatedTerm(listInt)));
Term testConsTerm = atomicTerm.get();
assertNotEquals(testConsTerm, nilc.getTerm());
// error to get the specialized constructor term for Int
- assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedConstructorTerm(isort));
+ assertThrows(CVC5ApiException.class, () -> nilc.getInstantiatedTerm(isort));
}
}
testConsTerm = Term(solver)
# get the specialized constructor term for list[Int]
- testConsTerm = nilc.getInstantiatedConstructorTerm(listInt)
+ testConsTerm = nilc.getInstantiatedTerm(listInt)
assert testConsTerm != nilc.getTerm()
# error to get the specialized constructor term for Int
with pytest.raises(RuntimeError):
- nilc.getInstantiatedConstructorTerm(isort)
+ nilc.getInstantiatedTerm(isort)
projects / cvc5.git / commitdiff