diff options
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(); |