[API/Python] Add support for `Solver::getProof()` (#8259)

This commit implements support for Solver::getProof() in the Python
API, which was missing before.

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 0950283655033392408d5a50b694f35939d31a0d..392e7b412c6d2e990862f8b7fc0f4a0f523a1089 100644 (file)
--- a/src/api/python/cvc5.pxd
+++ b/src/api/python/cvc5.pxd
@@ -273,6 +273,7 @@ cdef extern from "api/cpp/cvc5.h" namespace "cvc5::api":
                           Term term, bint glbl) except +
         Term defineFunsRec(vector[Term]& funs, vector[vector[Term]]& bound_vars,
                            vector[Term]& terms, bint glbl) except +
+        string getProof() except +
         vector[Term] getLearnedLiterals() except +
         vector[Term] getAssertions() except +
         string getInfo(const string& flag) except +

diff --git a/src/api/python/cvc5.pxi b/src/api/python/cvc5.pxi
index f0a2d361732d42b4eb8c2f40850f4f9f7ec17681..46703d36fb872188371fbcdc84cc9d67d576c62f 100644 (file)
--- a/src/api/python/cvc5.pxi
+++ b/src/api/python/cvc5.pxi
@@ -1943,6 +1943,23 @@ cdef class Solver:
         for t in terms:
             vf.push_back((<Term?> t).cterm)
 
+    def getProof(self):
+        """Get the refutation proof
+
+        SMT-LIB:
+
+        .. code-block:: smtlib
+        
+           (get-proof)
+
+        Requires to enable option
+        :ref:`produce-proofs <lbl-option-produce-proofs>`.
+
+        :return: a string representing the proof, according to the value of
+                 proof-format-mode.
+        """
+        return self.csolver.getProof()
+
     def getLearnedLiterals(self):
         """Get a list of literals that are entailed by the current set of assertions
 

diff --git a/test/unit/api/python/test_solver.py b/test/unit/api/python/test_solver.py
index 24f180c7b4ffc2ab87e7b4900e69dc9ac15bfdb7..69b08e092ca358173f8bce4677a8eade8c3b110a 100644 (file)
--- a/test/unit/api/python/test_solver.py
+++ b/test/unit/api/python/test_solver.py
@@ -1223,9 +1223,10 @@ def test_get_unsat_core2(solver):
         solver.getUnsatCore()
 
 
-def test_get_unsat_core3(solver):
+def test_get_unsat_core_and_proof(solver):
     solver.setOption("incremental", "true")
     solver.setOption("produce-unsat-cores", "true")
+    solver.setOption("produce-proofs", "true");
 
     uSort = solver.mkUninterpretedSort("u")
     intSort = solver.getIntegerSort()
@@ -1258,6 +1259,7 @@ def test_get_unsat_core3(solver):
         solver.assertFormula(t)
     res = solver.checkSat()
     assert res.isUnsat()
+    solver.getProof()
 
 def test_learned_literals(solver):
     solver.setOption("produce-learned-literals", "true")