diff options
Diffstat (limited to 'src/smt/smt_engine.cpp')
-rw-r--r-- | src/smt/smt_engine.cpp | 205 |
1 files changed, 99 insertions, 106 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index c21a0b4c2..1705cd0a3 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -68,6 +68,7 @@ #include "options/strings_options.h" #include "options/theory_options.h" #include "options/uf_options.h" +#include "preprocessing/passes/apply_substs.h" #include "preprocessing/passes/bool_to_bv.h" #include "preprocessing/passes/bv_abstraction.h" #include "preprocessing/passes/bv_ackermann.h" @@ -522,9 +523,6 @@ class SmtEnginePrivate : public NodeManagerListener { /** Whether any assertions have been processed */ CDO<bool> d_assertionsProcessed; - /** Index for where to store substitutions */ - CDO<unsigned> d_substitutionsIndex; - // Cached true value Node d_true; @@ -576,9 +574,6 @@ public: std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext; PreprocessingPassRegistry d_preprocessingPassRegistry; - /** The top level substitutions */ - SubstitutionMap d_topLevelSubstitutions; - static const bool d_doConstantProp = true; /** @@ -653,30 +648,27 @@ public: bool simplifyAssertions(); public: - - SmtEnginePrivate(SmtEngine& smt) : - d_smt(smt), - d_managedRegularChannel(), - d_managedDiagnosticChannel(), - d_managedDumpChannel(), - d_managedReplayLog(), - d_listenerRegistrations(new ListenerRegistrationList()), - d_nonClausalLearnedLiterals(), - d_realAssertionsEnd(0), - d_propagator(d_nonClausalLearnedLiterals, true, true), - d_propagatorNeedsFinish(false), - d_assertions(), - d_assertionsProcessed(smt.d_userContext, false), - d_substitutionsIndex(smt.d_userContext, 0), - d_fakeContext(), - d_abstractValueMap(&d_fakeContext), - d_abstractValues(), - d_simplifyAssertionsDepth(0), - //d_needsExpandDefs(true), //TODO? - d_exprNames(smt.d_userContext), - d_iteSkolemMap(), - d_iteRemover(smt.d_userContext), - d_topLevelSubstitutions(smt.d_userContext) + SmtEnginePrivate(SmtEngine& smt) + : d_smt(smt), + d_managedRegularChannel(), + d_managedDiagnosticChannel(), + d_managedDumpChannel(), + 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), + d_assertionsProcessed(smt.d_userContext, false), + d_fakeContext(), + d_abstractValueMap(&d_fakeContext), + d_abstractValues(), + d_simplifyAssertionsDepth(0), + // d_needsExpandDefs(true), //TODO? + d_exprNames(smt.d_userContext), + d_iteSkolemMap(), + d_iteRemover(smt.d_userContext) { d_smt.d_nodeManager->subscribeEvents(this); d_true = NodeManager::currentNM()->mkConst(true); @@ -811,17 +803,13 @@ public: void nmNotifyDeleteNode(TNode n) override {} - Node applySubstitutions(TNode node) const { - return Rewriter::rewrite(d_topLevelSubstitutions.apply(node)); + Node applySubstitutions(TNode node) + { + return Rewriter::rewrite( + d_assertions.getTopLevelSubstitutions().apply(node)); } /** - * Apply the substitutions in d_topLevelAssertions and the rewriter to each of - * the assertions in d_assertions, and store the result back in d_assertions. - */ - void applySubstitutionsToAssertions(); - - /** * Process the assertions that have been asserted. */ void processAssertions(); @@ -2703,10 +2691,14 @@ bool SmtEngine::isDefinedFunction( Expr func ){ return d_definedFunctions->find(nf) != d_definedFunctions->end(); } -void SmtEnginePrivate::finishInit() { - d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt)); +void SmtEnginePrivate::finishInit() +{ + d_preprocessingPassContext.reset( + new PreprocessingPassContext(&d_smt, d_resourceManager)); // TODO: register passes here (this will likely change when we add support for // actually assembling preprocessing pipelines). + std::unique_ptr<ApplySubsts> applySubsts( + new ApplySubsts(d_preprocessingPassContext.get())); std::unique_ptr<BoolToBV> boolToBv( new BoolToBV(d_preprocessingPassContext.get())); std::unique_ptr<BvAbstraction> bvAbstract( @@ -2731,6 +2723,8 @@ void SmtEnginePrivate::finishInit() { new SymBreakerPass(d_preprocessingPassContext.get())); std::unique_ptr<SynthRewRulesPass> srrProc( new SynthRewRulesPass(d_preprocessingPassContext.get())); + d_preprocessingPassRegistry.registerPass("apply-substs", + std::move(applySubsts)); d_preprocessingPassRegistry.registerPass("bool-to-bv", std::move(boolToBv)); d_preprocessingPassRegistry.registerPass("bv-abstraction", std::move(bvAbstract)); @@ -3024,10 +3018,12 @@ bool SmtEnginePrivate::nonClausalSimplify() { // Assert all the assertions to the propagator Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): " << "asserting to propagator" << endl; + CDO<unsigned>& substs_index = d_assertions.getSubstitutionsIndex(); for (unsigned i = 0; i < d_assertions.size(); ++ i) { Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]); // Don't reprocess substitutions - if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) { + if (substs_index > 0 && i == substs_index) + { continue; } Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl; @@ -3052,6 +3048,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "Iterate through " << d_nonClausalLearnedLiterals.size() << " learned literals." << std::endl; // No conflict, go through the literals and solve them + SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); SubstitutionMap constantPropagations(d_smt.d_context); SubstitutionMap newSubstitutions(d_smt.d_context); SubstitutionMap::iterator pos; @@ -3060,7 +3057,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // Simplify the literal we learned wrt previous substitutions Node learnedLiteral = d_nonClausalLearnedLiterals[i]; Assert(Rewriter::rewrite(learnedLiteral) == learnedLiteral); - Assert(d_topLevelSubstitutions.apply(learnedLiteral) == learnedLiteral); + Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral); Trace("simplify") << "Process learnedLiteral : " << learnedLiteral << std::endl; Node learnedLiteralNew = newSubstitutions.apply(learnedLiteral); if (learnedLiteral != learnedLiteralNew) { @@ -3109,11 +3106,13 @@ bool SmtEnginePrivate::nonClausalSimplify() { << "solved " << learnedLiteral << endl; Assert(Rewriter::rewrite(newSubstitutions.apply(learnedLiteral)).isConst()); // vector<pair<Node, Node> > equations; - // constantPropagations.simplifyLHS(d_topLevelSubstitutions, equations, true); - // if (equations.empty()) { + // constantPropagations.simplifyLHS(top_level_substs, equations, + // true); if (equations.empty()) { // break; // } - // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); + // Assert(equations[0].first.isConst() && + // equations[0].second.isConst() && equations[0].first != + // equations[0].second); // else fall through break; } @@ -3142,18 +3141,19 @@ bool SmtEnginePrivate::nonClausalSimplify() { } Assert(!t.isConst()); Assert(constantPropagations.apply(t) == t); - Assert(d_topLevelSubstitutions.apply(t) == t); + Assert(top_level_substs.apply(t) == t); Assert(newSubstitutions.apply(t) == t); constantPropagations.addSubstitution(t, c); // vector<pair<Node,Node> > equations; // constantPropagations.simplifyLHS(t, c, equations, true); // if (!equations.empty()) { - // Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second); - // d_assertions.clear(); - // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, false); - // return; + // Assert(equations[0].first.isConst() && + // equations[0].second.isConst() && equations[0].first != + // equations[0].second); d_assertions.clear(); + // addFormula(NodeManager::currentNM()->mkConst<bool>(false), false, + // false); return; // } - // d_topLevelSubstitutions.simplifyRHS(constantPropagations); + // top_level_substs.simplifyRHS(constantPropagations); } else { // Keep the literal @@ -3169,31 +3169,35 @@ bool SmtEnginePrivate::nonClausalSimplify() { // because it is costly for certain inputs (see bug 508). // // Check data structure invariants: - // 1. for each lhs of d_topLevelSubstitutions, does not appear anywhere in rhs of d_topLevelSubstitutions or anywhere in constantPropagations + // 1. for each lhs of top_level_substs, does not appear anywhere in rhs of + // top_level_substs or anywhere in constantPropagations // 2. each lhs of constantPropagations rewrites to itself - // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> r' another constant propagation, then l'[l/r] -> r' should be a + // 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> + // r' another constant propagation, then l'[l/r] -> r' should be a // constant propagation too // 4. each lhs of constantPropagations is different from each rhs for (pos = newSubstitutions.begin(); pos != newSubstitutions.end(); ++pos) { Assert((*pos).first.isVar()); - Assert(d_topLevelSubstitutions.apply((*pos).first) == (*pos).first); - Assert(d_topLevelSubstitutions.apply((*pos).second) == (*pos).second); + Assert(top_level_substs.apply((*pos).first) == (*pos).first); + Assert(top_level_substs.apply((*pos).second) == (*pos).second); Assert(newSubstitutions.apply(newSubstitutions.apply((*pos).second)) == newSubstitutions.apply((*pos).second)); } for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { Assert((*pos).second.isConst()); Assert(Rewriter::rewrite((*pos).first) == (*pos).first); - // Node newLeft = d_topLevelSubstitutions.apply((*pos).first); + // Node newLeft = top_level_substs.apply((*pos).first); // if (newLeft != (*pos).first) { // newLeft = Rewriter::rewrite(newLeft); // Assert(newLeft == (*pos).second || - // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // (constantPropagations.hasSubstitution(newLeft) && + // constantPropagations.apply(newLeft) == (*pos).second)); // } // newLeft = constantPropagations.apply((*pos).first); // if (newLeft != (*pos).first) { // newLeft = Rewriter::rewrite(newLeft); // Assert(newLeft == (*pos).second || - // (constantPropagations.hasSubstitution(newLeft) && constantPropagations.apply(newLeft) == (*pos).second)); + // (constantPropagations.hasSubstitution(newLeft) && + // constantPropagations.apply(newLeft) == (*pos).second)); // } Assert(constantPropagations.apply((*pos).second) == (*pos).second); } @@ -3234,9 +3238,10 @@ bool SmtEnginePrivate::nonClausalSimplify() { } // If in incremental mode, add substitutions to the list of assertions - if (d_substitutionsIndex > 0) { + if (substs_index > 0) + { NodeBuilder<> substitutionsBuilder(kind::AND); - substitutionsBuilder << d_assertions[d_substitutionsIndex]; + substitutionsBuilder << d_assertions[substs_index]; pos = newSubstitutions.begin(); for (; pos != newSubstitutions.end(); ++pos) { // Add back this substitution as an assertion @@ -3246,8 +3251,8 @@ bool SmtEnginePrivate::nonClausalSimplify() { Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl; } if (substitutionsBuilder.getNumChildren() > 1) { - d_assertions.replace(d_substitutionsIndex, - Rewriter::rewrite(Node(substitutionsBuilder))); + d_assertions.replace(substs_index, + Rewriter::rewrite(Node(substitutionsBuilder))); } } else { // If not in incremental mode, must add substitutions to model @@ -3268,7 +3273,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) { Node learned = d_nonClausalLearnedLiterals[i]; - Assert(d_topLevelSubstitutions.apply(learned) == learned); + Assert(top_level_substs.apply(learned) == learned); Node learnedNew = newSubstitutions.apply(learned); if (learned != learnedNew) { learned = Rewriter::rewrite(learnedNew); @@ -3295,7 +3300,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) { Node cProp = (*pos).first.eqNode((*pos).second); - Assert(d_topLevelSubstitutions.apply(cProp) == cProp); + Assert(top_level_substs.apply(cProp) == cProp); Node cPropNew = newSubstitutions.apply(cProp); if (cProp != cPropNew) { cProp = Rewriter::rewrite(cPropNew); @@ -3314,7 +3319,7 @@ bool SmtEnginePrivate::nonClausalSimplify() { // Add new substitutions to topLevelSubstitutions // Note that we don't have to keep rhs's in full solved form // because SubstitutionMap::apply does a fixed-point iteration when substituting - d_topLevelSubstitutions.addSubstitutions(newSubstitutions); + top_level_substs.addSubstitutions(newSubstitutions); if(learnedBuilder.getNumChildren() > 1) { d_assertions.replace(d_realAssertionsEnd - 1, @@ -3460,6 +3465,7 @@ void SmtEnginePrivate::doMiplibTrick() { NodeManager* nm = NodeManager::currentNM(); Node zero = nm->mkConst(Rational(0)), one = nm->mkConst(Rational(1)); + SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); unordered_map<TNode, Node, TNodeHashFunction> intVars; for(vector<Node>::const_iterator i = d_boolVars.begin(); i != d_boolVars.end(); ++i) { if(d_propagator.isAssigned(*i)) { @@ -3720,13 +3726,16 @@ void SmtEnginePrivate::doMiplibTrick() { Debug("miplib") << "vars[] " << var << endl << " eq " << Rewriter::rewrite(sum) << endl; Node newAssertion = var.eqNode(Rewriter::rewrite(sum)); - if(d_topLevelSubstitutions.hasSubstitution(newAssertion[0])) { - //Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; - //Warning() << "REPLACE " << newAssertion[1] << endl; - //Warning() << "ORIG " << d_topLevelSubstitutions.getSubstitution(newAssertion[0]) << endl; - Assert(d_topLevelSubstitutions.getSubstitution(newAssertion[0]) == newAssertion[1]); + if (top_level_substs.hasSubstitution(newAssertion[0])) + { + // Warning() << "RE-SUBSTITUTION " << newAssertion[0] << endl; + // Warning() << "REPLACE " << newAssertion[1] << endl; + // Warning() << "ORIG " << + // top_level_substs.getSubstitution(newAssertion[0]) << endl; + Assert(top_level_substs.getSubstitution(newAssertion[0]) + == newAssertion[1]); } else if(pos.getNumChildren() <= options::arithMLTrickSubstitutions()) { - d_topLevelSubstitutions.addSubstitution(newAssertion[0], newAssertion[1]); + top_level_substs.addSubstitution(newAssertion[0], newAssertion[1]); Debug("miplib") << "addSubs: " << newAssertion[0] << " to " << newAssertion[1] << endl; } else { Debug("miplib") << "skipSubs: " << newAssertion[0] << " to " << newAssertion[1] << " (threshold is " << options::arithMLTrickSubstitutions() << ")" << endl; @@ -3759,7 +3768,8 @@ void SmtEnginePrivate::doMiplibTrick() { } } Debug("miplib") << "had: " << d_assertions[i] << endl; - d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])); + d_assertions[i] = + Rewriter::rewrite(top_level_substs.apply(d_assertions[i])); Debug("miplib") << "now: " << d_assertions[i] << endl; } } else { @@ -4013,35 +4023,12 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<N return false; } -void SmtEnginePrivate::applySubstitutionsToAssertions() { - if(!options::unsatCores()) { - Chat() << "applying substitutions..." << endl; - Trace("simplify") << "SmtEnginePrivate::processAssertions(): " - << "applying substitutions" << endl; - // TODO(b/1255): Substitutions in incremental mode should be managed with a - // proper data structure. - - // When solving incrementally, all substitutions are piled into the - // assertion at d_substitutionsIndex: we don't want to apply substitutions - // to this assertion or information will be lost. - unsigned substitutionAssertion = d_substitutionsIndex > 0 ? d_substitutionsIndex : d_assertions.size(); - for (unsigned i = 0; i < d_assertions.size(); ++ i) { - if (i == substitutionAssertion) { - continue; - } - Trace("simplify") << "applying to " << d_assertions[i] << endl; - spendResource(options::preprocessStep()); - d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]))); - Trace("simplify") << " got " << d_assertions[i] << endl; - } - } -} - void SmtEnginePrivate::processAssertions() { TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime); spendResource(options::preprocessStep()); Assert(d_smt.d_fullyInited); Assert(d_smt.d_pendingPops == 0); + SubstitutionMap& top_level_substs = d_assertions.getTopLevelSubstitutions(); // Dump the assertions dumpAssertions("pre-everything", d_assertions); @@ -4067,7 +4054,7 @@ void SmtEnginePrivate::processAssertions() { // proper data structure. // Placeholder for storing substitutions - d_substitutionsIndex = d_assertions.size(); + d_assertions.getSubstitutionsIndex() = d_assertions.size(); d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true)); } @@ -4199,13 +4186,18 @@ void SmtEnginePrivate::processAssertions() { Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-substitution" << endl; dumpAssertions("pre-substitution", d_assertions); - if(options::unsatCores()) { - // special rewriting pass for unsat cores, since many of the passes below are skipped - for (unsigned i = 0; i < d_assertions.size(); ++ i) { + if (options::unsatCores()) + { + // special rewriting pass for unsat cores, since many of the passes below + // are skipped + for (unsigned i = 0; i < d_assertions.size(); ++i) + { d_assertions.replace(i, Rewriter::rewrite(d_assertions[i])); } - } else { - applySubstitutionsToAssertions(); + } + else + { + d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-substitution" << endl; dumpAssertions("post-substitution", d_assertions); @@ -4367,7 +4359,7 @@ void SmtEnginePrivate::processAssertions() { // This is needed because when solving incrementally, removeITEs may introduce // skolems that were solved for earlier and thus appear in the substitution // map. - applySubstitutionsToAssertions(); + d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); d_smt.d_stats->d_numAssertionsPost += d_assertions.size(); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-ite-removal" << endl; @@ -4391,8 +4383,9 @@ void SmtEnginePrivate::processAssertions() { // First, find all skolems that appear in the substitution map - their associated iteExpr will need // to be moved to the main assertion set set<TNode> skolemSet; - SubstitutionMap::iterator pos = d_topLevelSubstitutions.begin(); - for (; pos != d_topLevelSubstitutions.end(); ++pos) { + SubstitutionMap::iterator pos = top_level_substs.begin(); + for (; pos != top_level_substs.end(); ++pos) + { collectSkolems((*pos).first, skolemSet, cache); collectSkolems((*pos).second, skolemSet, cache); } @@ -4438,7 +4431,7 @@ void SmtEnginePrivate::processAssertions() { // 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 removeITEs(); - applySubstitutionsToAssertions(); + d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions); // Assert(iteRewriteAssertionsEnd == d_assertions.size()); } Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : post-repeat-simplify" << endl; |