[proof-new] Implementing getProof in the API and SMT engine (#5751)

A proof is represented as a string in GetProofCommand. The string is generated by the custom ways in which the SMT engine may choose to print the proof, based on proof-format-mode (to be added in subsequent commits).

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 49974d30d54a504338fed3286a65ebcf39ed155a..621e3c1c004c3ddd9e8c523984e984713556ae16 100644 (file)
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -2473,7 +2473,7 @@ Term DatatypeConstructor::getSpecializedConstructorTerm(Sort retSort) const
       << "Cannot get specialized constructor type for non-datatype type "
       << retSort;
   CVC4_API_SOLVER_TRY_CATCH_BEGIN;
-  
+
   NodeManager* nm = d_solver->getNodeManager();
   Node ret =
       nm->mkNode(kind::APPLY_TYPE_ASCRIPTION,

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index f3b0ee915eeb27973c182e766e6cf82a9f779932..0c8accf7a394bbb9c6028d289062402fac0437c0 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -1886,7 +1886,31 @@ void BlockModelValuesCommand::toStream(std::ostream& out,
 GetProofCommand::GetProofCommand() {}
 void GetProofCommand::invoke(api::Solver* solver, SymbolManager* sm)
 {
-  Unimplemented() << "Unimplemented get-proof\n";
+  try
+  {
+    d_result = solver->getSmtEngine()->getProof();
+    d_commandStatus = CommandSuccess::instance();
+  }
+  catch (api::CVC4ApiRecoverableException& e)
+  {
+    d_commandStatus = new CommandRecoverableFailure(e.what());
+  }
+  catch (exception& e)
+  {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+void GetProofCommand::printResult(std::ostream& out, uint32_t verbosity) const
+{
+  if (ok())
+  {
+    out << d_result;
+  }
+  else
+  {
+    this->Command::printResult(out, verbosity);
+  }
 }
 
 Command* GetProofCommand::clone() const

diff --git a/src/smt/command.h b/src/smt/command.h
index 399050d947a3640f044d49a13588c4cb7dd8b76b..9330f20154bb00413d00ffc9b9883efc75ce09d0 100644 (file)
--- a/src/smt/command.h
+++ b/src/smt/command.h
@@ -1015,6 +1015,9 @@ class CVC4_PUBLIC GetProofCommand : public Command
   GetProofCommand();
 
   void invoke(api::Solver* solver, SymbolManager* sm) override;
+
+  void printResult(std::ostream& out, uint32_t verbosity = 2) const override;
+
   Command* clone() const override;
   std::string getCommandName() const override;
   void toStream(
@@ -1022,6 +1025,10 @@ class CVC4_PUBLIC GetProofCommand : public Command
       int toDepth = -1,
       size_t dag = 1,
       OutputLanguage language = language::output::LANG_AUTO) const override;
+
+ private:
+  /** the result of the getProof call */
+  std::string d_result;
 }; /* class GetProofCommand */
 
 class CVC4_PUBLIC GetInstantiationsCommand : public Command

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index ce9b4923c62efc2ea3e6f1b587d6447b22130d64..d82e227369cd9ffd4dd90d90a5476e071a437fbe 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -108,7 +108,8 @@ void PfManager::setFinalProof(std::shared_ptr<ProofNode> pfn,
   Trace("smt-proof") << "SmtEngine::setFinalProof(): finished.\n";
 }
 
-void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
+void PfManager::printProof(std::ostream& out,
+                           std::shared_ptr<ProofNode> pfn,
                            Assertions& as,
                            DefinedFunctionMap& df)
 {
@@ -116,7 +117,6 @@ void PfManager::printProof(std::shared_ptr<ProofNode> pfn,
   std::shared_ptr<ProofNode> fp = getFinalProof(pfn, as, df);
   // TODO (proj #37) according to the proof format, post process the proof node
   // TODO (proj #37) according to the proof format, print the proof node
-  std::ostream& out = *options::out();
   out << "(proof\n";
   out << *fp;
   out << "\n)\n";

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index be05fc2f799e3b614607fd7abab3ac96a9343037..a6f284cade2a709a873cfeb7c8c4448691b782d9 100644 (file)
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -49,7 +49,7 @@ class PfManager
   PfManager(context::UserContext* u, SmtEngine* smte);
   ~PfManager();
   /**
-   * Print the proof on the output channel of the current options in scope.
+   * Print the proof on the given output stream.
    *
    * The argument pfn is the proof for false in the current context.
    *
@@ -58,7 +58,8 @@ class PfManager
    * function map correspond to equalities of the form (= f (lambda (...) t)),
    * which are considered assertions in the final proof.
    */
-  void printProof(std::shared_ptr<ProofNode> pfn,
+  void printProof(std::ostream& out,
+                  std::shared_ptr<ProofNode> pfn,
                   Assertions& as,
                   DefinedFunctionMap& df);
   /**

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 4c47587a6fe3dae08dde157b3f51aebfac3d37bc..d89b6e802c0056f99e94bdcde05962771856903b 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -953,12 +953,6 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     Trace("smt") << "SmtEngine::" << (isEntailmentCheck ? "query" : "checkSat")
                  << "(" << assumptions << ") => " << r << endl;
 
-    if (options::dumpProofs() && options::proofNew()
-        && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
-    {
-      printProof();
-    }
-
     // Check that SAT results generate a model correctly.
     if(options::checkModels()) {
       if (r.asSatisfiabilityResult().isSat() == Result::SAT)
@@ -1496,23 +1490,38 @@ UnsatCore SmtEngine::getUnsatCore() {
   return getUnsatCoreInternal();
 }
 
-void SmtEngine::printProof()
+std::string SmtEngine::getProof()
 {
-  if (d_pfManager == nullptr)
+  Trace("smt") << "SMT getProof()\n";
+  SmtScope smts(this);
+  finishInit();
+  if (Dump.isOn("benchmark"))
   {
-    throw RecoverableModalException("Cannot print proof, no proof manager.");
+    getOutputManager().getPrinter().toStreamCmdGetProof(
+        getOutputManager().getDumpOut());
   }
-  if (getSmtMode() != SmtMode::UNSAT)
+#if IS_PROOFS_BUILD
+  if (!options::proofNew())
+  {
+    throw ModalException("Cannot get a proof when proof-new option is off.");
+  }
+  if (d_state->getMode() != SmtMode::UNSAT)
   {
     throw RecoverableModalException(
-        "Cannot print proof unless immediately preceded by "
-        "UNSAT/ENTAILED.");
+        "Cannot get a proof unless immediately preceded by "
+        "UNSAT/ENTAILED response.");
   }
+  // the prop engine has the proof of false
   PropEngine* pe = getPropEngine();
   Assert(pe != nullptr);
   Assert(pe->getProof() != nullptr);
-  // the prop engine has the proof of false
-  d_pfManager->printProof(pe->getProof(), *d_asserts, *d_definedFunctions);
+  Assert(d_pfManager);
+  std::ostringstream ss;
+  d_pfManager->printProof(ss, pe->getProof(), *d_asserts, *d_definedFunctions);
+  return ss.str();
+#else  /* IS_PROOFS_BUILD */
+  throw ModalException("This build of CVC4 doesn't have proof support.");
+#endif /* IS_PROOFS_BUILD */
 }
 
 void SmtEngine::printInstantiations( std::ostream& out ) {

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 091f69642cc5c9fbdbf5aa3c8a166a2e2691b86f..558bd2b40a75405ed640518ab4fc9d1b08481545 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -683,6 +683,12 @@ class CVC4_PUBLIC SmtEngine
    */
   UnsatCore getUnsatCore();
 
+  /**
+   * Get a refutation proof (only if immediately preceded by an UNSAT or
+   * ENTAILED query). Only permitted if CVC4 was built with proof support and
+   * the proof option is on. */
+  std::string getProof();
+
   /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.