diff options
| -rw-r--r-- | src/Makefile.am | 2 | ||||
| -rw-r--r-- | src/preprocessing/passes/apply_substs.cpp | 74 | ||||
| -rw-r--r-- | src/preprocessing/passes/apply_substs.h | 49 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass.cpp | 7 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass.h | 37 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass_context.cpp | 9 | ||||
| -rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 13 | ||||
| -rw-r--r-- | src/smt/smt_engine.cpp | 205 | ||||
| -rw-r--r-- | test/unit/preprocessing/pass_bv_gauss_white.h | 14 |
9 files changed, 286 insertions, 124 deletions
diff --git a/src/Makefile.am b/src/Makefile.am index 2ddc905e0..b4a083b0a 100644 --- a/src/Makefile.am +++ b/src/Makefile.am @@ -65,6 +65,8 @@ libcvc4_la_SOURCES = \ decision/decision_strategy.h \ decision/justification_heuristic.cpp \ decision/justification_heuristic.h \ + preprocessing/passes/apply_substs.cpp \ + preprocessing/passes/apply_substs.h \ preprocessing/passes/bv_abstraction.cpp \ preprocessing/passes/bv_abstraction.h \ preprocessing/passes/bv_ackermann.cpp \ diff --git a/src/preprocessing/passes/apply_substs.cpp b/src/preprocessing/passes/apply_substs.cpp new file mode 100644 index 000000000..6fb4b7793 --- /dev/null +++ b/src/preprocessing/passes/apply_substs.cpp @@ -0,0 +1,74 @@ +/********************* */ +/*! \file apply_substs.cpp + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Apply substitutions preprocessing pass. + ** + ** Apply top level substitutions to assertions, rewrite, and store back into + ** assertions. + **/ + +#include "preprocessing/passes/apply_substs.h" + +#include "context/cdo.h" +#include "theory/rewriter.h" +#include "theory/substitutions.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +ApplySubsts::ApplySubsts(PreprocessingPassContext* preprocContext) + : PreprocessingPass(preprocContext, "apply-substs") +{ +} + +PreprocessingPassResult ApplySubsts::applyInternal( + AssertionPipeline* assertionsToPreprocess) +{ + if (!options::unsatCores()) + { + Chat() << "applying substitutions..." << std::endl; + Trace("apply-substs") << "SmtEnginePrivate::processAssertions(): " + << "applying substitutions" << std::endl; + // TODO(#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. + context::CDO<unsigned>& substs_index = + assertionsToPreprocess->getSubstitutionsIndex(); + unsigned size = assertionsToPreprocess->size(); + unsigned substitutionAssertion = substs_index > 0 ? substs_index : size; + for (unsigned i = 0; i < size; ++i) + { + if (i == substitutionAssertion) + { + continue; + } + Trace("apply-substs") << "applying to " << (*assertionsToPreprocess)[i] + << std::endl; + d_preprocContext->spendResource(options::preprocessStep()); + assertionsToPreprocess->replace( + i, + theory::Rewriter::rewrite( + assertionsToPreprocess->getTopLevelSubstitutions().apply( + (*assertionsToPreprocess)[i]))); + Trace("apply-substs") << " got " << (*assertionsToPreprocess)[i] + << std::endl; + } + } + return PreprocessingPassResult::NO_CONFLICT; +} + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 diff --git a/src/preprocessing/passes/apply_substs.h b/src/preprocessing/passes/apply_substs.h new file mode 100644 index 000000000..f2f77fd0e --- /dev/null +++ b/src/preprocessing/passes/apply_substs.h @@ -0,0 +1,49 @@ +/********************* */ +/*! \file apply_substs.h + ** \verbatim + ** Top contributors (to current version): + ** Aina Niemetz + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Apply substitutions preprocessing pass. + ** + ** Apply top level substitutions to assertions, rewrite, and store back into + ** assertions. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H +#define __CVC4__PREPROCESSING__PASSES__APPLY_SUBSTS_H + +#include "preprocessing/preprocessing_pass.h" +#include "preprocessing/preprocessing_pass_context.h" + +namespace CVC4 { +namespace preprocessing { +namespace passes { + +class ApplySubsts : public PreprocessingPass +{ + public: + ApplySubsts(PreprocessingPassContext* preprocContext); + + protected: + /** + * Apply assertionsToPreprocess->getTopLevelSubstitutions() to the + * assertions, in assertionsToPreprocess, rewrite, and store back into + * given assertion pipeline. + */ + PreprocessingPassResult applyInternal( + AssertionPipeline* assertionsToPreprocess) override; +}; + +} // namespace passes +} // namespace preprocessing +} // namespace CVC4 + +#endif diff --git a/src/preprocessing/preprocessing_pass.cpp b/src/preprocessing/preprocessing_pass.cpp index 06992dedc..97b05802d 100644 --- a/src/preprocessing/preprocessing_pass.cpp +++ b/src/preprocessing/preprocessing_pass.cpp @@ -2,7 +2,7 @@ /*! \file preprocessing_pass.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu + ** Justin Xu, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -24,6 +24,11 @@ namespace CVC4 { namespace preprocessing { +AssertionPipeline::AssertionPipeline(context::Context* context) + : d_substitutionsIndex(context, 0), d_topLevelSubstitutions(context) +{ +} + void AssertionPipeline::replace(size_t i, Node n) { PROOF(ProofManager::currentPM()->addDependence(n, d_nodes[i]);); d_nodes[i] = n; diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h index d57484eff..441d1c7cd 100644 --- a/src/preprocessing/preprocessing_pass.h +++ b/src/preprocessing/preprocessing_pass.h @@ -2,7 +2,7 @@ /*! \file preprocessing_pass.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu + ** Justin Xu, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -34,19 +34,24 @@ #include <string> #include <vector> +#include "context/cdo.h" #include "expr/node.h" #include "preprocessing/preprocessing_pass_context.h" #include "smt/smt_engine_scope.h" +#include "theory/substitutions.h" namespace CVC4 { namespace preprocessing { -/* Assertion Pipeline stores a list of assertions modified by preprocessing - * passes. */ -class AssertionPipeline { - std::vector<Node> d_nodes; - +/** + * Assertion Pipeline stores a list of assertions modified by preprocessing + * passes. + */ +class AssertionPipeline +{ public: + AssertionPipeline(context::Context* context); + size_t size() const { return d_nodes.size(); } void resize(size_t n) { d_nodes.resize(n); } @@ -80,6 +85,26 @@ class AssertionPipeline { * dependencies. */ void replace(size_t i, const std::vector<Node>& ns); + + context::CDO<unsigned>& getSubstitutionsIndex() + { + return d_substitutionsIndex; + } + + theory::SubstitutionMap& getTopLevelSubstitutions() + { + return d_topLevelSubstitutions; + } + + private: + std::vector<Node> d_nodes; + + /* Index for where to store substitutions */ + context::CDO<unsigned> d_substitutionsIndex; + + /* The top level substitutions */ + theory::SubstitutionMap d_topLevelSubstitutions; + }; /* class AssertionPipeline */ /** diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp index d44f24e13..1f3d245d7 100644 --- a/src/preprocessing/preprocessing_pass_context.cpp +++ b/src/preprocessing/preprocessing_pass_context.cpp @@ -2,7 +2,7 @@ /*! \file preprocessing_pass_context.cpp ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Mathias Preiner + ** Justin Xu, Mathias Preiner, Aina Niemetz ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -19,8 +19,11 @@ namespace CVC4 { namespace preprocessing { -PreprocessingPassContext::PreprocessingPassContext(SmtEngine* smt) - : d_smt(smt) {} +PreprocessingPassContext::PreprocessingPassContext( + SmtEngine* smt, ResourceManager* resourceManager) + : d_smt(smt), d_resourceManager(resourceManager) +{ +} void PreprocessingPassContext::widenLogic(theory::TheoryId id) { diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index f85f0af7d..9927cd8fb 100644 --- a/src/preprocessing/preprocessing_pass_context.h +++ b/src/preprocessing/preprocessing_pass_context.h @@ -2,7 +2,7 @@ /*! \file preprocessing_pass_context.h ** \verbatim ** Top contributors (to current version): - ** Justin Xu, Mathias Preiner, Andres Noetzli + ** Justin Xu, Aina Niemetz, Mathias Preiner ** This file is part of the CVC4 project. ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS ** in the top-level source directory) and their institutional affiliations. @@ -25,18 +25,24 @@ #include "decision/decision_engine.h" #include "smt/smt_engine.h" #include "theory/theory_engine.h" +#include "util/resource_manager.h" namespace CVC4 { namespace preprocessing { -class PreprocessingPassContext { +class PreprocessingPassContext +{ public: - PreprocessingPassContext(SmtEngine* smt); + PreprocessingPassContext(SmtEngine* smt, ResourceManager* resourceManager); SmtEngine* getSmt() { return d_smt; } TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; } DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; } prop::PropEngine* getPropEngine() { return d_smt->d_propEngine; } context::Context* getUserContext() { return d_smt->d_userContext; } + void spendResource(unsigned amount) + { + d_resourceManager->spendResource(amount); + } /* Widen the logic to include the given theory. */ void widenLogic(theory::TheoryId id); @@ -44,6 +50,7 @@ class PreprocessingPassContext { private: /* Pointer to the SmtEngine that this context was created in. */ SmtEngine* d_smt; + ResourceManager* d_resourceManager; }; // class PreprocessingPassContext } // namespace preprocessing 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; diff --git a/test/unit/preprocessing/pass_bv_gauss_white.h b/test/unit/preprocessing/pass_bv_gauss_white.h index cdf620285..7d7ee1a3a 100644 --- a/test/unit/preprocessing/pass_bv_gauss_white.h +++ b/test/unit/preprocessing/pass_bv_gauss_white.h @@ -14,14 +14,15 @@ ** Unit tests for Gaussian Elimination preprocessing pass. **/ +#include "context/context.h" #include "expr/node.h" #include "expr/node_manager.h" -#include "preprocessing/preprocessing_pass.h" #include "preprocessing/passes/bv_gauss.cpp" +#include "preprocessing/preprocessing_pass.h" #include "smt/smt_engine.h" #include "smt/smt_engine_scope.h" -#include "theory/rewriter.h" #include "theory/bv/theory_bv_utils.h" +#include "theory/rewriter.h" #include "util/bitvector.h" #include <cxxtest/TestSuite.h> @@ -2377,7 +2378,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(a); passes::BVGauss bgauss(nullptr); std::unordered_map<Node, Node, NodeHashFunction> res; @@ -2459,7 +2461,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite Node a = d_nm->mkNode(kind::AND, d_nm->mkNode(kind::AND, eq1, eq2), eq3); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(a); apipe.push_back(eq4); apipe.push_back(eq5); @@ -2510,7 +2513,8 @@ class TheoryBVGaussWhite : public CxxTest::TestSuite d_p), d_nine); - AssertionPipeline apipe; + context::Context context; + AssertionPipeline apipe(&context); apipe.push_back(eq1); apipe.push_back(eq2); passes::BVGauss bgauss(nullptr); |