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

diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 7e7202a5a44ebf75d9aa19f366c00d56e9f89603..f8c6e6e5a9717c2dc464264169a8ab419b224755 100644 (file)
--- 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 390d83ebae2d047122b4a46d13649b99cb19fc35..d9932fb430bdba238be4dd53462b266a7b2a8ccb 100644 (file)
--- 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 7b45bcb3c5a60aad165fe04604302269c116dcdb..d7c1ece96779b6739312d40570dbf7ec8c021f04 100644 (file)
--- 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 599087cb09f46dc4994ea37326f3024d2c0b1be2..08bb773d6c646029eeff5840e54a474be8586c3d 100644 (file)
--- 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