From a8b58d71052ac692438f0303121adc06f08585ee Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Mon, 28 Mar 2022 14:23:21 -0700 Subject: [PATCH] [API] Mark methods as experimental (#8249) --- src/api/cpp/cvc5.h | 66 +++++++++++++++++-- .../github/cvc5/api/DatatypeConstructor.java | 2 + src/api/java/io/github/cvc5/api/Solver.java | 55 ++++++++++++++++ src/api/java/io/github/cvc5/api/Sort.java | 25 +++++-- src/api/python/cvc5.pxi | 61 ++++++++++++++++- 5 files changed, 194 insertions(+), 15 deletions(-) diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index eb9976361..4e8287fa8 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -604,14 +604,14 @@ class CVC5_EXPORT Sort * * Create sorts parameter with Solver::mkParamSort(). * + * @warning This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ Sort instantiate(const std::vector& params) const; /** * Substitution of Sorts. - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. @@ -619,18 +619,26 @@ class CVC5_EXPORT Sort * For example, * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will * return (Array (Array C D) B). + * + * @warning This method is experimental and may change in future versions. + * + * @param sort the subsort to be substituted within this sort. + * @param replacement the sort replacing the substituted subsort. */ Sort substitute(const Sort& sort, const Sort& replacement) const; /** * Simultaneous substitution of Sorts. - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. In the case that * sorts contains duplicates, the replacement earliest in the vector takes * priority. + * + * @warning This method is experimental and may change in future versions. + * + * @param sorts the subsorts to be substituted within this sort. + * @param replacements the sort replacing the substituted subsorts. */ Sort substitute(const std::vector& sorts, const std::vector& replacements) const; @@ -2036,6 +2044,8 @@ class CVC5_EXPORT DatatypeConstructor * `Solver::mkTerm(APPLY_CONSTRUCTOR, {t})` is used to construct the * above (nullary) application of nil. * + * @warning This method is experimental and may change in future versions. + * * @param retSort the desired return sort of the constructor * @return the constructor term */ @@ -3480,12 +3490,18 @@ class CVC5_EXPORT Solver /** * Create a separation logic empty term. + * + * @warning This method is experimental and may change in future versions. + * * @return the separation logic empty term */ Term mkSepEmp() const; /** * Create a separation logic nil term. + * + * @warning This method is experimental and may change in future versions. + * * @param sort the sort of the nil term * @return the separation logic nil term */ @@ -4072,16 +4088,20 @@ class CVC5_EXPORT Solver * :ref:`produce-proofs `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ std::string getProof() const; /** - * Get learned literals + * Get a list of learned literals that are entailed by the current set of + * assertions. * - * @return a list of literals that were learned at top-level. In other words, - * these are literals that are entailed by the current set of assertions. + * @warning This method is experimental and may change in future versions. + * + * @return a list of literals that were learned at top-level. */ std::vector getLearnedLiterals() const; @@ -4135,6 +4155,8 @@ class CVC5_EXPORT Solver * \verbatim embed:rst:inline :ref:`model-cores ` * \endverbatim has been set. * + * @warning This method is experimental and may change in future versions. + * * @param v The term in question * @return true if v is a model core symbol */ @@ -4154,6 +4176,8 @@ class CVC5_EXPORT Solver * :ref:`produce-models `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the @@ -4242,6 +4266,9 @@ class CVC5_EXPORT Solver * When using separation logic, this sets the location sort and the * datatype sort to the given ones. This method should be invoked exactly * once, before any separation logic constraints are provided. + * + * @warning This method is experimental and may change in future versions. + * * @param locSort The location sort of the heap * @param dataSort The data sort of the heap */ @@ -4249,12 +4276,18 @@ class CVC5_EXPORT Solver /** * When using separation logic, obtain the term for the heap. + * + * @warning This method is experimental and may change in future versions. + * * @return The term for the heap */ Term getValueSepHeap() const; /** * When using separation logic, obtain the term for nil. + * + * @warning This method is experimental and may change in future versions. + * * @return The term for nil */ Term getValueSepNil() const; @@ -4311,6 +4344,8 @@ class CVC5_EXPORT Solver * mode different from `none`. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj, @@ -4333,6 +4368,8 @@ class CVC5_EXPORT Solver * mode different from `none`. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param conj the conjecture term * @param grammar the grammar for the interpolant I * @return a Term I such that A->I and I->B are valid, where A is the @@ -4359,6 +4396,8 @@ class CVC5_EXPORT Solver * mode different from `none`. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @return a Term I such that A->I and I->B are valid, where A is the * current set of assertions and B is given in the input by conj * on the last call to getInterpolant. @@ -4379,6 +4418,8 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a term @f$C@f$ such that @f$(A \wedge C)@f$ is satisfiable, * and @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @@ -4402,6 +4443,9 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * + * * @param conj the conjecture term * @param grammar the grammar for the abduct @f$C@f$ * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and @@ -4427,6 +4471,8 @@ class CVC5_EXPORT Solver * :ref:`produce-abducts `. * \endverbatim * + * @warning This method is experimental and may change in future versions. + * * @return a term C such that @f$(A \wedge C)@f$ is satisfiable, and * @f$(A \wedge \neg B \wedge C)@f$ is unsatisfiable, where @f$A@f$ is * the current set of assertions and @f$B@f$ is given in the input by @@ -4452,6 +4498,8 @@ class CVC5_EXPORT Solver * :ref:`block-models `. * to a mode other than ``none``. * \endverbatim + * + * @warning This method is experimental and may change in future versions. */ void blockModel() const; @@ -4470,10 +4518,14 @@ class CVC5_EXPORT Solver * :ref:`produce-models `. * 'produce-models'. * \endverbatim + * + * @warning This method is experimental and may change in future versions. */ void blockModelValues(const std::vector& terms) const; /** + * @warning This method is experimental and may change in future versions. + * * @return a string that contains information about all instantiations made by * the quantifiers module. */ diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java index f824ac121..da30b3d4a 100644 --- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java +++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java @@ -75,6 +75,8 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable ) * } + * * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and * to mkUninterpretedSortConstructorSort() const if arity > 0. + * * @param symbol the name of the sort * @param arity the arity of the sort * @return the sort @@ -1769,6 +1779,9 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( get-learned-literals ) * } + * + * @apiNote This method is experimental and may change in future versions. + * * @return the list of learned literals */ public Term[] getLearnedLiterals() { @@ -1871,11 +1884,13 @@ public class Solver implements IPointer, AutoCloseable * (get-unsat-core) * } * Requires to enable option 'produce-unsat-cores'. + * * @apiNote In contrast to SMT-LIB, the API does not distinguish between * named and unnamed assertions when producing an unsatisfiable * core. Additionally, the API allows this option to be called after * a check with assumptions. A subset of those assumptions may be * included in the unsatisfiable core returned by this method. + * * @return a set of terms representing the unsatisfiable core */ public Term[] getUnsatCore() @@ -1916,6 +1931,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-proof ) * } * Requires to enable option 'produce-proofs'. + * + * @apiNote This method is experimental and may change in future versions. + * * @return a string representing the proof, according to the value of * proof-format-mode. */ @@ -1983,6 +2001,8 @@ public class Solver implements IPointer, AutoCloseable * current model. This method will only return false (for any v) if * the model-cores option has been set. * + * @apiNote This method is experimental and may change in future versions. + * * @param v The term in question * @return true if v is a model core symbol */ @@ -2000,6 +2020,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-model ) * } * Requires to enable option 'produce-models'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param sorts The list of uninterpreted sorts that should be printed in the * model. * @param vars The list of free constants that should be printed in the @@ -2079,6 +2102,9 @@ public class Solver implements IPointer, AutoCloseable * When using separation logic, this sets the location sort and the * datatype sort to the given ones. This method should be invoked exactly * once, before any separation logic constraints are provided. + * + * @apiNote This method is experimental and may change in future versions. + * * @param locSort The location sort of the heap * @param dataSort The data sort of the heap */ @@ -2091,6 +2117,9 @@ public class Solver implements IPointer, AutoCloseable /** * When using separation logic, obtain the term for the heap. + * + * @apiNote This method is experimental and may change in future versions. + * * @return The term for the heap */ public Term getValueSepHeap() @@ -2103,6 +2132,9 @@ public class Solver implements IPointer, AutoCloseable /** * When using separation logic, obtain the term for nil. + * + * @apiNote This method is experimental and may change in future versions. + * * @return The term for nil */ public Term getValueSepNil() @@ -2170,6 +2202,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-interpol ) * } * Requires 'produce-interpols' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a Term I such that {@code A->I} and {@code I->B} are valid, where * A is the current set of assertions and B is given in the input by @@ -2190,6 +2225,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-interpol ) * } * Requires 'produce-interpols' to be set to a mode different from 'none'. + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @param grammar the grammar for the interpolant I * @return a Term I such that {@code A->I} and {@code I->B} are valid, where @@ -2221,6 +2259,8 @@ public class Solver implements IPointer, AutoCloseable * set to a mode different from 'none'. * \endverbatim * + * @apiNote This method is experimental and may change in future versions. + * * @return a Term I such that {@code A->I} and {@code I->B} are valid, * where A is the current set of assertions and B is given in the input * by conj on the last call to getInterpolant, or the null term if such @@ -2241,6 +2281,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-abduct ) * } * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is @@ -2261,6 +2304,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-abduct ) * } * Requires enabling option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @param conj the conjecture term * @param grammar the grammar for the abduct C * @return a term C such that A^C is satisfiable, and A^~B^C is @@ -2285,6 +2331,9 @@ public class Solver implements IPointer, AutoCloseable * ( get-abduct-next ) * } * Requires enabling incremental mode and option 'produce-abducts' + * + * @apiNote This method is experimental and may change in future versions. + * * @return a term C such that A^C is satisfiable, and A^~B^C is * unsatisfiable, where A is the current set of assertions and B is * given in the input by conj in the last call to getAbduct, or the @@ -2307,6 +2356,8 @@ public class Solver implements IPointer, AutoCloseable * } * Requires enabling 'produce-models' option and setting 'block-models' option * to a mode other than "none". + * + * @apiNote This method is experimental and may change in future versions. */ public void blockModel() { @@ -2323,6 +2374,8 @@ public class Solver implements IPointer, AutoCloseable * ( block-model-values ( + ) ) * } * Requires enabling 'produce-models' option. + * + * @apiNote This method is experimental and may change in future versions. */ public void blockModelValues(Term[] terms) { @@ -2335,6 +2388,8 @@ public class Solver implements IPointer, AutoCloseable /** * Return a string that contains information about all instantiations made by * the quantifiers module. + * + * @apiNote This method is experimental and may change in future versions. */ public String getInstantiations() { diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index bf85107f6..458a60e68 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -373,7 +373,11 @@ public class Sort extends AbstractPointer implements Comparable /** * Instantiate a parameterized datatype sort or uninterpreted sort * constructor sort. + * * Create sorts parameter with Solver.mkParamSort(). + * + * @apiNote This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ public Sort instantiate(List params) @@ -382,8 +386,13 @@ public class Sort extends AbstractPointer implements Comparable } /** - * Instantiate a parameterized datatype/sort sort. + * Instantiate a parameterized datatype sort or uninterpreted sort + * constructor sort. + * * Create sorts parameter with Solver.mkParamSort(). + * + * @apiNote This method is experimental and may change in future versions. + * * @param params the list of sort parameters to instantiate with */ public Sort instantiate(Sort[] params) @@ -397,11 +406,14 @@ public class Sort extends AbstractPointer implements Comparable /** * Substitution of Sorts. - * @param sort the subsort to be substituted within this sort. - * @param replacement the sort replacing the substituted subsort. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. + * + * @apiNote This method is experimental and may change in future versions. + * + * @param sort the subsort to be substituted within this sort. + * @param replacement the sort replacing the substituted subsort. */ public Sort substitute(Sort sort, Sort replacement) { @@ -413,8 +425,6 @@ public class Sort extends AbstractPointer implements Comparable /** * Simultaneous substitution of Sorts. - * @param sorts the subsorts to be substituted within this sort. - * @param replacements the sort replacing the substituted subsorts. * * Note that this replacement is applied during a pre-order traversal and * only once to the sort. It is not run until fix point. In the case that @@ -424,6 +434,11 @@ public class Sort extends AbstractPointer implements Comparable * For example, * (Array A B).substitute({A, C}, {(Array C D), (Array A B)}) will * return (Array (Array C D) B). + * + * @apiNote This method is experimental and may change in future versions. + * + * @param sorts the subsorts to be substituted within this sort. + * @param replacements the sort replacing the substituted subsorts. */ public Sort substitute(Sort[] sorts, Sort[] replacements) { diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 09749b3d5..afbdb8f26 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -255,6 +255,9 @@ cdef class DatatypeConstructor: :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm() `). + .. warning:: This method is experimental and may change in future + versions. + :param retSort: the desired return sort of the constructor :return: the constructor operator as a term. """ @@ -1218,6 +1221,9 @@ cdef class Solver: def mkSepEmp(self): """Create a separation logic empty term. + .. warning:: This method is experimental and may change in future + versions. + :return: the separation logic empty term """ cdef Term term = Term(self) @@ -1227,6 +1233,9 @@ cdef class Solver: def mkSepNil(self, Sort sort): """Create a separation logic nil term. + .. warning:: This method is experimental and may change in future + versions. + :param sort: the sort of the nil term :return: the separation logic nil term """ @@ -1963,6 +1972,9 @@ cdef class Solver: Requires to enable option :ref:`produce-proofs `. + .. warning:: This method is experimental and may change in future + versions. + :return: a string representing the proof, according to the value of proof-format-mode. """ @@ -1977,6 +1989,9 @@ cdef class Solver: ( get-learned-literals ) + .. warning:: This method is experimental and may change in future + versions. + :return: the list of literals """ lits = [] @@ -2198,6 +2213,9 @@ cdef class Solver: using the current model. This method will only return false (for any v) if the model-cores option has been set. + .. warning:: This method is experimental and may change in future + versions. + :param v: The term in question :return: true if v is a model core symbol """ @@ -2214,6 +2232,9 @@ cdef class Solver: Requires to enable option :ref:`produce-models `. + + .. warning:: This method is experimental and may change in future + versions. :param sorts: The list of uninterpreted sorts that should be printed in the model. @@ -2257,6 +2278,9 @@ cdef class Solver: datatype sort to the given ones. This method should be invoked exactly once, before any separation logic constraints are provided. + .. warning:: This method is experimental and may change in future + versions. + :param locSort: The location sort of the heap :param dataSort: The data sort of the heap """ @@ -2271,6 +2295,9 @@ cdef class Solver: ( declare-pool ( * ) ) + .. warning:: This method is experimental and may change in future + versions. + :param symbol: The name of the pool :param sort: The sort of the elements of the pool. :param initValue: The initial value of the pool @@ -2379,6 +2406,9 @@ cdef class Solver: - ``Term getInteprolant(Term conj)`` - ``Term getInteprolant(Term conj, Grammar grammar)`` + + .. warning:: This method is experimental and may change in future + versions. :param conj: the conjecture term :param output: the term where the result will be stored @@ -2411,6 +2441,9 @@ cdef class Solver: Requires to enable incremental mode, and option :ref:`produce-interpols ` to be set to a mode different from `none`. + .. warning:: This method is experimental and may change in future + versions. + :param output: the term where the result will be stored :return: True iff an interpolant was found """ @@ -2434,6 +2467,9 @@ cdef class Solver: - ``Term getAbduct(Term conj)`` - ``Term getAbduct(Term conj, Grammar grammar)`` + + .. warning:: This method is experimental and may change in future + versions. :param conj: the conjecture term :param output: the term where the result will be stored @@ -2464,6 +2500,10 @@ cdef class Solver: Requires to enable incremental mode, and option :ref:`produce-abducts `. + + .. warning:: This method is experimental and may change in future + versions. + :param output: the term where the result will be stored :return: True iff an abduct was found """ @@ -2487,6 +2527,9 @@ cdef class Solver: and setting option :ref:`block-models ` to a mode other than ``none``. + + .. warning:: This method is experimental and may change in future + versions. """ self.csolver.blockModel() @@ -2503,6 +2546,9 @@ cdef class Solver: Requires enabling option :ref:`produce-models `. + + .. warning:: This method is experimental and may change in future + versions. """ cdef vector[c_Term] nts for t in terms: @@ -2513,6 +2559,9 @@ cdef class Solver: """ Return a string that contains information about all instantiations made by the quantifiers module. + + .. warning:: This method is experimental and may change in future + versions. """ return self.csolver.getInstantiations() @@ -2783,6 +2832,9 @@ cdef class Sort: constructor sort. Create sorts parameter with :py:meth:`Solver.mkParamSort()` + .. warning:: This method is experimental and may change in future + versions. + :param params: the list of sort parameters to instantiate with """ cdef Sort sort = Sort(self.solver) @@ -2796,9 +2848,6 @@ cdef class Sort: """ Substitution of Sorts. - :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. - :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. - Note that this replacement is applied during a pre-order traversal and only once to the sort. It is not run until fix point. In the case that sort_or_list_1 contains duplicates, the replacement earliest in the list @@ -2807,6 +2856,12 @@ cdef class Sort: For example, ``(Array A B) .substitute([A, C], [(Array C D), (Array A B)])`` will return ``(Array (Array C D) B)``. + + .. warning:: This method is experimental and may change in future + versions. + + :param sort_or_list_1: the subsort or subsorts to be substituted within this sort. + :param sort_or_list_2: the sort or list of sorts replacing the substituted subsort. """ # The resulting sort after substitution -- 2.30.2