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

12 files changed, 106 insertions, 7 deletions

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 51b0c6083..08146760f 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2468,7 +2468,12 @@ Context* ValidityChecker::getCurrentContext() {
 }
 
 void ValidityChecker::reset() {
-  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
+  // reset everything, forget everything
+  d_smt->reset();
+  delete d_parserContext;
+  d_parserContext = CVC4::parser::ParserBuilder(d_em, "<internal>").withInputLanguage(CVC4::language::input::LANG_CVC4).withStringInput("").build();
+  s_typeToExpr.clear();
+  s_exprToType.clear();
 }
 
 void ValidityChecker::logAnnotation(const Expr& annot) {
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 4d9ca9f30..c976588d4 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -362,11 +362,31 @@ std::string QueryCommand::getCommandName() const throw() {
   return "query";
 }
 
-/* class QuitCommand */
+/* class ResetCommand */
+
+void ResetCommand::invoke(SmtEngine* smtEngine) throw() {
+  try {
+    smtEngine->reset();
+    d_commandStatus = CommandSuccess::instance();
+  } catch(exception& e) {
+    d_commandStatus = new CommandFailure(e.what());
+  }
+}
+
+Command* ResetCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
+  return new ResetCommand();
+}
 
-QuitCommand::QuitCommand() throw() {
+Command* ResetCommand::clone() const {
+  return new ResetCommand();
 }
 
+std::string ResetCommand::getCommandName() const throw() {
+  return "reset";
+}
+
+/* class QuitCommand */
+
 void QuitCommand::invoke(SmtEngine* smtEngine) throw() {
   Dump("benchmark") << *this;
   d_commandStatus = CommandSuccess::instance();
diff --git a/src/expr/command.h b/src/expr/command.h
index 4d2957b7c..75cf80aae 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -454,7 +454,6 @@ public:
   std::string getCommandName() const throw();
 };/* class SetUserAttributeCommand */
 
-
 class CVC4_PUBLIC CheckSatCommand : public Command {
 protected:
   Expr d_expr;
@@ -798,10 +797,19 @@ public:
   std::string getCommandName() const throw();
 };/* class PropagateRuleCommand */
 
+class CVC4_PUBLIC ResetCommand : public Command {
+public:
+  ResetCommand() throw() {}
+  ~ResetCommand() throw() {}
+  void invoke(SmtEngine* smtEngine) throw();
+  Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
+  Command* clone() const;
+  std::string getCommandName() const throw();
+};/* class ResetCommand */
 
 class CVC4_PUBLIC QuitCommand : public Command {
 public:
-  QuitCommand() throw();
+  QuitCommand() throw() {}
   ~QuitCommand() throw() {}
   void invoke(SmtEngine* smtEngine) throw();
   Command* exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap);
diff --git a/src/expr/symbol_table.cpp b/src/expr/symbol_table.cpp
index ce7d571db..3d53f2e44 100644
--- a/src/expr/symbol_table.cpp
+++ b/src/expr/symbol_table.cpp
@@ -34,7 +34,7 @@ using namespace std;
 namespace CVC4 {
 
 SymbolTable::SymbolTable() :
-  d_context(new Context),
+  d_context(new Context()),
   d_exprMap(new(true) CDHashMap<std::string, Expr, StringHashFunction>(d_context)),
   d_typeMap(new(true) CDHashMap<std::string, pair<vector<Type>, Type>, StringHashFunction>(d_context)),
   d_functions(new(true) CDHashSet<Expr, ExprHashFunction>(d_context)) {
@@ -206,4 +206,9 @@ size_t SymbolTable::getLevel() const throw() {
   return d_context->getLevel();
 }
 
+void SymbolTable::reset() {
+  this->SymbolTable::~SymbolTable();
+  new(this) SymbolTable();
+}
+
 }/* CVC4 namespace */
diff --git a/src/expr/symbol_table.h b/src/expr/symbol_table.h
index a9ab43cfe..451a482dc 100644
--- a/src/expr/symbol_table.h
+++ b/src/expr/symbol_table.h
@@ -198,6 +198,9 @@ public:
   /** Get the current level of this symbol table. */
   size_t getLevel() const throw();
 
+  /** Reset everything. */
+  void reset();
+
 };/* class SymbolTable */
 
 }/* CVC4 namespace */
diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index aad365563..bb987332c 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -697,7 +697,7 @@ mainCommand[CVC4::Command*& cmd]
     { UNSUPPORTED("POPTO_SCOPE command"); }
 
   | RESET_TOK
-    { UNSUPPORTED("RESET command"); }
+    { cmd = new ResetCommand(); }
 
     // Datatypes can be mututally-recursive if they're in the same
     // definition block, separated by a comma.  So we parse everything
diff --git a/src/parser/parser.h b/src/parser/parser.h
index 87a331711..52236294a 100644
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -561,6 +561,10 @@ public:
     }
   }
 
+  inline void reset() {
+    d_symtab->reset();
+  }
+
   /**
    * Set the current symbol table used by this parser.
    * From now on, this parser will perform its definitions and
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 9b60c8942..220916a1a 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -140,6 +140,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<PopCommand>(out, c) ||
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
+     tryToStream<ResetCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -224,6 +225,10 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   out << "Query(" << c->getExpr() << ')';
 }
 
+static void toStream(std::ostream& out, const ResetCommand* c) throw() {
+  out << "Reset()";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "Quit()";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index ed5116bc6..2b5cc39c8 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -859,6 +859,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<PopCommand>(out, c, d_cvc3Mode) ||
      tryToStream<CheckSatCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QueryCommand>(out, c, d_cvc3Mode) ||
+     tryToStream<ResetCommand>(out, c, d_cvc3Mode) ||
      tryToStream<QuitCommand>(out, c, d_cvc3Mode) ||
      tryToStream<DeclarationSequence>(out, c, d_cvc3Mode) ||
      tryToStream<CommandSequence>(out, c, d_cvc3Mode) ||
@@ -1045,6 +1046,10 @@ static void toStream(std::ostream& out, const QueryCommand* c, bool cvc3Mode) th
   }
 }
 
+static void toStream(std::ostream& out, const ResetCommand* c, bool cvc3Mode) throw() {
+  out << "RESET;";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c, bool cvc3Mode) throw() {
   //out << "EXIT;";
 }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index 3ca5674e9..b415c6b19 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -699,6 +699,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<PopCommand>(out, c) ||
      tryToStream<CheckSatCommand>(out, c) ||
      tryToStream<QueryCommand>(out, c) ||
+     tryToStream<ResetCommand>(out, c) ||
      tryToStream<QuitCommand>(out, c) ||
      tryToStream<DeclarationSequence>(out, c) ||
      tryToStream<CommandSequence>(out, c) ||
@@ -940,6 +941,10 @@ static void toStream(std::ostream& out, const QueryCommand* c) throw() {
   }
 }
 
+static void toStream(std::ostream& out, const ResetCommand* c) throw() {
+  out << "(reset)";
+}
+
 static void toStream(std::ostream& out, const QuitCommand* c) throw() {
   out << "(exit)";
 }
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.