Support for RESET command in CVC native language (and infrastructure for support elsewhere).

2 files changed, 39 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 015e6a4f4..dc652ad69 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -4162,6 +4162,33 @@ void SmtEngine::doPendingPops() {
   }
 }
 
+void SmtEngine::reset() throw() {
+  SmtScope smts(this);
+  ExprManager *em = d_exprManager;
+  Trace("smt") << "SMT reset()" << endl;
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << ResetCommand();
+  }
+  this->~SmtEngine();
+  new(this) SmtEngine(em);
+}
+
+void SmtEngine::resetAssertions() throw() {
+  SmtScope smts(this);
+
+  while(!d_userLevels.empty()) {
+    pop();
+  }
+
+  // Also remember the global push/pop around everything.
+  Assert(d_userLevels.size() == 0 && d_userContext->getLevel() == 1);
+  d_context->popto(0);
+  d_userContext->popto(0);
+  d_modelGlobalCommands.clear();
+  d_userContext->push();
+  d_context->push();
+}
+
 void SmtEngine::interrupt() throw(ModalException) {
   if(!d_fullyInited) {
     return;
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index ac0170f3b..7effa521a 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -533,6 +533,18 @@ public:
   void pop() throw(ModalException);
 
   /**
+   * Completely reset the state of the solver, as though destroyed and
+   * recreated.  The result is as if newly constructed (so it still
+   * retains the same options structure and ExprManager).
+   */
+  void reset() throw();
+
+  /**
+   * Reset all assertions, global declarations, etc.
+   */
+  void resetAssertions() throw();
+
+  /**
    * Interrupt a running query.  This can be called from another thread
    * or from a signal handler.  Throws a ModalException if the SmtEngine
    * isn't currently in a query.