Don't allow get-model & co after a user push/pop

This makes us more strictly adhere to the spec, but it's useful anyway:
previously we would support a get-model until the problem was explicitly
changed with e.g. a new assertion.  That meant you could check-sat, then
pop, then get-model, but you'd only get the part of the model still in
scope.  This is strange, and would likely lead to problems, so it's now
disabled.

Thanks to David Cok for inquiring about this.

diff --git a/NEWS b/NEWS
index b8f1177d009477e5634b6b9e34d65b3f6d867579..eb991f74ca5aecfa62711077f4a8fc80b1263abb 100644 (file)
--- a/NEWS
+++ b/NEWS
@@ -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 3ee6b1d7427ac83e7a417d708ec2e0ddf52b37ad..3cc6e7502210fdd9fd6d6c58c5b8ed35645b1e00 100644 (file)
--- 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 8266bb1edc27ab93204caace9dc2e0c4c93da2ff..1b5af415f18102e2a81bb4df7d5d07867116370d 100644 (file)
--- 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;