From 72e997f13bc2e89d1c9b1c6b59d4e57a0cfcc0d1 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Tue, 8 Mar 2022 14:02:50 -0800
Subject: [PATCH] [API/Python] Add support for `Solver::getProof()` (#8259)

This commit implements support for Solver::getProof() in the Python
API, which was missing before.
---
 src/api/python/cvc5.pxd             |  1 +
 src/api/python/cvc5.pxi             | 17 +++++++++++++++++
 test/unit/api/python/test_solver.py |  4 +++-
 3 files changed, 21 insertions(+), 1 deletion(-)

diff --git a/src/api/python/cvc5.pxd b/src/api/python/cvc5.pxd
index 095028365..392e7b412 100644
--- 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 f0a2d3617..46703d36f 100644
--- 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 24f180c7b..69b08e092 100644
--- 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")
-- 
2.30.2