+ def getInterpolant(self, Term conj, Grammar grammar=None):
+ """
+ Get an interpolant.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-interpolant <conj> )
+ ( get-interpolant <conj> <grammar> )
+
+ Requires option :ref:`produce-interpolants
+ <lbl-option-produce-interpolants>` to be set to a mode different
+ from `none`.
+
+ .. warning:: This method is experimental and may change in future
+ versions.
+ :param conj: The conjecture term.
+ :param grammar: A grammar for the inteprolant.
+ :return: The interpolant.
+ See :cpp:func:`cvc5::Solver::getInterpolant` for details.
+ """
+ cdef Term result = Term(self)
+ if grammar is None:
+ result.cterm = self.csolver.getInterpolant(conj.cterm)
+ else:
+ result.cterm = self.csolver.getInterpolant(conj.cterm, grammar.cgrammar)
+ return result
+
+
+ def getInterpolantNext(self):
+ """
+ Get the next interpolant. Can only be called immediately after
+ a successful call to :py:func:`Solver.getInterpolant()` or
+ :py:func:`Solver.getInterpolantNext()`.
+ Is guaranteed to produce a syntactically different interpolant wrt
+ the last returned interpolant if successful.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-interpolant-next )
+
+ Requires to enable incremental mode, and option
+ :ref:`produce-interpolants <lbl-option-produce-interpolants>` 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.
+ """
+ cdef Term result = Term(self)
+ result.cterm = self.csolver.getInterpolantNext()
+ return result
+ def getAbduct(self, Term conj, Grammar grammar=None):
+ """
+ Get an abduct.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-abduct <conj> )
+ ( get-abduct <conj> <grammar> )
+
+ Requires to enable option :ref:`produce-abducts
+ <lbl-option-produce-abducts>`.
+
+ .. warning:: This method is experimental and may change in future
+ versions.
+ :param conj: The conjecture term.
+ :param grammar: A grammar for the abduct.
+ :return: The abduct.
+ See :cpp:func:`cvc5::Solver::getAbduct` for details.
+ """
+ cdef Term result = Term(self)
+ if grammar is None:
+ result.cterm = self.csolver.getAbduct(conj.cterm)
+ else:
+ result.cterm = self.csolver.getAbduct(conj.cterm, grammar.cgrammar)
+ return result
+
+ def getAbductNext(self):
+ """
+ Get the next abduct. Can only be called immediately after
+ a succesful call to :py:func:`Solver.getAbduct()` or
+ :py:func:`Solver.getAbductNext()`.
+ Is guaranteed to produce a syntactically different abduct wrt the
+ last returned abduct if successful.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ ( get-abduct-next )
+
+ 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.
+ """
+ cdef Term result = Term(self)
+ result.cterm = self.csolver.getAbductNext()
+ return result
+
+ def blockModel(self, mode):
+ """
+ Block the current model. Can be called only if immediately preceded
+ by a SAT or INVALID query.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ (block-model)
+
+ Requires enabling option
+ :ref:`produce-models <lbl-option-produce-models>`
+ 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.
+
+ :param mode: The mode to use for blocking
+ """
+ self.csolver.blockModel(<c_BlockModelsMode> mode.value)
+
+ def blockModelValues(self, terms):
+ """
+ Block the current model values of (at least) the values in terms.
+ Can be called only if immediately preceded by a SAT or NOT_ENTAILED
+ query.
+
+ SMT-LIB:
+
+ .. code-block:: smtlib
+
+ (block-model-values ( <terms>+ ))
+
+ 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:
+ nts.push_back((<Term?> t).cterm)
+ self.csolver.blockModelValues(nts)
+
+ def getInstantiations(self):
+ """
+ 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()
+
+ def getStatistics(self):
+ """
+ Returns a snapshot of the current state of the statistic values of
+ this solver. The returned object is completely decoupled from the
+ solver and will not change when the solver is used again.
+ """
+ res = Statistics()
+ res.cstats = self.csolver.getStatistics()
+ return res
+
+