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

4 files changed, 41 insertions, 5 deletions

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 */