diff options
Diffstat (limited to 'src/api')
| -rw-r--r-- | src/api/cpp/cvc5.cpp | 12 | ||||
| -rw-r--r-- | src/api/cpp/cvc5.h | 12 |
2 files changed, 24 insertions, 0 deletions
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 @@ -3741,6 +3741,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: * \verbatim |