Refactor proof output for TPTP (#7029)

This eliminates the old option "inst format mode" and makes proof output for TPTP organized as an ordinary proof output format.

diff --git a/src/options/options_handler.cpp b/src/options/options_handler.cpp
index 55661a0949501f257cd7940f43ae157ceef0f421..42a63b47c27092d14a5df58771333370693e0751 100644 (file)
--- a/src/options/options_handler.cpp
+++ b/src/options/options_handler.cpp
@@ -209,34 +209,6 @@ void OptionsHandler::setBitblastAig(const std::string& option,
   }
 }
 
-// printer/options_handlers.h
-const std::string OptionsHandler::s_instFormatHelp = "\
-Inst format modes currently supported by the --inst-format option:\n\
-\n\
-default \n\
-+ Print instantiations as a list in the output language format.\n\
-\n\
-szs\n\
-+ Print instantiations as SZS compliant proof.\n\
-";
-
-InstFormatMode OptionsHandler::stringToInstFormatMode(const std::string& option,
-                                                      const std::string& flag,
-                                                      const std::string& optarg)
-{
-  if(optarg == "default") {
-    return InstFormatMode::DEFAULT;
-  } else if(optarg == "szs") {
-    return InstFormatMode::SZS;
-  } else if(optarg == "help") {
-    puts(s_instFormatHelp.c_str());
-    exit(1);
-  } else {
-    throw OptionException(std::string("unknown option for --inst-format: `") +
-                          optarg + "'.  Try --inst-format help.");
-  }
-}
-
 void OptionsHandler::setProduceAssertions(const std::string& option,
                                           const std::string& flag,
                                           bool value)

diff --git a/src/options/options_handler.h b/src/options/options_handler.h
index f19e63445bbf977836b53849efc3e06a44adc6f5..d6b81525d707296a82fdf2d455e726f1a6089436 100644 (file)
--- a/src/options/options_handler.h
+++ b/src/options/options_handler.h
@@ -183,10 +183,6 @@ public:
 
   /** Pointer to the containing Options object.*/
   Options* d_options;
-
-  /* Help strings */
-  static const std::string s_instFormatHelp;
-
 }; /* class OptionHandler */
 
 }  // namespace options

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index 433e6f613b77ce39bfeeae4ee38f2cdf667d7117..a8b11c1979c6e36aee96341691d97027bd374396 100644 (file)
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -16,25 +16,6 @@ name   = "Printing"
   name = "table"
   help = "Print functional expressions over finite domains in a table format."
 
-[[option]]
-  name       = "instFormatMode"
-  category   = "regular"
-  long       = "inst-format=MODE"
-  type       = "InstFormatMode"
-  default    = "InstFormatMode::DEFAULT"
-  handler    = "stringToInstFormatMode"
-  includes   = ["options/printer_modes.h"]
-  help       = "print format mode for instantiations, see --inst-format=help"
-# InstFormatMode is currently exported as public so we can't auto genenerate
-# the enum.
-#  help_mode  = "Inst format modes."
-#[[option.mode.DEFAULT]]
-#  name = "default"
-#  help = "Print instantiations as a list in the output language format."
-#[[option.mode.SZS]]
-#  name = "szs"
-#  help = "Print instantiations as SZS compliant proof."
-
 [[option]]
   name       = "flattenHOChains"
   category   = "regular"

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index f0458793e4d98fc5e9dce686c08b4eca17643d5c..071f14dec73d08703979c584f44e53b1a93eb393 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -18,6 +18,9 @@ name   = "Proof"
 [[option.mode.VERIT]]
   name       = "verit"
   help       = "Output veriT proof"
+[[option.mode.TPTP]]
+  name       = "tptp"
+  help       = "Output TPTP proof (work in progress)"
 
 [[option]]
   name       = "proofPrintConclusion"

diff --git a/src/smt/command.cpp b/src/smt/command.cpp
index bb501fa5ccaf62df89d6cd24286b8c1c26d4252e..7aa05dde1bc09d72c780a156a612d2e904fc655b 100644 (file)
--- a/src/smt/command.cpp
+++ b/src/smt/command.cpp
@@ -2047,11 +2047,9 @@ GetInstantiationsCommand::GetInstantiationsCommand() : d_solver(nullptr) {}
 bool GetInstantiationsCommand::isEnabled(api::Solver* solver,
                                          const api::Result& res)
 {
-  return (solver->getOptions().printer.instFormatMode
-              != options::InstFormatMode::SZS
-          && (res.isSat()
-              || (res.isSatUnknown()
-                  && res.getUnknownExplanation() == api::Result::INCOMPLETE)))
+  return (res.isSat()
+          || (res.isSatUnknown()
+              && res.getUnknownExplanation() == api::Result::INCOMPLETE))
          || res.isUnsat() || res.isEntailed();
 }
 void GetInstantiationsCommand::invoke(api::Solver* solver, SymbolManager* sm)

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 2c04b9e763b4e412aae21982938a8c805e35ebd7..718d6cd6d5d5d05ce1b03b8ff6628b9bd93d0699 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -23,17 +23,19 @@
 #include "proof/proof_node_algorithm.h"
 #include "proof/proof_node_manager.h"
 #include "smt/assertions.h"
+#include "smt/env.h"
 #include "smt/preprocess_proof_generator.h"
 #include "smt/proof_post_processor.h"
 
 namespace cvc5 {
 namespace smt {
 
-PfManager::PfManager(context::UserContext* u, SmtEngine* smte)
-    : d_pchecker(new ProofChecker(options::proofPedantic())),
+PfManager::PfManager(Env& env, SmtEngine* smte)
+    : d_env(env),
+      d_pchecker(new ProofChecker(options::proofPedantic())),
       d_pnm(new ProofNodeManager(d_pchecker.get())),
       d_pppg(new PreprocessProofGenerator(
-          d_pnm.get(), u, "smt::PreprocessProofGenerator")),
+          d_pnm.get(), env.getUserContext(), "smt::PreprocessProofGenerator")),
       d_pfpp(new ProofPostproccess(
           d_pnm.get(),
           smte,
@@ -157,6 +159,13 @@ void PfManager::printProof(std::ostream& out,
     proof::DotPrinter dotPrinter;
     dotPrinter.print(out, fp.get());
   }
+  else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
+  {
+    out << "% SZS output start Proof for " << d_env.getFilename() << std::endl;
+    // TODO (proj #37) print in TPTP compliant format
+    out << *fp;
+    out << "% SZS output end Proof for " << d_env.getFilename() << std::endl;
+  }
   else
   {
     out << "(proof\n";

diff --git a/src/smt/proof_manager.h b/src/smt/proof_manager.h
index 57478573c8744d242af5359ffac4f421cbe824c3..fd24f62f691952e0fb2c0e7f2270b6f0da3ef819 100644 (file)
--- a/src/smt/proof_manager.h
+++ b/src/smt/proof_manager.h
@@ -23,6 +23,7 @@
 
 namespace cvc5 {
 
+class Env;
 class ProofChecker;
 class ProofNode;
 class ProofNodeManager;
@@ -70,7 +71,7 @@ class ProofPostproccess;
 class PfManager
 {
  public:
-  PfManager(context::UserContext* u, SmtEngine* smte);
+  PfManager(Env& env, SmtEngine* smte);
   ~PfManager();
   /**
    * Print the proof on the given output stream.
@@ -116,6 +117,8 @@ class PfManager
    */
   void getAssertions(Assertions& as,
                      std::vector<Node>& assertions);
+  /** Reference to the env of SmtEngine */
+  Env& d_env;
   /** The false node */
   Node d_false;
   /** For the new proofs module */

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 78bb9044a30cc3212a9b49bd3095b1f47119ee53..0ddac720286525118d52974477ff7ae8e77c7534 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -203,7 +203,7 @@ void SmtEngine::finishInit()
     // ensure bound variable uses canonical bound variables
     getNodeManager()->getBoundVarManager()->enableKeepCacheValues();
     // make the proof manager
-    d_pfManager.reset(new PfManager(getUserContext(), this));
+    d_pfManager.reset(new PfManager(*d_env.get(), this));
     PreprocessProofGenerator* pppg = d_pfManager->getPreprocessProofGenerator();
     // start the unsat core manager
     d_ucManager.reset(new UnsatCoreManager());
@@ -1599,10 +1599,6 @@ std::string SmtEngine::getProof()
 void SmtEngine::printInstantiations( std::ostream& out ) {
   SmtScope smts(this);
   finishInit();
-  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
-  {
-    out << "% SZS output start Proof for " << d_env->getFilename() << std::endl;
-  }
   QuantifiersEngine* qe = getAvailableQuantifiersEngine("printInstantiations");
 
   // First, extract and print the skolemizations
@@ -1689,10 +1685,6 @@ void SmtEngine::printInstantiations( std::ostream& out ) {
   {
     out << "none" << std::endl;
   }
-  if (d_env->getOptions().printer.instFormatMode == options::InstFormatMode::SZS)
-  {
-    out << "% SZS output end Proof for " << d_env->getFilename() << std::endl;
-  }
 }
 
 void SmtEngine::getInstantiationTermVectors(