diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-04 20:33:50 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-10-06 11:56:39 -0400 |
commit | 5738d3d2f9e917829156e678cbf317f3a1a37c9a (patch) | |
tree | a1270a0330b80deaeb4c8feec7629c5f748ab367 /src/expr | |
parent | 54b2aac34e418108265dd43a956a7865c50b9cf4 (diff) |
Support for RESET command in CVC native language (and infrastructure for support elsewhere).
Diffstat (limited to 'src/expr')
-rw-r--r-- | src/expr/command.cpp | 24 | ||||
-rw-r--r-- | src/expr/command.h | 12 | ||||
-rw-r--r-- | src/expr/symbol_table.cpp | 7 | ||||
-rw-r--r-- | src/expr/symbol_table.h | 3 |
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 */ |