From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Fri, 25 Feb 2022 00:32:18 +0000 (-0800)
Subject: [Python API] Add support for blocking models (#8134)
X-Git-Tag: cvc5-1.0.0~382
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e06dd209a23e4667b5e5202d48d7706f0942bca4;p=cvc5.git

[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 bf988dda0..357d5d149 100644
--- 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 65c17b416..03bb2c9d3 100644
--- 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 d0e2094f9..9b89f7187 100644
--- 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):