Refactor filename handling (#7088)

This PR simplifies how we store the current input file name and handle setting and getting it.
It is now an option, that can also be set and get via setInfo() and getInfo().

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 005de6a34044e80e6bf6b6744b36e12094800ddf..2c64135037256a8344c738fc5894d1eab6ed0ab8 100644 (file)
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -205,7 +205,7 @@ int runCvc5(int argc, char* argv[], std::unique_ptr<api::Solver>& solver)
   int returnValue = 0;
   {
     // notify SmtEngine that we are starting to parse
-    pExecutor->getSmtEngine()->notifyStartParsing(filenameStr);
+    pExecutor->getSmtEngine()->setInfo("filename", filenameStr);
 
     // Parse and execute commands until we are done
     std::unique_ptr<Command> cmd;

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index 55f74f50cf15e38969aafb011cda37af1923b7be..41d6766e8bcf140eb1508a716be91146bddf0cdb 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -72,6 +72,13 @@ public = true
   type       = "bool"
   help       = "force interactive shell/non-interactive mode"
 
+[[option]]
+  name       = "filename"
+  category   = "undocumented"
+  long       = "filename=FILENAME"
+  type       = "std::string"
+  help       = "filename of the input"
+
 [[option]]
   name       = "segvSpin"
   category   = "regular"

diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 7efefabcdd65927b8b8c3db075b0b708a2e45cf9..9f647f7c95cd18e19e790294b5636feece9ef508 100644 (file)
--- a/src/smt/env.cpp
+++ b/src/smt/env.cpp
@@ -65,8 +65,6 @@ void Env::setProofNodeManager(ProofNodeManager* pnm)
   d_topLevelSubs->setProofNodeManager(pnm);
 }
 
-void Env::setFilename(const std::string& filename) { d_filename = filename; }
-
 void Env::shutdown()
 {
   d_rewriter.reset(nullptr);
@@ -83,8 +81,6 @@ NodeManager* Env::getNodeManager() const { return d_nodeManager; }
 
 ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
 
-const std::string& Env::getFilename() const { return d_filename; }
-
 bool Env::isSatProofProducing() const
 {
   return d_proofNodeManager != nullptr

diff --git a/src/smt/env.h b/src/smt/env.h
index 7c12c86b901dccb89c12a6a17023fabc517f4828..786cdcab2f3b0d50447c7e7356c116289bf6ea6f 100644 (file)
--- a/src/smt/env.h
+++ b/src/smt/env.h
@@ -82,9 +82,6 @@ class Env
    */
   ProofNodeManager* getProofNodeManager();
 
-  /** Return the input name, or the empty string if not set */
-  const std::string& getFilename() const;
-
   /**
    * Check whether the SAT solver should produce proofs. Other than whether
    * the proof node manager is set, SAT proofs are only generated when the
@@ -143,11 +140,6 @@ class Env
 
   /** Set proof node manager if it exists */
   void setProofNodeManager(ProofNodeManager* pnm);
-  /**
-   * Set that the file name of the current instance is the given string. This
-   * is used for various purposes (e.g. get-info, SZS status).
-   */
-  void setFilename(const std::string& filename);
 
   /* Private shutdown ------------------------------------------------------- */
   /**
@@ -214,12 +206,6 @@ class Env
   const Options* d_originalOptions;
   /** Manager for limiting time and abstract resource usage. */
   std::unique_ptr<ResourceManager> d_resourceManager;
-
-  /**
-   * The input file name or the name set through (set-info :filename ...), if
-   * any.
-   */
-  std::string d_filename;
 }; /* class Env */
 
 }  // namespace cvc5

diff --git a/src/smt/proof_manager.cpp b/src/smt/proof_manager.cpp
index 58ae025b832220a7193ba6ad46f20dc347ce650b..829d6f2f5f358480f4d110f0f767d0cdd57f182d 100644 (file)
--- a/src/smt/proof_manager.cpp
+++ b/src/smt/proof_manager.cpp
@@ -16,6 +16,7 @@
 #include "smt/proof_manager.h"
 
 #include "options/base_options.h"
+#include "options/main_options.h"
 #include "options/proof_options.h"
 #include "options/smt_options.h"
 #include "proof/dot/dot_printer.h"
@@ -161,10 +162,10 @@ void PfManager::printProof(std::ostream& out,
   }
   else if (options::proofFormatMode() == options::ProofFormatMode::TPTP)
   {
-    out << "% SZS output start Proof for " << d_env.getFilename() << std::endl;
+    out << "% SZS output start Proof for " << d_env.getOptions().driver.filename << std::endl;
     // TODO (proj #37) print in TPTP compliant format
     out << *fp << std::endl;
-    out << "% SZS output end Proof for " << d_env.getFilename() << std::endl;
+    out << "% SZS output end Proof for " << d_env.getOptions().driver.filename << std::endl;
   }
   else
   {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0ca4d5b15ecc5bbf709891f36309c6e772db6048..8ecf171bdcb97da42ccc486f27f1bbeadc570993 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -375,25 +375,6 @@ LogicInfo SmtEngine::getUserLogicInfo() const
   return res;
 }
 
-void SmtEngine::notifyStartParsing(const std::string& filename)
-{
-  d_env->setFilename(filename);
-  d_env->getStatisticsRegistry().registerValue<std::string>("driver::filename",
-                                                            filename);
-  // Copy the original options. This is called prior to beginning parsing.
-  // Hence reset should revert to these options, which note is after reading
-  // the command line.
-}
-
-const std::string& SmtEngine::getFilename() const
-{
-  return d_env->getFilename();
-}
-
-void SmtEngine::setResultStatistic(const std::string& result) {
-  d_env->getStatisticsRegistry().registerValue<std::string>("driver::sat/unsat",
-                                                            result);
-}
 void SmtEngine::setTotalTimeStatistic(double seconds) {
   d_env->getStatisticsRegistry().registerValue<double>("driver::totalTime",
                                                        seconds);
@@ -432,7 +413,10 @@ void SmtEngine::setInfo(const std::string& key, const std::string& value)
 
   if (key == "filename")
   {
-    d_env->setFilename(value);
+    d_env->d_options.driver.filename = value;
+    d_env->d_originalOptions->driver.filename = value;
+    d_env->getStatisticsRegistry().registerValue<std::string>(
+        "driver::filename", value);
   }
   else if (key == "smt-lib-version" && !getOptions().base.inputLanguageWasSetByUser)
   {
@@ -487,6 +471,10 @@ std::string SmtEngine::getInfo(const std::string& key) const
   {
     return "immediate-exit";
   }
+  if (key == "filename")
+  {
+    return d_env->getOptions().driver.filename;
+  }
   if (key == "name")
   {
     return toSExpr(Configuration::getName());
@@ -724,7 +712,7 @@ void SmtEngine::defineFunctionRec(Node func,
 Result SmtEngine::quickCheck() {
   Assert(d_state->isFullyInited());
   Trace("smt") << "SMT quickCheck()" << endl;
-  const std::string& filename = d_env->getFilename();
+  const std::string& filename = d_env->getOptions().driver.filename;
   return Result(
       Result::ENTAILMENT_UNKNOWN, Result::REQUIRES_FULL_CHECK, filename);
 }
@@ -940,7 +928,7 @@ Result SmtEngine::checkSatInternal(const std::vector<Node>& assumptions,
     {
       printStatisticsDiff();
     }
-    return Result(Result::SAT_UNKNOWN, why, d_env->getFilename());
+    return Result(Result::SAT_UNKNOWN, why, d_env->getOptions().driver.filename);
   }
 }
 
@@ -1242,7 +1230,7 @@ Model* SmtEngine::getModel() {
   }
   // set the information on the SMT-level model
   Assert(m != nullptr);
-  m->d_inputName = d_env->getFilename();
+  m->d_inputName = d_env->getOptions().driver.filename;
   m->d_isKnownSat = (d_state->getMode() == SmtMode::SAT);
   return m;
 }

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index a250e2a7f193d382aebdaa8ead9cd74c5c3fe6e9..353d96da8f429250dcabb0b0ac2ec56437774286 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -226,22 +226,6 @@ class CVC5_EXPORT SmtEngine
   /** Is this an internal subsolver? */
   bool isInternalSubsolver() const;
 
-  /**
-   * Notify that we are now parsing the input with the given filename.
-   * This call sets the filename maintained by this SmtEngine for bookkeeping
-   * and also makes a copy of the current options of this SmtEngine. This
-   * is required so that the SMT-LIB command (reset) returns the SmtEngine
-   * to a state where its options were prior to parsing but after e.g.
-   * reading command line options.
-   */
-  void notifyStartParsing(const std::string& filename) CVC5_EXPORT;
-  /** return the input name (if any) */
-  const std::string& getFilename() const;
-
-  /**
-   * Helper method for the API to put the last check result into the statistics.
-   */
-  void setResultStatistic(const std::string& result) CVC5_EXPORT;
   /**
    * Helper method for the API to put the total runtime into the statistics.
    */

diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index a61c18384c46d5c4e33fcaede2889e6e42cc60b6..2206b29cd9f31aa5d9b07b77e18040fe55ed5454 100644 (file)
--- a/src/smt/smt_engine_state.cpp
+++ b/src/smt/smt_engine_state.cpp
@@ -17,6 +17,7 @@
 
 #include "base/modal_exception.h"
 #include "options/base_options.h"
+#include "options/main_options.h"
 #include "options/option_exception.h"
 #include "options/smt_options.h"
 #include "smt/env.h"
@@ -43,7 +44,7 @@ void SmtEngineState::notifyExpectedStatus(const std::string& status)
   Assert(status == "sat" || status == "unsat" || status == "unknown")
       << "SmtEngineState::notifyExpectedStatus: unexpected status string "
       << status;
-  d_expectedStatus = Result(status, d_env.getFilename());
+  d_expectedStatus = Result(status, d_env.getOptions().driver.filename);
 }
 
 void SmtEngineState::notifyResetAssertions()

diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index 214193b00701a2cf61442681765609a0972b2f84..e509eafcf3e194444fc35a190a0449ead12bb2f9 100644 (file)
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -15,6 +15,7 @@
 
 #include "smt/smt_solver.h"
 
+#include "options/main_options.h"
 #include "options/smt_options.h"
 #include "prop/prop_engine.h"
 #include "smt/assertions.h"
@@ -133,7 +134,7 @@ Result SmtSolver::checkSatisfiability(Assertions& as,
 
   Trace("smt") << "SmtSolver::check()" << endl;
 
-  const std::string& filename = d_env.getFilename();
+  const std::string& filename = d_env.getOptions().driver.filename;
   ResourceManager* rm = d_env.getResourceManager();
   if (rm->out())
   {

diff --git a/src/util/statistics_public.cpp b/src/util/statistics_public.cpp
index f88996278e202d7c650fbc1a699e3e2a0fdadffd..5d17ae7925b2721f652b5dc83160e0dc8b1ae1be 100644 (file)
--- a/src/util/statistics_public.cpp
+++ b/src/util/statistics_public.cpp
@@ -30,7 +30,6 @@ void registerPublicStatistics(StatisticsRegistry& reg)
   reg.registerHistogram<api::Kind>("api::TERM", false);
 
   reg.registerValue<std::string>("driver::filename", false);
-  reg.registerValue<std::string>("driver::sat/unsat", false);
   reg.registerValue<double>("driver::totalTime", false);
 
   for (theory::TheoryId id = theory::THEORY_FIRST; id != theory::THEORY_LAST;