Remove SmtEngine::getStackLevel(), which exposed implementation details and was only...

Make SmtEngine::internalPop() delay popping.  This fixes a bug in model generation.

diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 96cef406f3ecce0d5c73c9cf5e22f43935b6694a..fafc8ccb2470324e5cf19b2dd45985e6f1b0bf64 100644 (file)
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -2228,7 +2228,7 @@ Proof ValidityChecker::getProofClosure() {
 }
 
 int ValidityChecker::stackLevel() {
-  return d_smt->getStackLevel();
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 void ValidityChecker::push() {
@@ -2240,15 +2240,7 @@ void ValidityChecker::pop() {
 }
 
 void ValidityChecker::popto(int stackLevel) {
-  CheckArgument(stackLevel >= 0, stackLevel,
-                "Cannot pop to a negative stack level %u", stackLevel);
-  CheckArgument(unsigned(stackLevel) <= d_smt->getStackLevel(), stackLevel,
-                "Cannot pop to a level higher than the current one!  "
-                "At level %u, user requested level %d",
-                d_smt->getStackLevel(), stackLevel);
-  while(unsigned(stackLevel) < d_smt->getStackLevel()) {
-    pop();
-  }
+  Unimplemented("This CVC3 compatibility function not yet implemented (sorry!)");
 }
 
 int ValidityChecker::scopeLevel() {

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 8327799449adc735d9fd69f39c97fd19445717fa..b9732c32ebe48d38c766993798a3fdda9b941781 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -143,7 +143,8 @@ class SmtEnginePrivate {
    * holds the last substitution from d_topLevelSubstitutions
    * that was pushed out to SAT.
    * If d_lastSubstitutionPos == d_topLevelSubstitutions.end(),
-   * then nothing has been pushed out yet. */
+   * then nothing has been pushed out yet.
+   */
   context::CDO<SubstitutionMap::iterator> d_lastSubstitutionPos;
 
   static const bool d_doConstantProp = true;
@@ -254,6 +255,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_assertionList(NULL),
   d_assignments(NULL),
   d_logic(),
+  d_pendingPops(0),
   d_fullyInited(false),
   d_problemExtended(false),
   d_queryMade(false),
@@ -377,6 +379,8 @@ void SmtEngine::shutdown() {
     Dump("benchmark") << QuitCommand();
   }
 
+  doPendingPops();
+
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
     d_theoryEngine->postsolve();
@@ -392,8 +396,10 @@ SmtEngine::~SmtEngine() throw() {
   SmtScope smts(this);
 
   try {
+    doPendingPops();
+
     while(options::incrementalSolving() && d_userContext->getLevel() > 1) {
-      internalPop();
+      internalPop(true);
     }
 
     shutdown();
@@ -1267,6 +1273,7 @@ void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertion
 // returns false if simpflication led to "false"
 bool SmtEnginePrivate::simplifyAssertions()
   throw(TypeCheckingException, AssertionException) {
+  Assert(d_smt.d_pendingPops == 0);
   try {
 
     Trace("simplify") << "SmtEnginePrivate::simplify()" << endl;
@@ -1348,6 +1355,7 @@ bool SmtEnginePrivate::simplifyAssertions()
 
 Result SmtEngine::check() {
   Assert(d_fullyInited);
+  Assert(d_pendingPops == 0);
 
   Trace("smt") << "SmtEngine::check()" << endl;
 
@@ -1399,6 +1407,7 @@ Result SmtEngine::quickCheck() {
 
 void SmtEnginePrivate::processAssertions() {
   Assert(d_smt.d_fullyInited);
+  Assert(d_smt.d_pendingPops == 0);
 
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
@@ -1572,6 +1581,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) throw(TypeCheckingException) {
   SmtScope smts(this);
 
   finalOptionsAreSet();
+  doPendingPops();
 
   Trace("smt") << "SmtEngine::checkSat(" << e << ")" << endl;
 
@@ -1635,6 +1645,7 @@ Result SmtEngine::query(const BoolExpr& e) throw(TypeCheckingException) {
   SmtScope smts(this);
 
   finalOptionsAreSet();
+  doPendingPops();
 
   Trace("smt") << "SMT query(" << e << ")" << endl;
 
@@ -1690,6 +1701,7 @@ Result SmtEngine::assertFormula(const BoolExpr& e) throw(TypeCheckingException)
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   Trace("smt") << "SmtEngine::assertFormula(" << e << ")" << endl;
   ensureBoolean(e);
   if(d_assertionList != NULL) {
@@ -1703,6 +1715,7 @@ Expr SmtEngine::simplify(const Expr& e) throw(TypeCheckingException) {
   Assert(e.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   if( options::typeChecking() ) {
     e.getType(true);// ensure expr is type-checked at this point
   }
@@ -1766,6 +1779,7 @@ Expr SmtEngine::getValue(const Expr& e)
 bool SmtEngine::addToAssignment(const Expr& e) throw(AssertionException) {
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   Type type = e.getType(options::typeChecking());
   // must be Boolean
   CheckArgument( type.isBoolean(), e,
@@ -1857,6 +1871,7 @@ void SmtEngine::addToModelCommand( Command* c, int c_type ){
   Trace("smt") << "SMT addToModelCommand(" << c << ", " << c_type << ")" << endl;
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   if( options::produceModels() ) {
     d_theoryEngine->getModel()->addCommand( c, c_type );
   }
@@ -1866,6 +1881,12 @@ Model* SmtEngine::getModel() throw(ModalException, AssertionException){
   Trace("smt") << "SMT getModel()" << endl;
   SmtScope smts(this);
 
+  finalOptionsAreSet();
+
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << GetModelCommand();
+  }
+
   if(d_status.isNull() ||
      d_status.asSatisfiabilityResult() == Result::UNSAT  ||
      d_problemExtended) {
@@ -1911,6 +1932,7 @@ Proof* SmtEngine::getProof() throw(ModalException, AssertionException) {
 
 vector<Expr> SmtEngine::getAssertions()
   throw(ModalException, AssertionException) {
+  finalOptionsAreSet();
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << GetAssertionsCommand();
   }
@@ -1926,15 +1948,10 @@ vector<Expr> SmtEngine::getAssertions()
   return vector<Expr>(d_assertionList->begin(), d_assertionList->end());
 }
 
-size_t SmtEngine::getStackLevel() const {
-  SmtScope smts(this);
-  Trace("smt") << "SMT getStackLevel()" << endl;
-  return d_context->getLevel();
-}
-
 void SmtEngine::push() {
   SmtScope smts(this);
   finalOptionsAreSet();
+  doPendingPops();
   Trace("smt") << "SMT push()" << endl;
   d_private->processAssertions();
   if(Dump.isOn("benchmark")) {
@@ -1978,7 +1995,7 @@ void SmtEngine::pop() {
 
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
-    internalPop();
+    internalPop(true);
   }
   d_userLevels.pop_back();
 
@@ -1996,6 +2013,7 @@ void SmtEngine::pop() {
 void SmtEngine::internalPush() {
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPush()" << endl;
+  doPendingPops();
   if(options::incrementalSolving()) {
     d_private->processAssertions();
     d_userContext->push();
@@ -2004,13 +2022,24 @@ void SmtEngine::internalPush() {
   }
 }
 
-void SmtEngine::internalPop() {
+void SmtEngine::internalPop(bool immediate) {
   Assert(d_fullyInited);
   Trace("smt") << "SmtEngine::internalPop()" << endl;
   if(options::incrementalSolving()) {
+    ++d_pendingPops;
+  }
+  if(immediate) {
+    doPendingPops();
+  }
+}
+
+void SmtEngine::doPendingPops() {
+  Assert(d_pendingPops == 0 || options::incrementalSolving());
+  while(d_pendingPops > 0) {
     d_propEngine->pop();
     d_context->pop();
     d_userContext->pop();
+    --d_pendingPops;
   }
 }
 

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 23481424523c01a683121cb261c50f9ed5950ff8..2c99bc7eb3b09032bfb1ed9206f07379fdead19c 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -134,6 +134,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
@@ -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
@@ -414,11 +421,6 @@ public:
    */
   std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
 
-  /**
-   * Get the current context level.
-   */
-  size_t getStackLevel() const;
-
   /**
    * Push a user-level context.
    */

diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index aafe1fa1c0cce5629b841c5def9d27836962cc7d..b8c2a2f481a3463b2adbb1b26221cdce19798493 100644 (file)
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -48,7 +48,8 @@ SMT2_TESTS = \
        simple-rdl.smt2 \
        simple-uf.smt2 \
        simplification_bug4.smt2 \
-       parallel-let.smt2
+       parallel-let.smt2 \
+       get-value-incremental.smt2
 
 # Regression tests for PL inputs
 CVC_TESTS = \

diff --git a/test/regress/regress0/get-value-incremental.smt2 b/test/regress/regress0/get-value-incremental.smt2
new file mode 100644 (file)
index 0000000..a3f3e3f
--- /dev/null
+++ b/test/regress/regress0/get-value-incremental.smt2
@@ -0,0 +1,14 @@
+; COMMAND-LINE: --incremental
+; EXPECT: sat
+; EXPECT: (((f 0) 1))
+; EXIT: 10
+(set-info :smt-lib-version 2.0)
+(set-option :produce-models true)
+(set-logic QF_UFLIA)
+
+(declare-fun f (Int) Int)
+(assert (= (f 0) 1))
+(check-sat)
+(get-value ((f 0)))
+; add a "push" just to double-check that incremental mode is on
+(push)