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().

10 files changed, 26 insertions, 63 deletions

diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 005de6a34..2c6413503 100644
--- 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 55f74f50c..41d6766e8 100644
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -73,6 +73,13 @@ public = true
   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"
   long       = "segv-spin"
diff --git a/src/smt/env.cpp b/src/smt/env.cpp
index 7efefabcd..9f647f7c9 100644
--- 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 7c12c86b9..786cdcab2 100644
--- 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 58ae025b8..829d6f2f5 100644
--- 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 0ca4d5b15..8ecf171bd 100644
--- 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 a250e2a7f..353d96da8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -227,22 +227,6 @@ class CVC5_EXPORT SmtEngine
   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.
    */
   void setTotalTimeStatistic(double seconds) CVC5_EXPORT;
diff --git a/src/smt/smt_engine_state.cpp b/src/smt/smt_engine_state.cpp
index a61c18384..2206b29cd 100644
--- 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 214193b00..e509eafcf 100644
--- 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 f88996278..5d17ae792 100644
--- 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;