Makes the filename be set in the SMT engine by default (#2366)

4 files changed, 11 insertions, 1 deletions

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 7e7202a5a..f8c6e6e5a 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -69,6 +69,8 @@ public:
     return d_stats;
   }
 
+  SmtEngine* getSmtEngine() { return d_smtEngine; }
+
   /**
    * Flushes statistics to a file descriptor.
    */
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index 390d83eba..d9932fb43 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -269,6 +269,8 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     ReferenceStat<std::string> s_statFilename("filename", filenameStr);
     RegisterStatistic statFilenameReg(&pExecutor->getStatisticsRegistry(),
                                       &s_statFilename);
+    // set filename in smt engine
+    pExecutor->getSmtEngine()->setFilename(filenameStr);
 
     // Parse and execute commands until we are done
     Command* cmd;
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 7b45bcb3c..d7c1ece96 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1186,6 +1186,8 @@ void SmtEngine::setLogic(const char* logic) { setLogic(string(logic)); }
 LogicInfo SmtEngine::getLogicInfo() const {
   return d_logic;
 }
+void SmtEngine::setFilename(std::string filename) { d_filename = filename; }
+std::string SmtEngine::getFilename() const { return d_filename; }
 void SmtEngine::setLogicInternal()
 {
   Assert(!d_fullyInited, "setting logic in SmtEngine but the engine has already"
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 599087cb0..08bb773d6 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -260,7 +260,7 @@ class CVC4_PUBLIC SmtEngine {
   Result d_status;
 
   /**
-   * The name of the input (if any).
+   * The input file name (if any) or the name set through setInfo (if any)
    */
   std::string d_filename;
 
@@ -494,6 +494,10 @@ class CVC4_PUBLIC SmtEngine {
   void setOption(const std::string& key, const CVC4::SExpr& value)
       /* throw(OptionException, ModalException) */;
 
+  /** sets the input name */
+  void setFilename(std::string filename);
+  /** return the input name (if any) */
+  std::string getFilename() const;
   /**
    * Get the model (only if immediately preceded by a SAT
    * or INVALID query).  Only permitted if CVC4 was built with model