From 5738d3d2f9e917829156e678cbf317f3a1a37c9a Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 4 Oct 2014 20:33:50 -0400 Subject: [PATCH] Support for RESET command in CVC native language (and infrastructure for support elsewhere). --- src/compat/cvc3_compat.cpp | 7 ++++++- src/expr/command.cpp | 24 ++++++++++++++++++++++-- src/expr/command.h | 12 ++++++++++-- src/expr/symbol_table.cpp | 7 ++++++- src/expr/symbol_table.h | 3 +++ src/parser/cvc/Cvc.g | 2 +- src/parser/parser.h | 4 ++++ src/printer/ast/ast_printer.cpp | 5 +++++ src/printer/cvc/cvc_printer.cpp | 5 +++++ src/printer/smt2/smt2_printer.cpp | 5 +++++ src/smt/smt_engine.cpp | 27 +++++++++++++++++++++++++++ src/smt/smt_engine.h | 12 ++++++++++++ 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, "").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(d_context)), d_typeMap(new(true) CDHashMap, Type>, StringHashFunction>(d_context)), d_functions(new(true) CDHashSet(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(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(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(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || + tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(out, c, d_cvc3Mode) || tryToStream(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(out, c) || tryToStream(out, c) || tryToStream(out, c) || + tryToStream(out, c) || tryToStream(out, c) || tryToStream(out, c) || tryToStream(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 @@ -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 -- 2.30.2