[Python API] Add support for blocking models (#8134)

The methods for blocking models were missing in the Python API. This
commit adds the blockModel() and blockModelValues() methods as well
as the corresponding tests.

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index bf988dda069b959f3cc43bf05d550e839e434b84..357d5d14941dc7464f091327b2f2a4ddf350c2be 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -299,6 +299,8 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
         bint getAbduct(const Term& conj, Term& output) except +
         bint getAbduct(const Term& conj, Grammar& grammar, Term& output) except +
         bint getAbductNext(const Term& conj) except +
+        void blockModel() except +
+        void blockModelValues(const vector[Term]& terms) except +
 
     cdef cppclass Grammar:
         Grammar() except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index 65c17b416a7d4d4c7acf9b4c3180b83c8b51f320..03bb2c9d38deef0bf813468f66f0b59b6eaac89a 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -2315,6 +2315,43 @@ cdef class Solver:
         result = self.csolver.getAbductNext(output.cterm)
         return result
 
+    def blockModel(self):
+        """
+        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``.
+        """
+        self.csolver.blockModel()
+
+    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>`.
+        """
+        cdef vector[c_Term] nts
+        for t in terms:
+            nts.push_back((<Term?> t).cterm)
+        self.csolver.blockModelValues(nts)
 
 
 cdef class Sort:

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index d0e2094f975acde58b97c14f7651ea69dc21f5d4..9b89f71875c6681028d0dae7607b618c0769910c 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1473,6 +1473,81 @@ def test_pop3(solver):
     with pytest.raises(RuntimeError):
         solver.pop(1)
 
+def test_block_model1(solver):
+    solver.setOption("produce-models", "true")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.blockModel()
+
+def test_block_model2(solver):
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.blockModel()
+
+def test_block_model3(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    with pytest.raises(RuntimeError):
+        solver.blockModel()
+
+def test_block_model4(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x");
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    solver.blockModel()
+
+def test_block_model_values1(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x");
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.blockModelValues([])
+    with pytest.raises(RuntimeError):
+        solver.blockModelValues([cvc5.Term(solver)])
+    with pytest.raises(RuntimeError):
+        solver.blockModelValues([cvc5.Solver().mkBoolean(False)])
+
+def test_block_model_values2(solver):
+    solver.setOption("produce-models", "true")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    solver.blockModelValues([x])
+
+def test_block_model_values3(solver):
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    with pytest.raises(RuntimeError):
+        solver.blockModelValues([x])
+
+def test_block_model_values4(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    with pytest.raises(RuntimeError):
+        solver.blockModelValues([x])
+
+def test_block_model_values5(solver):
+    solver.setOption("produce-models", "true")
+    solver.setOption("block-models", "literals")
+    x = solver.mkConst(solver.getBooleanSort(), "x")
+    solver.assertFormula(x.eqTerm(x))
+    solver.checkSat()
+    solver.blockModelValues([x])
 
 def test_set_info(solver):
     with pytest.raises(RuntimeError):