Refactor IteRemoval preprocessing pass (#1793)

This commit refactors the IteRemoval pass to follow the new format.
In addition to moving the code, this entails the following changes:

- The timer for the ITE removal is now called differently (the default
  timer of PreprocessingPass is used) and measures just the
  preprocessing pass without applySubstitutions(). It also measures the
  time used by both invocations of the ITE removal pass.
- Debug output will be slightly different because we now just rely on
  the default functionality of PreprocessingPass.
- d_iteRemover is now passed into the PreprocessingPassContext.
- AssertionPipeline now owns the d_iteSkolemMap, which makes it
  accessible by preprocessing passes. The idea behind this is that the
  preprocessing passes collect information in AssertionPipeline and
  d_iteSkolemMap fits that pattern.

diff --git a/src/Makefile.am b/src/Makefile.am
index 992f229d605e9a097eda7c8ea4014f5de79a7f95..59a2a64c0d23ad7e3ce2dea57f507e6736001b00 100644 (file)
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -77,6 +77,8 @@ libcvc4_la_SOURCES = \
        preprocessing/passes/extended_rewriter_pass.h \
        preprocessing/passes/int_to_bv.cpp \
        preprocessing/passes/int_to_bv.h \
+       preprocessing/passes/ite_removal.cpp \
+       preprocessing/passes/ite_removal.h \
        preprocessing/passes/pseudo_boolean_processor.cpp \
        preprocessing/passes/pseudo_boolean_processor.h \
        preprocessing/passes/bool_to_bv.cpp \

diff --git a/src/preprocessing/passes/ite_removal.cpp b/src/preprocessing/passes/ite_removal.cpp
new file mode 100644 (file)
index 0000000..86c40a7
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.cpp
@@ -0,0 +1,49 @@
+/*********************                                                        */
+/*! \file ite_removal.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "preprocessing/passes/ite_removal.h"
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+
+IteRemoval::IteRemoval(PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "ite-removal")
+{
+}
+
+PreprocessingPassResult IteRemoval::applyInternal(AssertionPipeline* assertions)
+{
+  d_preprocContext->spendResource(options::preprocessStep());
+
+  // Remove all of the ITE occurrences and normalize
+  d_preprocContext->getIteRemover()->run(
+      assertions->ref(), assertions->getIteSkolemMap(), true);
+  for (unsigned i = 0, size = assertions->size(); i < size; ++i)
+  {
+    assertions->replace(i, Rewriter::rewrite((*assertions)[i]));
+  }
+
+  return PreprocessingPassResult::NO_CONFLICT;
+}
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4

diff --git a/src/preprocessing/passes/ite_removal.h b/src/preprocessing/passes/ite_removal.h
new file mode 100644 (file)
index 0000000..27ec4f0
--- /dev/null
+++ b/src/preprocessing/passes/ite_removal.h
@@ -0,0 +1,46 @@
+/*********************                                                        */
+/*! \file ite_removal.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Tim King, Paul Meng
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2017 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 Remove ITEs from the assertions
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+#define __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H
+
+#include <unordered_set>
+#include <vector>
+
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
+
+namespace CVC4 {
+namespace preprocessing {
+namespace passes {
+
+class IteRemoval : public PreprocessingPass
+{
+ public:
+  IteRemoval(PreprocessingPassContext* preprocContext);
+
+ protected:
+  PreprocessingPassResult applyInternal(AssertionPipeline* assertions) override;
+};
+
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
+
+#endif  // __CVC4__PREPROCESSING__PASSES__ITE_REMOVAL_H

diff --git a/src/preprocessing/preprocessing_pass.h b/src/preprocessing/preprocessing_pass.h
index 441d1c7cdfc3cc2009ead124845d6e265666c3ae..6f76b60e9b7269a97c13ae431f8ca94e386b2c1b 100644 (file)
--- a/src/preprocessing/preprocessing_pass.h
+++ b/src/preprocessing/preprocessing_pass.h
@@ -38,6 +38,7 @@
 #include "expr/node.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/term_formula_removal.h"
 #include "theory/substitutions.h"
 
 namespace CVC4 {
@@ -86,6 +87,8 @@ class AssertionPipeline
    */
   void replace(size_t i, const std::vector<Node>& ns);
 
+  IteSkolemMap& getIteSkolemMap() { return d_iteSkolemMap; }
+
   context::CDO<unsigned>& getSubstitutionsIndex()
   {
     return d_substitutionsIndex;
@@ -99,12 +102,17 @@ class AssertionPipeline
  private:
   std::vector<Node> d_nodes;
 
+  /**
+   * Map from skolem variables to index in d_assertions containing
+   * corresponding introduced Boolean ite
+   */
+  IteSkolemMap d_iteSkolemMap;
+  
   /* 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 1f3d245d7a734bbb6a7dd8d100f2e1c2437de856..31987b00bfe36ee80267957f0256a330d8b9360d 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -20,8 +20,10 @@ namespace CVC4 {
 namespace preprocessing {
 
 PreprocessingPassContext::PreprocessingPassContext(
-    SmtEngine* smt, ResourceManager* resourceManager)
-    : d_smt(smt), d_resourceManager(resourceManager)
+    SmtEngine* smt,
+    ResourceManager* resourceManager,
+    RemoveTermFormulas* iteRemover)
+    : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover)
 {
 }
 

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 9927cd8fbcf3dc32db5c046b8851bae0d53e7540..b50421e6caf856376c69b830862c4fa180981da3 100644 (file)
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -24,6 +24,7 @@
 #include "context/context.h"
 #include "decision/decision_engine.h"
 #include "smt/smt_engine.h"
+#include "smt/term_formula_removal.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 
@@ -33,12 +34,16 @@ namespace preprocessing {
 class PreprocessingPassContext
 {
  public:
-  PreprocessingPassContext(SmtEngine* smt, ResourceManager* resourceManager);
+  PreprocessingPassContext(SmtEngine* smt,
+                           ResourceManager* resourceManager,
+                           RemoveTermFormulas* iteRemover);
   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; }
+  RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
+
   void spendResource(unsigned amount)
   {
     d_resourceManager->spendResource(amount);
@@ -51,6 +56,9 @@ class PreprocessingPassContext
   /* Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
   ResourceManager* d_resourceManager;
+
+  /** Instance of the ITE remover */
+  RemoveTermFormulas* d_iteRemover;
 };  // class PreprocessingPassContext
 
 }  // namespace preprocessing

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index b5d758bca13ffa215621d8ceaeac4fbc52b1eb34..d2e9c2f36a2490118e99360d10caef8a3cc24416 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -79,6 +79,7 @@
 #include "preprocessing/passes/bv_to_bool.h"
 #include "preprocessing/passes/extended_rewriter_pass.h"
 #include "preprocessing/passes/int_to_bv.h"
+#include "preprocessing/passes/ite_removal.h"
 #include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/passes/real_to_int.h"
 #include "preprocessing/passes/rewrite.h"
@@ -204,8 +205,6 @@ struct SmtEngineStatistics {
   TimerStat d_simpITETime;
   /** time spent in simplifying ITEs */
   TimerStat d_unconstrainedSimpTime;
-  /** time spent removing ITEs */
-  TimerStat d_iteRemovalTime;
   /** time spent in theory preprocessing */
   TimerStat d_theoryPreprocessTime;
   /** time spent in theory preprocessing */
@@ -243,7 +242,6 @@ struct SmtEngineStatistics {
     d_numConstantProps("smt::SmtEngine::numConstantProps", 0),
     d_simpITETime("smt::SmtEngine::simpITETime"),
     d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
-    d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
     d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
     d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
@@ -267,7 +265,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->registerStat(&d_numConstantProps);
     smtStatisticsRegistry()->registerStat(&d_simpITETime);
     smtStatisticsRegistry()->registerStat(&d_unconstrainedSimpTime);
-    smtStatisticsRegistry()->registerStat(&d_iteRemovalTime);
     smtStatisticsRegistry()->registerStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->registerStat(&d_rewriteApplyToConstTime);
     smtStatisticsRegistry()->registerStat(&d_cnfConversionTime);
@@ -292,7 +289,6 @@ struct SmtEngineStatistics {
     smtStatisticsRegistry()->unregisterStat(&d_numConstantProps);
     smtStatisticsRegistry()->unregisterStat(&d_simpITETime);
     smtStatisticsRegistry()->unregisterStat(&d_unconstrainedSimpTime);
-    smtStatisticsRegistry()->unregisterStat(&d_iteRemovalTime);
     smtStatisticsRegistry()->unregisterStat(&d_theoryPreprocessTime);
     smtStatisticsRegistry()->unregisterStat(&d_rewriteApplyToConstTime);
     smtStatisticsRegistry()->unregisterStat(&d_cnfConversionTime);
@@ -563,12 +559,8 @@ class SmtEnginePrivate : public NodeManagerListener {
   /** mapping from expressions to name */
   context::CDHashMap< Node, std::string, NodeHashFunction > d_exprNames;
   //------------------------------- end expression names
-public:
-  /**
-   * Map from skolem variables to index in d_assertions containing
-   * corresponding introduced Boolean ite
-   */
-  IteSkolemMap d_iteSkolemMap;
+ public:
+  IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
 
   /** Instance of the ITE remover */
   RemoveTermFormulas d_iteRemover;
@@ -595,11 +587,6 @@ public:
    */
   void staticLearning();
 
-  /**
-   * Remove ITEs from the assertions.
-   */
-  void removeITEs();
-
   Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
   Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
 
@@ -638,8 +625,8 @@ public:
    * Remove conjuncts in toRemove from conjunction n. Return # of removed
    * conjuncts.
    */
-  size_t removeFromConjunction(Node& n,
-                               const std::unordered_set<unsigned long>& toRemove);
+  size_t removeFromConjunction(
+      Node& n, const std::unordered_set<unsigned long>& toRemove);
 
   /** Scrub miplib encodings. */
   void doMiplibTrick();
@@ -673,7 +660,6 @@ public:
         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);
@@ -839,7 +825,7 @@ public:
     d_assertions.clear();
     d_nonClausalLearnedLiterals.clear();
     d_realAssertionsEnd = 0;
-    d_iteSkolemMap.clear();
+    getIteSkolemMap().clear();
   }
 
   /**
@@ -988,7 +974,8 @@ SmtEngine::SmtEngine(ExprManager* em)
 
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
-  d_theoryEngine = new TheoryEngine(d_context, d_userContext,
+  d_theoryEngine = new TheoryEngine(d_context,
+                                    d_userContext,
                                     d_private->d_iteRemover,
                                     const_cast<const LogicInfo&>(d_logic),
                                     d_channels);
@@ -2654,7 +2641,7 @@ bool SmtEngine::isDefinedFunction( Expr func ){
 void SmtEnginePrivate::finishInit()
 {
   d_preprocessingPassContext.reset(
-      new PreprocessingPassContext(&d_smt, d_resourceManager));
+      new PreprocessingPassContext(&d_smt, d_resourceManager, &d_iteRemover));
   // TODO: register passes here (this will likely change when we add support for
   // actually assembling preprocessing pipelines).
   std::unique_ptr<ApplySubsts> applySubsts(
@@ -2679,6 +2666,8 @@ void SmtEnginePrivate::finishInit()
       new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<PseudoBooleanProcessor> pbProc(
       new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
+  std::unique_ptr<IteRemoval> iteRemoval(
+      new IteRemoval(d_preprocessingPassContext.get()));
   std::unique_ptr<RealToInt> realToInt(
       new RealToInt(d_preprocessingPassContext.get()));
   std::unique_ptr<Rewrite> rewrite(
@@ -2711,6 +2700,8 @@ void SmtEnginePrivate::finishInit()
   d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
   d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
                                            std::move(pbProc));
+  d_preprocessingPassRegistry.registerPass("ite-removal",
+                                           std::move(iteRemoval));
   d_preprocessingPassRegistry.registerPass("real-to-int", std::move(realToInt));
   d_preprocessingPassRegistry.registerPass("rewrite", std::move(rewrite));
   d_preprocessingPassRegistry.registerPass("sep-skolem-emp",
@@ -2968,20 +2959,6 @@ Node SmtEnginePrivate::purifyNlTerms(TNode n, NodeMap& cache, NodeMap& bcache, s
   return ret;
 }
 
-void SmtEnginePrivate::removeITEs() {
-  d_smt.finalOptionsAreSet();
-  spendResource(options::preprocessStep());
-  Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
-
-  // Remove all of the ITE occurrences and normalize
-  d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
-  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-    d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
-  }
-}
-
-
-
 // do dumping (before/after any preprocessing pass)
 static void dumpAssertions(const char* key,
                            const AssertionPipeline& assertionList) {
@@ -3937,7 +3914,8 @@ Result SmtEngine::check() {
        (not d_logic.isQuantified() &&
         d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isDifferenceLogic() &&  !d_logic.areIntegersUsed()
         )){
-      if(d_private->d_iteSkolemMap.empty()){
+      if (d_private->getIteSkolemMap().empty())
+      {
         options::decisionStopOnly.set(false);
         d_decisionEngine->clearStrategies();
         Trace("smt") << "SmtEngine::check(): turning off stop only" << endl;
@@ -3976,8 +3954,9 @@ void SmtEnginePrivate::collectSkolems(TNode n, set<TNode>& skolemSet, unordered_
 
   size_t sz = n.getNumChildren();
   if (sz == 0) {
-    IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
-    if (it != d_iteSkolemMap.end()) {
+    IteSkolemMap::iterator it = getIteSkolemMap().find(n);
+    if (it != getIteSkolemMap().end())
+    {
       skolemSet.insert(n);
     }
     cache[n] = true;
@@ -4002,9 +3981,10 @@ bool SmtEnginePrivate::checkForBadSkolems(TNode n, TNode skolem, unordered_map<N
 
   size_t sz = n.getNumChildren();
   if (sz == 0) {
-    IteSkolemMap::iterator it = d_iteSkolemMap.find(n);
+    IteSkolemMap::iterator it = getIteSkolemMap().find(n);
     bool bad = false;
-    if (it != d_iteSkolemMap.end()) {
+    if (it != getIteSkolemMap().end())
+    {
       if (!((*it).first < n)) {
         bad = true;
       }
@@ -4326,22 +4306,15 @@ void SmtEnginePrivate::processAssertions() {
   }
   Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-ite-removal" << endl;
-  dumpAssertions("pre-ite-removal", d_assertions);
   {
-    Chat() << "removing term ITEs..." << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
-    // Remove ITEs, updating d_iteSkolemMap
     d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
-    removeITEs();
+    d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions);
     // This is needed because when solving incrementally, removeITEs may introduce
     // skolems that were solved for earlier and thus appear in the substitution
     // map.
     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;
-  dumpAssertions("post-ite-removal", d_assertions);
 
   dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
@@ -4372,8 +4345,8 @@ void SmtEnginePrivate::processAssertions() {
       // 1. iteExpr has the form (ite cond (sk = t) (sk = e))
       // 2. if some sk' in Sk appears in cond, t, or e, then sk' <_sk sk
       // If either of these is violated, we must add iteExpr as a proper assertion
-      IteSkolemMap::iterator it = d_iteSkolemMap.begin();
-      IteSkolemMap::iterator iend = d_iteSkolemMap.end();
+      IteSkolemMap::iterator it = getIteSkolemMap().begin();
+      IteSkolemMap::iterator iend = getIteSkolemMap().end();
       NodeBuilder<> builder(kind::AND);
       builder << d_assertions[d_realAssertionsEnd - 1];
       vector<TNode> toErase;
@@ -4401,14 +4374,14 @@ void SmtEnginePrivate::processAssertions() {
       }
       if(builder.getNumChildren() > 1) {
         while (!toErase.empty()) {
-          d_iteSkolemMap.erase(toErase.back());
+          getIteSkolemMap().erase(toErase.back());
           toErase.pop_back();
         }
         d_assertions[d_realAssertionsEnd - 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
-      removeITEs();
+      d_preprocessingPassRegistry.getPass("ite-removal")->apply(&d_assertions);
       d_preprocessingPassRegistry.getPass("apply-substs")->apply(&d_assertions);
       //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
@@ -4468,8 +4441,8 @@ 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, d_iteSkolemMap);
+    d_smt.d_decisionEngine->addAssertions(
+        d_assertions.ref(), d_realAssertionsEnd, getIteSkolemMap());
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
@@ -4491,7 +4464,7 @@ void SmtEnginePrivate::processAssertions() {
   d_assertionsProcessed = true;
 
   d_assertions.clear();
-  d_iteSkolemMap.clear();
+  getIteSkolemMap().clear();
 }
 
 void SmtEnginePrivate::addFormula(TNode n, bool inUnsatCore, bool inInput)