New --tear-down-incremental mode, useful for debugging and performance profiling.

5 files changed, 98 insertions, 7 deletions

diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index a1410d910..4644c91a7 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -28,7 +28,7 @@ void printStatsIncremental(std::ostream& out, const std::string& prvsStatsString
 
 CommandExecutor::CommandExecutor(ExprManager &exprMgr, Options &options) :
   d_exprMgr(exprMgr),
-  d_smtEngine(SmtEngine(&exprMgr)),
+  d_smtEngine(new SmtEngine(&exprMgr)),
   d_options(options),
   d_stats("driver"),
   d_result() {
@@ -61,13 +61,22 @@ bool CommandExecutor::doCommand(Command* cmd)
   }
 }
 
+void CommandExecutor::reset()
+{
+  if(d_options[options::statistics]) {
+    flushStatistics(*d_options[options::err]);
+  }
+  delete d_smtEngine;
+  d_smtEngine = new SmtEngine(&d_exprMgr);
+}
+
 bool CommandExecutor::doCommandSingleton(Command* cmd)
 {
   bool status = true;
   if(d_options[options::verbosity] >= -1) {
-    status = smtEngineInvoke(&d_smtEngine, cmd, d_options[options::out]);
+    status = smtEngineInvoke(d_smtEngine, cmd, d_options[options::out]);
   } else {
-    status = smtEngineInvoke(&d_smtEngine, cmd, NULL);
+    status = smtEngineInvoke(d_smtEngine, cmd, NULL);
   }
 
   Result res;
diff --git a/src/main/command_executor.h b/src/main/command_executor.h
index 5395cc804..e6e3d3411 100644
--- a/src/main/command_executor.h
+++ b/src/main/command_executor.h
@@ -33,7 +33,7 @@ private:
 
 protected:
   ExprManager& d_exprMgr;
-  SmtEngine d_smtEngine;
+  SmtEngine* d_smtEngine;
   Options& d_options;
   StatisticsRegistry d_stats;
   Result d_result;
@@ -41,7 +41,9 @@ protected:
 public:
   CommandExecutor(ExprManager &exprMgr, Options &options);
 
-  virtual ~CommandExecutor() {}
+  virtual ~CommandExecutor() {
+    delete d_smtEngine;
+  }
 
   /**
    * Executes a command. Recursively handles if cmd is a command
@@ -51,6 +53,7 @@ public:
   bool doCommand(CVC4::Command* cmd);
 
   Result getResult() const { return d_result; }
+  void reset();
 
   StatisticsRegistry& getStatisticsRegistry() {
     return d_stats;
@@ -58,7 +61,7 @@ public:
 
   virtual void flushStatistics(std::ostream& out) const {
     d_exprMgr.getStatistics().flushInformation(out);
-    d_smtEngine.getStatistics().flushInformation(out);
+    d_smtEngine->getStatistics().flushInformation(out);
     d_stats.flushInformation(out);
   }
 
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 61447afe2..9de3b2134 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -63,7 +63,7 @@ CommandExecutorPortfolio::CommandExecutorPortfolio
   }
 
   // Create the SmtEngine(s)
-  d_smts.push_back(&d_smtEngine);
+  d_smts.push_back(d_smtEngine);
   for(unsigned i = 1; i < d_numThreads; ++i) {
     d_smts.push_back(new SmtEngine(d_exprMgrs[i]));
   }
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index c2b879a6b..8117dbc05 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -238,6 +238,9 @@ int runCvc4(int argc, char* argv[], Options& opts) {
     Command* cmd;
     bool status = true;
     if(opts[options::interactive] && inputFromStdin) {
+      if( opts[options::tearDownIncremental] ) {
+        throw OptionException("--tear-down-incremental incompatible with --interactive");
+      }
 #ifndef PORTFOLIO_BUILD
       if(!opts.wasSetByUser(options::incrementalSolving)) {
         cmd = new SetOptionCommand("incremental", true);
@@ -267,6 +270,79 @@ int runCvc4(int argc, char* argv[], Options& opts) {
         status = pExecutor->doCommand(cmd) && status;
         delete cmd;
       }
+    } else if(opts[options::tearDownIncremental]) {
+      if(opts[options::incrementalSolving]) {
+        throw OptionException("--tear-down-incremental incompatible with --incremental");
+      }
+
+      ParserBuilder parserBuilder(exprMgr, filename, opts);
+
+      if( inputFromStdin ) {
+#if defined(CVC4_COMPETITION_MODE) && !defined(CVC4_SMTCOMP_APPLICATION_TRACK)
+        parserBuilder.withStreamInput(cin);
+#else /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
+        parserBuilder.withLineBufferedStreamInput(cin);
+#endif /* CVC4_COMPETITION_MODE && !CVC4_SMTCOMP_APPLICATION_TRACK */
+      }
+
+      vector< vector<Command*> > allCommands;
+      allCommands.push_back(vector<Command*>());
+      Parser *parser = parserBuilder.build();
+      if(replayParser != NULL) {
+        // have the replay parser use the file's declarations
+        replayParser->useDeclarationsFrom(parser);
+      }
+      bool needReset = false;
+      while(status && (cmd = parser->nextCommand())) {
+        if(dynamic_cast<PushCommand*>(cmd) != NULL) {
+          if(needReset) {
+            pExecutor->reset();
+            for(size_t i = 0; i < allCommands.size(); ++i) {
+              for(size_t j = 0; j < allCommands[i].size(); ++j) {
+                Command* cmd = allCommands[i][j]->clone();
+                pExecutor->doCommand(cmd);
+                delete cmd;
+              }
+            }
+            needReset = false;
+          }
+          allCommands.push_back(vector<Command*>());
+        } else if(dynamic_cast<PopCommand*>(cmd) != NULL) {
+          allCommands.pop_back(); // fixme leaks cmds here
+          pExecutor->reset();
+          for(size_t i = 0; i < allCommands.size(); ++i) {
+            for(size_t j = 0; j < allCommands[i].size(); ++j) {
+              Command* cmd = allCommands[i][j]->clone();
+              pExecutor->doCommand(cmd);
+              delete cmd;
+            }
+          }
+        } else if(dynamic_cast<CheckSatCommand*>(cmd) != NULL ||
+                  dynamic_cast<QueryCommand*>(cmd) != NULL) {
+          if(needReset) {
+            pExecutor->reset();
+            for(size_t i = 0; i < allCommands.size(); ++i) {
+              for(size_t j = 0; j < allCommands[i].size(); ++j) {
+                Command* cmd = allCommands[i][j]->clone();
+                pExecutor->doCommand(cmd);
+                delete cmd;
+              }
+            }
+          }
+          status = pExecutor->doCommand(cmd);
+          needReset = true;
+        } else {
+          allCommands.back().push_back(cmd->clone());
+          if(dynamic_cast<QuitCommand*>(cmd) != NULL) {
+            delete cmd;
+            break;
+          }
+          status = pExecutor->doCommand(cmd);
+        }
+        delete cmd;
+      }
+      // Remove the parser
+      delete parser;
     } else {
       if(!opts.wasSetByUser(options::incrementalSolving)) {
         cmd = new SetOptionCommand("incremental", false);
diff --git a/src/main/options b/src/main/options
index 8733011f7..fdb172c18 100644
--- a/src/main/options
+++ b/src/main/options
@@ -50,6 +50,9 @@ option segvSpin --segv-spin bool :default false
  spin on segfault/other crash waiting for gdb
 undocumented-alias --segv-nospin = --no-segv-spin
 
+expert-option tearDownIncremental --tear-down-incremental bool :default false
+ implement PUSH/POP/multi-query by destroying and recreating SmtEngine
+
 expert-option waitToJoin --wait-to-join bool :default true
  wait for other threads to join before quitting