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/smt | |
parent | 54b2aac34e418108265dd43a956a7865c50b9cf4 (diff) |
Support for RESET command in CVC native language (and infrastructure for support elsewhere).
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 27 | ||||
-rw-r--r-- | src/smt/smt_engine.h | 12 |
2 files changed, 39 insertions, 0 deletions
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. |