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

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 51b0c6083bf812da71da5baacdeb08ab76324fa7..08146760ff04bbd64a052360c77f4b8fe7a3611c 100644 (file)
--- 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 4d9ca9f308be7a43f9febcc8fabe5082968bf2cb..c976588d488a65bfe249b9f851318ceedc83696b 100644 (file)
--- 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 4d2957b7cd615c2318c98a8cbface18aeea3da50..75cf80aae647efdb1b0f8aef26284a15a1cd722e 100644 (file)
--- 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 ce7d571db636d4c8676d4fb82e37faaeaace2d23..3d53f2e44bae67faebc0c77cda00121c6bf9d8fb 100644 (file)
--- 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 a9ab43cfe3a699e5e531fb1ceb54f70ec1dc2e56..451a482dc9851bfb96bbee48769fbc4a131d41ca 100644 (file)
--- 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 aad3655630f64119ee102392ea020b679eefe77f..bb987332cd5ed72a641b0c0ebb109a6c38bd7e4e 100644 (file)
--- 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 87a331711ba23b8a031482e0106c79efb204e226..52236294a26016ed5c564c4322e4bb9c73c7b57d 100644 (file)
--- 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 9b60c8942587eda4faa2adf0de86b8847f50954d..220916a1ab70446a7479d4c4c313ecc2cdcce630 100644 (file)
--- 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 ed5116bc626f66e07c6e553b1cf460ccae7ccc94..2b5cc39c82a9ddaf7c8e34fdda31487194d13c79 100644 (file)
--- 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 3ca5674e9f98f59d46a20154b3baf41f3bec58b8..b415c6b19307b3b6a3732bd084ebf3a172a5a2b2 100644 (file)
--- 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 015e6a4f4c70bfddafce52cecbecd2127d7bf386..dc652ad69c1fc397718cb67819ece88cee1a2ddb 100644 (file)
--- 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 ac0170f3b363ec962780a7eaaf696d78eb62bd98..7effa521ac441645461a044723992117db0c16fd 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -532,6 +532,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