Refactor ApplySubsts preprocessing pass. (#2120)

diff --git a/src/Makefile.am b/src/Makefile.am
index 2ddc905e01bb8cd99bca4ae0cbaa8dcb1d22d77b..b4a083b0ab8773e42db1bb39e708b0716c1e4a50 100644 (file)
--- 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 (file)
index 0000000..6fb4b77
--- /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 (file)
index 0000000..f2f77fd
--- /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 06992dedc7bef54ce36a4833d4f36bed98e8d0f2..97b05802da113fb7138ad87e96a6e308a629977b 100644 (file)
--- 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 d57484eff840f89ed01459e888ae150f45f8e58e..441d1c7cdfc3cc2009ead124845d6e265666c3ae 100644 (file)
--- 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 d44f24e13c56d1b973135187b9e76305184a6d22..1f3d245d7a734bbb6a7dd8d100f2e1c2437de856 100644 (file)
--- 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 f85f0af7d32c467ca1d6bfdcdb17c21ce00121bd..9927cd8fbcf3dc32db5c046b8851bae0d53e7540 100644 (file)
--- 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 c21a0b4c2f32e6486a263ef95bb7cd6c6d6ba2ba..1705cd0a3e5149e37d621fda28c16c684e5413a8 100644 (file)
--- 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,16 +803,12 @@ 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.
    */
@@ -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 cdf6202859a06522ba4454459ce1efb0c3d57a1e..7d7ee1a3a024edf515723700b616eb9884bfbd79 100644 (file)
--- 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);