From: Mathias Preiner Date: Tue, 21 Aug 2018 20:33:01 +0000 (-0700) Subject: Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350) X-Git-Tag: cvc5-1.0.0~4748 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d98ea67b5d85c0f70f6dfffa0b61353160e2736b;p=cvc5.git Move d_realAssertionsEnd from SmtEnginePrivate to AssertionPipeline. (#2350) --- diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 97b05802d..6a7078696 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -25,7 +25,9 @@ namespace CVC4 { namespace preprocessing { AssertionPipeline::AssertionPipeline(context::Context* context) - : d_substitutionsIndex(context, 0), d_topLevelSubstitutions(context) + : d_substitutionsIndex(context, 0), + d_topLevelSubstitutions(context), + d_realAssertionsEnd(0) { } diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index 6f76b60e9..97fa32d17 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -56,7 +56,12 @@ class AssertionPipeline size_t size() const { return d_nodes.size(); } void resize(size_t n) { d_nodes.resize(n); } - void clear() { d_nodes.clear(); } + + void clear() + { + d_nodes.clear(); + d_realAssertionsEnd = 0; + } Node& operator[](size_t i) { return d_nodes[i]; } const Node& operator[](size_t i) const { return d_nodes[i]; } @@ -99,6 +104,10 @@ class AssertionPipeline return d_topLevelSubstitutions; } + size_t getRealAssertionsEnd() { return d_realAssertionsEnd; } + + void updateRealAssertionsEnd() { d_realAssertionsEnd = d_nodes.size(); } + private: std::vector d_nodes; @@ -107,12 +116,15 @@ class AssertionPipeline * corresponding introduced Boolean ite */ IteSkolemMap d_iteSkolemMap; - + /* Index for where to store substitutions */ context::CDO d_substitutionsIndex; /* The top level substitutions */ theory::SubstitutionMap d_topLevelSubstitutions; + + /** Size of d_nodes when preprocessing starts */ + size_t d_realAssertionsEnd; }; /* class AssertionPipeline */ /** diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index cabe825be..fbe6bcd63 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -502,9 +502,6 @@ class SmtEnginePrivate : public NodeManagerListener { /** 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; bool d_propagatorNeedsFinish; @@ -640,7 +637,6 @@ class SmtEnginePrivate : public NodeManagerListener { d_managedReplayLog(), d_listenerRegistrations(new ListenerRegistrationList()), d_nonClausalLearnedLiterals(), - d_realAssertionsEnd(0), d_propagator(d_nonClausalLearnedLiterals, true, true), d_propagatorNeedsFinish(false), d_assertions(d_smt.d_userContext), @@ -815,7 +811,6 @@ class SmtEnginePrivate : public NodeManagerListener { void notifyPop() { d_assertions.clear(); d_nonClausalLearnedLiterals.clear(); - d_realAssertionsEnd = 0; getIteSkolemMap().clear(); } @@ -3260,8 +3255,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { } NodeBuilder<> learnedBuilder(kind::AND); - Assert(d_realAssertionsEnd <= d_assertions.size()); - learnedBuilder << d_assertions[d_realAssertionsEnd - 1]; + Assert(d_assertions.getRealAssertionsEnd() <= d_assertions.size()); + learnedBuilder << d_assertions[d_assertions.getRealAssertionsEnd() - 1]; for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { Node learned = d_nonClausalLearnedLiterals[i]; @@ -3314,8 +3309,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { top_level_substs.addSubstitutions(newSubstitutions); if(learnedBuilder.getNumChildren() > 1) { - d_assertions.replace(d_realAssertionsEnd - 1, - Rewriter::rewrite(Node(learnedBuilder))); + d_assertions.replace(d_assertions.getRealAssertionsEnd() - 1, + Rewriter::rewrite(Node(learnedBuilder))); } d_propagatorNeedsFinish = true; @@ -3347,21 +3342,21 @@ bool SmtEnginePrivate::simpITE() { void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ size_t curr = d_assertions.size(); - if(before >= curr || - d_realAssertionsEnd <= 0 || - d_realAssertionsEnd >= curr){ + if (before >= curr || d_assertions.getRealAssertionsEnd() <= 0 + || d_assertions.getRealAssertionsEnd() >= curr) + { return; } // assertions - // original: [0 ... d_realAssertionsEnd) + // original: [0 ... d_assertions.getRealAssertionsEnd()) // can be modified - // ites skolems [d_realAssertionsEnd, before) + // ites skolems [d_assertions.getRealAssertionsEnd(), before) // cannot be moved // added [before, curr) // can be modified - Assert(0 < d_realAssertionsEnd); - Assert(d_realAssertionsEnd <= before); + Assert(0 < d_assertions.getRealAssertionsEnd()); + Assert(d_assertions.getRealAssertionsEnd() <= before); Assert(before < curr); std::vector intoConjunction; @@ -3369,7 +3364,7 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){ intoConjunction.push_back(d_assertions[i]); } d_assertions.resize(before); - size_t lastBeforeItes = d_realAssertionsEnd - 1; + size_t lastBeforeItes = d_assertions.getRealAssertionsEnd() - 1; intoConjunction.push_back(d_assertions[lastBeforeItes]); Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction); d_assertions.replace(lastBeforeItes, newLast); @@ -3448,7 +3443,7 @@ size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::unordered_set } void SmtEnginePrivate::doMiplibTrick() { - Assert(d_realAssertionsEnd == d_assertions.size()); + Assert(d_assertions.getRealAssertionsEnd() == d_assertions.size()); Assert(!options::incrementalSolving()); const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges(); @@ -3746,7 +3741,8 @@ void SmtEnginePrivate::doMiplibTrick() { } if(!removeAssertions.empty()) { Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl; - for(size_t i = 0; i < d_realAssertionsEnd; ++i) { + for (size_t i = 0; i < d_assertions.getRealAssertionsEnd(); ++i) + { if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) { Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl; d_assertions[i] = d_true; @@ -3767,7 +3763,7 @@ void SmtEnginePrivate::doMiplibTrick() { } else { Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl; } - d_realAssertionsEnd = d_assertions.size(); + d_assertions.updateRealAssertionsEnd(); } @@ -3795,16 +3791,17 @@ bool SmtEnginePrivate::simplifyAssertions() // We piggy-back off of the BackEdgesMap in the CircuitPropagator to // do the miplib trick. - if( // check that option is on + if ( // check that option is on options::arithMLTrick() && // miplib rewrites aren't safe in incremental mode - ! options::incrementalSolving() && + !options::incrementalSolving() && // only useful in arith d_smt.d_logic.isTheoryEnabled(THEORY_ARITH) && // we add new assertions and need this (in practice, this // restriction only disables miplib processing during // re-simplification, which we don't expect to be useful anyway) - d_realAssertionsEnd == d_assertions.size() ) { + d_assertions.getRealAssertionsEnd() == d_assertions.size()) + { Chat() << "...fixing miplib encodings..." << endl; Trace("simplify") << "SmtEnginePrivate::simplify(): " << "looking for miplib pseudobooleans..." << endl; @@ -4057,7 +4054,7 @@ void SmtEnginePrivate::processAssertions() { d_assertions.push_back(NodeManager::currentNM()->mkConst(true)); // any assertions added beyond realAssertionsEnd must NOT affect the // equisatisfiability - d_realAssertionsEnd = d_assertions.size(); + d_assertions.updateRealAssertionsEnd(); // Assertions are NOT guaranteed to be rewritten by this point @@ -4337,7 +4334,7 @@ void SmtEnginePrivate::processAssertions() { IteSkolemMap::iterator it = getIteSkolemMap().begin(); IteSkolemMap::iterator iend = getIteSkolemMap().end(); NodeBuilder<> builder(kind::AND); - builder << d_assertions[d_realAssertionsEnd - 1]; + builder << d_assertions[d_assertions.getRealAssertionsEnd() - 1]; vector toErase; for (; it != iend; ++it) { if (skolemSet.find((*it).first) == skolemSet.end()) { @@ -4366,7 +4363,8 @@ void SmtEnginePrivate::processAssertions() { getIteSkolemMap().erase(toErase.back()); toErase.pop_back(); } - d_assertions[d_realAssertionsEnd - 1] = Rewriter::rewrite(Node(builder)); + d_assertions[d_assertions.getRealAssertionsEnd() - 1] = + Rewriter::rewrite(Node(builder)); } // TODO(b/1256): For some reason this is needed for some benchmarks, such as // QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2 @@ -4420,8 +4418,9 @@ void SmtEnginePrivate::processAssertions() { if(noConflict) { Chat() << "pushing to decision engine..." << endl; Assert(iteRewriteAssertionsEnd == d_assertions.size()); - d_smt.d_decisionEngine->addAssertions( - d_assertions.ref(), d_realAssertionsEnd, getIteSkolemMap()); + d_smt.d_decisionEngine->addAssertions(d_assertions.ref(), + d_assertions.getRealAssertionsEnd(), + getIteSkolemMap()); } // end: INVARIANT to maintain: no reordering of assertions or