From: Andrew Reynolds Date: Mon, 28 Mar 2022 23:09:43 +0000 (-0500) Subject: Mark more methods as experimental (#8426) X-Git-Tag: cvc5-1.0.0~147 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=1fa8c5bd361c1c950127779cc364fa82c25477da;p=cvc5.git Mark more methods as experimental (#8426) --- diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h index bf785793f..4e9db9364 100644 --- a/src/api/cpp/cvc5.h +++ b/src/api/cpp/cvc5.h @@ -549,6 +549,7 @@ class CVC5_EXPORT Sort /** * Is this a record sort? + * @warning This method is experimental and may change in future versions. * @return true if the sort is a record sort */ bool isRecord() const; @@ -2303,12 +2304,17 @@ class CVC5_EXPORT Datatype size_t getNumConstructors() const; /** + * @warning This method is experimental and may change in future versions. + * * @return the parameters of this datatype, if it is parametric. An exception * is thrown if this datatype is not parametric. */ std::vector getParameters() const; - /** @return true if this datatype is parametric */ + /** + * @warning This method is experimental and may change in future versions. + * @return true if this datatype is parametric + */ bool isParametric() const; /** @return true if this datatype corresponds to a co-datatype */ @@ -2317,7 +2323,10 @@ class CVC5_EXPORT Datatype /** @return true if this datatype corresponds to a tuple */ bool isTuple() const; - /** @return true if this datatype corresponds to a record */ + /** + * @warning This method is experimental and may change in future versions. + * @return true if this datatype corresponds to a record + */ bool isRecord() const; /** @return true if this datatype is finite */ @@ -3233,6 +3242,9 @@ class CVC5_EXPORT Solver /** * Create a sort parameter. + * + * @warning This method is experimental and may change in future versions. + * * @param symbol the name of the sort * @return the sort parameter */ @@ -3247,6 +3259,9 @@ class CVC5_EXPORT Solver /** * Create a record sort + * + * @warning This method is experimental and may change in future versions. + * * @param fields the list of fields of the record * @return the record sort */ @@ -3629,6 +3644,9 @@ class CVC5_EXPORT Solver /** * Create a cardinality constraint for an uninterpreted sort. + * + * @warning This method is experimental and may change in future versions. + * * @param sort the sort the cardinality constraint is for * @param upperBound the upper bound on the cardinality of the sort * @return the cardinality constraint @@ -3678,6 +3696,11 @@ class CVC5_EXPORT Solver /* Create datatype constructor declarations */ /* .................................................................... */ + /** + * Create a datatype constructor declaration. + * @param name the name of the datatype constructor + * @return the DatatypeConstructorDecl + */ DatatypeConstructorDecl mkDatatypeConstructorDecl(const std::string& name); /* .................................................................... */ @@ -3726,6 +3749,9 @@ class CVC5_EXPORT Solver * the SAT Engine in the simplification, but uses the current * definitions, assertions, and the current partial model, if one * has been constructed. It also involves theory normalization. + * + * @warning This method is experimental and may change in future versions. + * * @param t the formula to simplify * @return the simplified formula */ @@ -4068,6 +4094,8 @@ class CVC5_EXPORT Solver * Get a difficulty estimate for an asserted formula. This method is * intended to be called immediately after any response to a checkSat. * + * @warning This method is experimental and may change in future versions. + * * @return a map from (a subset of) the input assertions to a real value that * is an estimate of how difficult each assertion was to solve. * Unmentioned assertions can be assumed to have zero difficulty. @@ -4198,10 +4226,10 @@ class CVC5_EXPORT Solver * (get-qe ) * \endverbatim * - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * @note Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. * - * @note Quantifier Elimination is is only complete for LRA and LIA. + * @warning This method is experimental and may change in future versions. * * @param q a quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ @@ -4229,8 +4257,11 @@ class CVC5_EXPORT Solver * (get-qe-disjunct ) * \endverbatim * - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * @note Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @warning This method is experimental and may change in future versions. + * * @param q a quantified formula of the form * @f$Q\bar{x}_1... Q\bar{x}_n. P( x_1...x_i, y_1...y_j)@f$ * where @@ -4306,6 +4337,8 @@ class CVC5_EXPORT Solver * (declare-pool ( * )) * \endverbatim * + * @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 @@ -4609,6 +4642,9 @@ class CVC5_EXPORT Solver * * @note The sort of the term must be convertible into the target sort. * Currently only Int to Real conversions are supported. + * + * @warning This method is experimental and may change in future versions. + * * @param t the term * @param s the target sort * @return the term wrapped into a sort conversion if needed diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java index f2e260eae..f4b73e1f4 100644 --- a/src/api/java/io/github/cvc5/api/Datatype.java +++ b/src/api/java/io/github/cvc5/api/Datatype.java @@ -111,6 +111,8 @@ public class Datatype extends AbstractPointer implements Iterable ) - * } - * @param out the output stream - * @param str the string to echo - */ - // TODO: void echo(std::ostream& out, String str) - /** * Get a list of literals that are entailed by the current set of assertions * SMT-LIB: @@ -1905,6 +1911,8 @@ public class Solver implements IPointer, AutoCloseable * Get a difficulty estimate for an asserted formula. This method is * intended to be called immediately after any response to a checkSat. * + * @apiNote This method is experimental and may change in future versions. + * * @return a map from (a subset of) the input assertions to a real value that * is an estimate of how difficult each assertion was to solve. Unmentioned * assertions can be assumed to have zero difficulty. @@ -2044,8 +2052,11 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( get-qe ) * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) * where P( x1...xn, y1...yn ) is a quantifier-free formula @@ -2070,8 +2081,11 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( get-qe-disjunct ) * } - * Requires a logic that supports quantifier elimination. Currently, the only - * logics supported by quantifier elimination is LRA and LIA. + * Quantifier Elimination is is only complete for logics such as LRA, + * LIA and BV. + * + * @apiNote This method is experimental and may change in future versions. + * * @param q a quantified formula of the form: * Q x1...xn. P( x1...xn, y1...yn ) * where P( x1...xn, y1...yn ) is a quantifier-free formula @@ -2151,6 +2165,9 @@ public class Solver implements IPointer, AutoCloseable * {@code * ( declare-pool ( * ) ) * } + * + * @apiNote 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 @@ -2496,6 +2513,9 @@ public class Solver implements IPointer, AutoCloseable * * @apiNote The sort of the term must be convertible into the target sort. * Currently only Int to Real conversions are supported. + * + * @apiNote This method is experimental and may change in future versions. + * * @param t the term * @param s the target sort * @return the term wrapped into a sort conversion if needed diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java index 458a60e68..ba97057e4 100644 --- a/src/api/java/io/github/cvc5/api/Sort.java +++ b/src/api/java/io/github/cvc5/api/Sort.java @@ -280,6 +280,9 @@ public class Sort extends AbstractPointer implements Comparable /** * Is this a record sort? + * + * @apiNote This method is experimental and may change in future versions. + * * @return true if the sort is a record sort */ public boolean isRecord() diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi index 10d714b92..fc24f32a2 100644 --- a/src/api/python/cvc5.pxi +++ b/src/api/python/cvc5.pxi @@ -174,7 +174,11 @@ cdef class Datatype: return param_sorts def isParametric(self): - """:return: True if this datatype is parametric.""" + """ + .. warning:: This method is experimental and may change in future + versions. + :return: True if this datatype is parametric. + """ return self.cd.isParametric() def isCodatatype(self): @@ -186,7 +190,11 @@ cdef class Datatype: return self.cd.isTuple() def isRecord(self): - """:return: True if this datatype corresponds to a record.""" + """ + .. warning:: This method is experimental and may change in future + versions. + :return: True if this datatype corresponds to a record. + """ return self.cd.isRecord() def isFinite(self): @@ -897,6 +905,9 @@ cdef class Solver: def mkParamSort(self, symbolname): """ Create a sort parameter. + .. warning:: This method is experimental and may change in future + versions. + :param symbol: the name of the sort :return: the sort parameter """ @@ -922,6 +933,9 @@ cdef class Solver: def mkRecordSort(self, *fields): """Create a record sort + .. warning:: This method is experimental and may change in future + versions. + :param fields: the list of fields of the record, as a list or as distinct arguments :return: the record sort """ @@ -1424,6 +1438,9 @@ cdef class Solver: def mkCardinalityConstraint(self, Sort sort, int index): """Create cardinality constraint. + .. warning:: This method is experimental and may change in future + versions. + :param sort: Sort of the constraint :param index: The upper bound for the cardinality of the sort """ @@ -1473,8 +1490,8 @@ cdef class Solver: def mkDatatypeConstructorDecl(self, str name): """ - :return: a datatype constructor declaration :param name: the constructor's name + :return: the DatatypeConstructorDecl """ cdef DatatypeConstructorDecl ddc = DatatypeConstructorDecl(self) ddc.cddc = self.csolver.mkDatatypeConstructorDecl(name.encode()) @@ -1537,6 +1554,9 @@ cdef class Solver: assertions, and the current partial model, if one has been constructed. It also involves theory normalization. + .. warning:: This method is experimental and may change in future + versions. + :param t: the formula to simplify :return: the simplified formula """ @@ -2257,6 +2277,9 @@ cdef class Solver: def getValueSepHeap(self): """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 """ cdef Term term = Term(self) @@ -2266,6 +2289,9 @@ cdef class Solver: def getValueSepNil(self): """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 """ cdef Term term = Term(self) @@ -2763,6 +2789,9 @@ cdef class Sort: """ Is this a record sort? + .. warning:: This method is experimental and may change in future + versions. + :return: True if the sort is a record sort. """ return self.csort.isRecord()