[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 22690fe49a1bb2abb3eb0e42cab71acf4aae4fb4..05f8bd07377f73b28bb848f5e0ca4d9f05bbcfa0 100644 (file)
--- 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 e41df9593e4394b33a9779778fe81f12c4526176..3b6ba7069750d2180955dc68564fef6b036e084e 100644 (file)
--- 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 36bc170965ec704d850d0501229888044d5a8086..342931912493721c08de1e7ec670719bbc7ebb72 100644 (file)
--- 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 20e0977f8d1aa51cb9beaeaeea07c09255672ebd..ce989c9eadba03c1eea3faaba7cb534163ceda0a 100644 (file)
--- 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)