*
* 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.
* 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;
* `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
*/
/**
* 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
*/
* :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;
* \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
*/
* :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
* 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
*/
/**
* 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;
* 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,
* 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
* 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.
* :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
* :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
* :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
* :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;
* :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.
*/
* 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
*/
* 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)
/**
* 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()
/**
* 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
*/
* {@code
* ( declare-sort <symbol> <numeral> )
* }
+ *
* @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
* {@code
* ( get-learned-literals )
* }
+ *
+ * @apiNote This method is experimental and may change in future versions.
+ *
* @return the list of learned literals
*/
public Term[] getLearnedLiterals() {
* (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()
* ( 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.
*/
* 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
*/
* ( 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
* 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
*/
/**
* 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()
/**
* 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()
* ( 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
* ( 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
* 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
* ( 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
* ( 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
* ( 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
* }
* 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()
{
* ( 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)
{
/**
* 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()
{
/**
* 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)
}
/**
- * 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)
/**
* 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)
{
/**
* 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
* 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)
{
: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.
"""
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)
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
"""
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.
"""
( get-learned-literals )
+ .. warning:: This method is experimental and may change in future
+ versions.
+
:return: the list of literals
"""
lits = []
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
"""
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.
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
"""
( 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
- ``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
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
"""
- ``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
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
"""
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()
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:
"""
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()
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)
"""
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
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