[API] Mark methods as experimental (#8249)
authorAndres Noetzli <andres.noetzli@gmail.com>
Mon, 28 Mar 2022 21:23:21 +0000 (14:23 -0700)
committerGitHub <noreply@github.com>
Mon, 28 Mar 2022 21:23:21 +0000 (21:23 +0000)
src/api/cpp/cvc5.h
src/api/java/io/github/cvc5/api/DatatypeConstructor.java
src/api/java/io/github/cvc5/api/Solver.java
src/api/java/io/github/cvc5/api/Sort.java
src/api/python/cvc5.pxi

index eb99763619638864670103ccc681d50d713cc0cc..4e8287fa888d06aad483479e50b04f21a4731ec1 100644 (file)
@@ -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<Sort>& 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<Sort>& sorts,
                   const std::vector<Sort>& 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 <lbl-option-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<Term> getLearnedLiterals() const;
 
@@ -4135,6 +4155,8 @@ class CVC5_EXPORT Solver
    * \verbatim embed:rst:inline :ref:`model-cores <lbl-option-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 <lbl-option-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 <lbl-option-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 <lbl-option-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 <lbl-option-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 <lbl-option-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 <lbl-option-produce-models>`.
    * 'produce-models'.
    * \endverbatim
+   *
+   * @warning This method is experimental and may change in future versions.
    */
   void blockModelValues(const std::vector<Term>& 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.
    */
index f824ac121f23b2b43379bf7cb5b91559d1ccb94b..da30b3d4a173d0b0633e20c4310ced3006b2a9e9 100644 (file)
@@ -75,6 +75,8 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
    * while Solver::mkTerm(APPLY_CONSTRUCTOR, t) is used to construct the above
    * (nullary) application of nil.
    *
+   * @apiNote This method is experimental and may change in future versions.
+   *
    * @param retSort the desired return sort of the constructor
    * @return the constructor term
    */
index 5b462bc2f18c64da83691d8cf68e5643590e6ba3..a9c270536cd8680d4851d62057ac31158433e56a 100644 (file)
@@ -689,8 +689,10 @@ public class Solver implements IPointer, AutoCloseable
    * Create an operator for a builtin Kind
    * The Kind may not be the Kind for an indexed operator
    *   (e.g. BITVECTOR_EXTRACT).
+   *
    * @apiNote In this case, the Op simply wraps the Kind. The Kind can be used
    *          in mkTerm directly without creating an op first.
+   *
    * @param kind the kind to wrap
    */
   public Op mkOp(Kind kind)
@@ -965,6 +967,9 @@ public class Solver implements IPointer, AutoCloseable
 
   /**
    * Create a separation logic empty term.
+   *
+   * @apiNote This method is experimental and may change in future versions.
+   *
    * @return the separation logic empty term
    */
   public Term mkSepEmp()
@@ -977,6 +982,9 @@ public class Solver implements IPointer, AutoCloseable
 
   /**
    * Create a separation logic nil term.
+   *
+   * @apiNote This method is experimental and may change in future versions.
+   *
    * @param sort the sort of the nil term
    * @return the separation logic nil term
    */
@@ -1559,8 +1567,10 @@ public class Solver implements IPointer, AutoCloseable
    * {@code
    *   ( declare-sort <symbol> <numeral> )
    * }
+   *
    * @apiNote This corresponds to mkUninterpretedSort() const if arity = 0, and
    *          to mkUninterpretedSortConstructorSort() const if arity &gt; 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 <conj> )
    * }
    * 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 <conj> <g> )
    * }
    * 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 <conj> )
    * }
    * 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 <conj> <g> )
    * }
    * 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 ( <terms>+ ) )
    * }
    * 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()
   {
index bf85107f66131068a9f16718ebb2bd03acee8270..458a60e6869d8190a9e051ae97d400ee56c959bc 100644 (file)
@@ -373,7 +373,11 @@ public class Sort extends AbstractPointer implements Comparable<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(List<Sort> params)
@@ -382,8 +386,13 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   }
 
   /**
-   * 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<Sort>
 
   /**
    * 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<Sort>
 
   /**
    * 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<Sort>
    * 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)
   {
index 09749b3d532f13d83d938ac925cf6308cb0380b3..afbdb8f26a72ac8e8604b8735a4586abd99b5e38 100644 (file)
@@ -255,6 +255,9 @@ cdef class DatatypeConstructor:
             :cpp:func:`DatatypeConstructor::getInstantiatedConstructorTerm()
             <cvc5::api::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 <lbl-option-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 <lbl-option-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 <symbol> <sort> ( <term>* ) )
 
+        .. 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 <lbl-option-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 <lbl-option-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 <lbl-option-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 <lbl-option-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