diff options
| -rw-r--r-- | NEWS | 5 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 13 | ||||
| -rw-r--r-- | src/smt/smt_engine.h | 6 |
3 files changed, 20 insertions, 4 deletions
@@ -3,7 +3,10 @@ This file contains a summary of important user-visible changes. Changes since 1.2 ================= -* nothing yet +* We no longer permit model or proof generation if there's been an + intervening push/pop. +* Increased compliance to SMT-LIBv2, numerous bugs and usability issues + resolved Changes since 1.1 ================= diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 3ee6b1d74..3cc6e7502 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -3625,6 +3625,11 @@ void SmtEngine::push() throw(ModalException, LogicException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a push, simplifying our lives somewhat and + // staying symmtric with pop. + d_problemExtended = true; + d_userLevels.push_back(d_userContext->getLevel()); internalPush(); Trace("userpushpop") << "SmtEngine: pushed to level " @@ -3651,6 +3656,14 @@ void SmtEngine::pop() throw(ModalException) { d_needPostsolve = false; } + // The problem isn't really "extended" yet, but this disallows + // get-model after a pop, simplifying our lives somewhat. It might + // not be strictly necessary to do so, since the pops occur lazily, + // but also it would be weird to have a legally-executed (get-model) + // that only returns a subset of the assignment (because the rest + // is no longer in scope!). + d_problemExtended = true; + AlwaysAssert(d_userContext->getLevel() > 0); AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h index 8266bb1ed..1b5af415f 100644 --- a/src/smt/smt_engine.h +++ b/src/smt/smt_engine.h @@ -189,9 +189,9 @@ class CVC4_PUBLIC SmtEngine { bool d_fullyInited; /** - * Whether or not we have added any assertions/declarations/definitions - * since the last checkSat/query (and therefore we're not responsible - * for an assignment). + * Whether or not we have added any assertions/declarations/definitions, + * or done push/pop, since the last checkSat/query, and therefore we're + * not responsible for models or proofs. */ bool d_problemExtended; |