From 84a3411720a59410c7dff7bc8ec9210638b7665b Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Thu, 6 Sep 2012 02:38:39 +0000 Subject: [PATCH] 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. --- src/compat/cvc3_compat.cpp | 12 +---- src/smt/smt_engine.cpp | 49 +++++++++++++++---- src/smt/smt_engine.h | 14 +++--- test/regress/regress0/Makefile.am | 3 +- .../regress0/get-value-incremental.smt2 | 14 ++++++ 5 files changed, 65 insertions(+), 27 deletions(-) create mode 100644 test/regress/regress0/get-value-incremental.smt2 diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp index 96cef406f..fafc8ccb2 100644 --- 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 832779944..b9732c32e 100644 --- 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 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& 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 SmtEngine::getAssertions() throw(ModalException, AssertionException) { + finalOptionsAreSet(); if(Dump.isOn("benchmark")) { Dump("benchmark") << GetAssertionsCommand(); } @@ -1926,15 +1948,10 @@ vector SmtEngine::getAssertions() return vector(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 234814245..2c99bc7eb 100644 --- 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 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 aafe1fa1c..b8c2a2f48 100644 --- 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 index 000000000..a3f3e3fce --- /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) -- 2.30.2