From: Haniel Barbosa <hanielbbarbosa@gmail.com>
Date: Wed, 4 Aug 2021 15:28:12 +0000 (-0300)
Subject: [proof] Add getProof to API and use it in GetProofCommand (#6974)
X-Git-Tag: cvc5-1.0.0~1414
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=5f89c684f95f16bdb5953fc543a36115093f1982;p=cvc5.git

[proof] Add getProof to API and use it in GetProofCommand (#6974)

Also adds a call to get proof in a unit test.
---

diff --git a/src/api/cpp/cvc5.cpp b/src/api/cpp/cvc5.cpp
index 22690fe49..05f8bd073 100644
--- a/src/api/cpp/cvc5.cpp
+++ b/src/api/cpp/cvc5.cpp
@@ -7099,6 +7099,18 @@ std::vector<Term> Solver::getUnsatCore(void) const
   CVC5_API_TRY_CATCH_END;
 }
 
+std::string Solver::getProof(void) const
+{
+  CVC5_API_TRY_CATCH_BEGIN;
+  NodeManagerScope scope(getNodeManager());
+  CVC5_API_CHECK(d_smtEngine->getOptions().smt.produceProofs)
+      << "Cannot get proof explicitly enabled (try --prooduce-proofs)";
+  CVC5_API_RECOVERABLE_CHECK(d_smtEngine->getSmtMode() == SmtMode::UNSAT)
+      << "Cannot get proof unless in unsat mode.";
+  return d_smtEngine->getProof();
+  CVC5_API_TRY_CATCH_END;
+}
+
 Term Solver::getValue(const Term& term) const
 {
   CVC5_API_TRY_CATCH_BEGIN;
diff --git a/src/api/cpp/cvc5.h b/src/api/cpp/cvc5.h
index e41df9593..3b6ba7069 100644
--- a/src/api/cpp/cvc5.h
+++ b/src/api/cpp/cvc5.h
@@ -3740,6 +3740,18 @@ class CVC5_EXPORT Solver
    */
   std::vector<Term> getUnsatCore() const;
 
+  /**
+   * Get the refutation proof
+   * SMT-LIB:
+   * \verbatim
+   * ( get-proof )
+   * \endverbatim
+   * Requires to enable option 'produce-proofs'.
+   * @return a string representing the proof, according to the the value of
+   * proof-format-mode.
+   */
+  std::string getProof() const;
+
   /**
    * Get the value of the given term.
    * SMT-LIB:
diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index 36bc17096..342931912 100644
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1993,7 +1993,7 @@ void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
   try
   {
-    d_result = solver->getSmtEngine()->getProof();
+    d_result = solver->getProof();
     d_commandStatus = CommandSuccess::instance();
   }
   catch (api::CVC5ApiRecoverableException& e)
diff --git a/test/unit/api/solver_black.cpp b/test/unit/api/solver_black.cpp
index 20e0977f8..ce989c9ea 100644
--- a/test/unit/api/solver_black.cpp
+++ b/test/unit/api/solver_black.cpp
@@ -1343,10 +1343,11 @@ TEST_F(TestApiBlackSolver, getUnsatCore2)
   ASSERT_THROW(d_solver.getUnsatCore(), CVC5ApiException);
 }
 
-TEST_F(TestApiBlackSolver, getUnsatCore3)
+TEST_F(TestApiBlackSolver, getUnsatCoreAndProof)
 {
   d_solver.setOption("incremental", "true");
   d_solver.setOption("produce-unsat-cores", "true");
+  d_solver.setOption("produce-proofs", "true");
 
   Sort uSort = d_solver.mkUninterpretedSort("u");
   Sort intSort = d_solver.getIntegerSort();
@@ -1375,6 +1376,8 @@ TEST_F(TestApiBlackSolver, getUnsatCore3)
 
   ASSERT_NO_THROW(unsat_core = d_solver.getUnsatCore());
 
+  ASSERT_NO_THROW(d_solver.getProof());
+
   d_solver.resetAssertions();
   for (const auto& t : unsat_core)
   {
@@ -1382,6 +1385,7 @@ TEST_F(TestApiBlackSolver, getUnsatCore3)
   }
   cvc5::api::Result res = d_solver.checkSat();
   ASSERT_TRUE(res.isUnsat());
+  ASSERT_NO_THROW(d_solver.getProof());
 }
 
 TEST_F(TestApiBlackSolver, getValue1)