diff options
author | Morgan Deters <mdeters@gmail.com> | 2012-09-06 02:38:39 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2012-09-06 02:38:39 +0000 |
commit | 84a3411720a59410c7dff7bc8ec9210638b7665b (patch) | |
tree | 96027609ae62ff12a37aee15762e2ea245a07216 /src/smt/smt_engine.h | |
parent | bf0912f64da23092716fa187df607e50eba92984 (diff) |
Remove SmtEngine::getStackLevel(), which exposed implementation details and was only used by the compatibility layer.
Make SmtEngine::internalPop() delay popping. This fixes a bug in model generation.
Diffstat (limited to 'src/smt/smt_engine.h')
-rw-r--r-- | src/smt/smt_engine.h | 14 |
1 files changed, 8 insertions, 6 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 234814245..2c99bc7eb 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -135,6 +135,11 @@ class CVC4_PUBLIC SmtEngine { LogicInfo d_logic; /** + * Number of internal pops that have been deferred. + */ + unsigned d_pendingPops; + + /** * Whether or not this SmtEngine has been fully initialized (that is, * the ). This post-construction initialization is automatically * triggered by the use of the SmtEngine; e.g. when setLogic() is @@ -238,7 +243,9 @@ class CVC4_PUBLIC SmtEngine { void internalPush(); - void internalPop(); + void internalPop(bool immediate = false); + + void doPendingPops(); /** * Internally handle the setting of a logic. This function should always @@ -415,11 +422,6 @@ public: std::vector<Expr> getAssertions() throw(ModalException, AssertionException); /** - * Get the current context level. - */ - size_t getStackLevel() const; - - /** * Push a user-level context. */ void push(); |