From 43839eed3814cb4175869cd1fbbb4e9a5ece59dc Mon Sep 17 00:00:00 2001 From: Clark Barrett Date: Fri, 15 Jun 2012 03:24:51 +0000 Subject: [PATCH] Fix for incompleteness bug with decision engine: repeated simplification could introduce additional assertions that were not beign processed by the decision engine. Now these assertions are merged in with pre-ITE-removal assertions, ensuring the decision engine sees them. --- src/smt/smt_engine.cpp | 92 ++++++++++++++++-------- src/theory/booleans/circuit_propagator.h | 24 +++++-- 2 files changed, 79 insertions(+), 37 deletions(-) diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index bfff22863..7492be465 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -116,6 +116,9 @@ class SmtEnginePrivate { /** Learned literals */ vector d_nonClausalLearnedLiterals; + /** Size of assertions array when preprocessing starts */ + unsigned d_realAssertionsEnd; + /** A circuit propagator for non-clausal propositional deduction */ booleans::CircuitPropagator d_propagator; @@ -188,7 +191,7 @@ public: SmtEnginePrivate(SmtEngine& smt) : d_smt(smt), d_nonClausalLearnedLiterals(), - d_propagator(smt.d_userContext, d_nonClausalLearnedLiterals, true, true), + d_propagator(d_nonClausalLearnedLiterals, true, true), d_topLevelSubstitutions(smt.d_userContext), d_lastSubstitutionPos(smt.d_userContext, d_topLevelSubstitutions.end()) { } @@ -903,15 +906,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify()" << endl; - // Apply the substitutions we already have, and normalize - Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " - << "applying substitutions" << endl; - for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { - Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl; - d_assertionsToPreprocess[i] = - theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); - Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; - } + d_propagator.initialize(); // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " @@ -929,6 +924,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << "conflict in non-clausal propagation" << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + d_propagator.finish(); return false; } @@ -962,6 +958,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << d_nonClausalLearnedLiterals[i] << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + d_propagator.finish(); return false; } } @@ -993,6 +990,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { << learnedLiteral << endl; d_assertionsToPreprocess.clear(); d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst(false)); + d_propagator.finish(); return false; default: if (d_doConstantProp && learnedLiteral.getKind() == kind::EQUAL && (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) { @@ -1105,6 +1103,9 @@ bool SmtEnginePrivate::nonClausalSimplify() { } d_assertionsToPreprocess.clear(); + NodeBuilder<> learnedBuilder(kind::AND); + learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd-1]; + for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { Node learned = d_nonClausalLearnedLiterals[i]; Node learnedNew = d_topLevelSubstitutions.apply(learned); @@ -1123,10 +1124,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { continue; } s.insert(learned); - d_assertionsToCheck.push_back(learned); + learnedBuilder << learned; Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal learned : " - << d_assertionsToCheck.back() << endl; + << learned << endl; } d_nonClausalLearnedLiterals.clear(); @@ -1137,12 +1138,17 @@ bool SmtEnginePrivate::nonClausalSimplify() { continue; } s.insert(cProp); - d_assertionsToCheck.push_back(cProp); + learnedBuilder << cProp; Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "non-clausal constant propagation : " - << d_assertionsToCheck.back() << endl; + << cProp << endl; } + if(learnedBuilder.getNumChildren() > 1) { + d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(learnedBuilder)); + } + + d_propagator.finish(); return true; } @@ -1237,10 +1243,7 @@ bool SmtEnginePrivate::simplifyAssertions() // Perform non-clausal simplification Trace("simplify") << "SmtEnginePrivate::simplify(): " << "performing non-clausal simplification" << endl; - // Abuse the user context to make sure circuit propagator gets backtracked - d_smt.d_userContext->push(); bool noConflict = nonClausalSimplify(); - d_smt.d_userContext->pop(); if(!noConflict) return false; } else { Assert(d_assertionsToCheck.empty()); @@ -1287,10 +1290,7 @@ bool SmtEnginePrivate::simplifyAssertions() Trace("simplify") << "SmtEnginePrivate::simplify(): " << " doing repeated simplification" << std::endl; d_assertionsToCheck.swap(d_assertionsToPreprocess); - // Abuse the user context to make sure circuit propagator gets backtracked - d_smt.d_userContext->push(); bool noConflict = nonClausalSimplify(); - d_smt.d_userContext->pop(); if(!noConflict) return false; } @@ -1373,7 +1373,10 @@ void SmtEnginePrivate::processAssertions() { Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; // any assertions added beyond realAssertionsEnd must NOT affect the equisatisfiability - int realAssertionsEnd = d_assertionsToPreprocess.size(); + d_realAssertionsEnd = d_assertionsToPreprocess.size(); + if (d_realAssertionsEnd == 0) { + return; + } // Any variables of subtype types need to be constrained properly. // Careful, here: constrainSubtypes() adds to the back of @@ -1397,6 +1400,16 @@ void SmtEnginePrivate::processAssertions() { } } + // Apply the substitutions we already have, and normalize + Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " + << "applying substitutions" << endl; + for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) { + Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl; + d_assertionsToPreprocess[i] = + theory::Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i])); + Trace("simplify") << " got " << d_assertionsToPreprocess[i] << endl; + } + bool noConflict = simplifyAssertions(); if(Options::current()->doStaticLearning) { @@ -1414,21 +1427,40 @@ void SmtEnginePrivate::processAssertions() { d_smt.d_numAssertionsPost += d_assertionsToCheck.size(); } + // begin: INVARIANT to maintain: no reordering of assertions or + // introducing new ones +#ifdef CVC4_ASSERTIONS + unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); +#endif + if(Options::current()->repeatSimp) { d_assertionsToCheck.swap(d_assertionsToPreprocess); noConflict &= simplifyAssertions(); - removeITEs(); + if (noConflict) { + // Some skolem variables may have been solved for - which is a good thing - + // but it means we have to move those ITE's back to the main set of assertions + IteSkolemMap::iterator it = d_iteSkolemMap.begin(); + IteSkolemMap::iterator iend = d_iteSkolemMap.end(); + NodeBuilder<> builder(kind::AND); + builder << d_assertionsToCheck[d_realAssertionsEnd-1]; + for (; it != iend; ++it) { + if (d_topLevelSubstitutions.hasSubstitution((*it).first)) { + builder << d_assertionsToCheck[(*it).second]; + d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst(true); + } + } + if(builder.getNumChildren() > 1) { + d_assertionsToCheck[d_realAssertionsEnd-1] = Rewriter::rewrite(Node(builder)); + } + // TODO: remove this - need to double-check it's not needed + removeITEs(); + Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); + } } Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; - // begin: INVARIANT to maintain: no reordering of assertions or - // introducing new ones -#ifdef CVC4_ASSERTIONS - unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size(); -#endif - Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl; Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl; Debug("smt") << " d_assertionsToCheck : " << d_assertionsToCheck.size() << endl; @@ -1451,10 +1483,10 @@ void SmtEnginePrivate::processAssertions() { } // Push the formula to decision engine - Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); if(noConflict) { + Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size()); d_smt.d_decisionEngine->addAssertions - (d_assertionsToCheck, realAssertionsEnd, d_iteSkolemMap); + (d_assertionsToCheck, d_realAssertionsEnd, d_iteSkolemMap); } // end: INVARIANT to maintain: no reordering of assertions or diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 60e48dba2..796bc9e21 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -68,6 +68,8 @@ public: private: + context::Context d_context; + /** The propagation queue */ std::vector d_propagationQueue; @@ -234,21 +236,29 @@ public: /** * Construct a new CircuitPropagator. */ - CircuitPropagator(context::Context* context, std::vector& outLearnedLiterals, + CircuitPropagator(std::vector& outLearnedLiterals, bool enableForward = true, bool enableBackward = true) : + d_context(), d_propagationQueue(), - d_propagationQueueClearer(context, d_propagationQueue), - d_conflict(context, false), + d_propagationQueueClearer(&d_context, d_propagationQueue), + d_conflict(&d_context, false), d_learnedLiterals(outLearnedLiterals), - d_learnedLiteralClearer(context, outLearnedLiterals), + d_learnedLiteralClearer(&d_context, outLearnedLiterals), d_backEdges(), - d_backEdgesClearer(context, d_backEdges), - d_seen(context), - d_state(context), + d_backEdgesClearer(&d_context, d_backEdges), + d_seen(&d_context), + d_state(&d_context), d_forwardPropagation(enableForward), d_backwardPropagation(enableBackward) { } + // Use custom context to ensure propagator is reset after use + void initialize() + { d_context.push(); } + + void finish() + { d_context.pop(); } + /** Assert for propagation */ void assert(TNode assertion); -- 2.30.2