Refactor pbRewrites preprocessing pass (#1767)

This commit refactors the pbRewrites preprocessing pass into the new
style. This commit is essentially just a code move and adds a regression
test for the preprocessing pass. It also makes use of the
AssertionPipeline::replace function to do proper dependency tracking.

6 files changed, 251 insertions, 161 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 67e105089..f89a8426e 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -62,10 +62,12 @@ libcvc4_la_SOURCES = \
 	decision/decision_strategy.h \
 	decision/justification_heuristic.cpp \
 	decision/justification_heuristic.h \
-	preprocessing/passes/int_to_bv.cpp \
-	preprocessing/passes/int_to_bv.h \
 	preprocessing/passes/bv_gauss.cpp \
 	preprocessing/passes/bv_gauss.h \
+	preprocessing/passes/int_to_bv.cpp \
+	preprocessing/passes/int_to_bv.h \
+	preprocessing/passes/pseudo_boolean_processor.cpp \
+	preprocessing/passes/pseudo_boolean_processor.h \
 	preprocessing/preprocessing_pass.cpp \
 	preprocessing/preprocessing_pass.h \
 	preprocessing/preprocessing_pass_context.cpp \
@@ -246,8 +248,6 @@ libcvc4_la_SOURCES = \
 	theory/arith/normal_form.h\
 	theory/arith/partial_model.cpp \
 	theory/arith/partial_model.h \
-	theory/arith/pseudoboolean_proc.cpp \
-	theory/arith/pseudoboolean_proc.h \
 	theory/arith/simplex.cpp \
 	theory/arith/simplex.h \
 	theory/arith/simplex_update.cpp \
diff --git a/src/theory/arith/pseudoboolean_proc.cpp b/src/preprocessing/passes/pseudo_boolean_processor.cpp
index 1cdb90e20..c102bee47 100644
--- a/src/theory/arith/pseudoboolean_proc.cpp
+++ b/src/preprocessing/passes/pseudo_boolean_processor.cpp
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file pseudoboolean_proc.cpp
+/*! \file pseudo_boolean_processor.cpp
  ** \verbatim
  ** Top contributors (to current version):
  **   Tim King, Paul Meng
@@ -15,7 +15,7 @@
  ** \todo document this file
  **/
 
-#include "theory/arith/pseudoboolean_proc.h"
+#include "preprocessing/passes/pseudo_boolean_processor.h"
 
 #include "base/output.h"
 #include "theory/arith/arith_utilities.h"
@@ -23,37 +23,61 @@
 #include "theory/rewriter.h"
 
 namespace CVC4 {
-namespace theory {
-namespace arith {
+namespace preprocessing {
+namespace passes {
+
+using namespace CVC4::theory;
+using namespace CVC4::theory::arith;
+
+PseudoBooleanProcessor::PseudoBooleanProcessor(
+    PreprocessingPassContext* preprocContext)
+    : PreprocessingPass(preprocContext, "pseudo-boolean-processor"),
+      d_pbBounds(preprocContext->getUserContext()),
+      d_subCache(preprocContext->getUserContext()),
+      d_pbs(preprocContext->getUserContext(), 0)
+{
+}
 
+PreprocessingPassResult PseudoBooleanProcessor::applyInternal(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  learn(assertionsToPreprocess->ref());
+  if (likelyToHelp())
+  {
+    applyReplacements(assertionsToPreprocess);
+  }
 
-PseudoBooleanProcessor::PseudoBooleanProcessor(context::Context* user_context)
-  : d_pbBounds(user_context)
-  , d_subCache(user_context)
-  , d_pbs(user_context, 0)
-{}
+  return PreprocessingPassResult::NO_CONFLICT;
+}
 
-bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
-  if (assertion.getKind() != kind::GEQ){ return false; }
+bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated)
+{
+  if (assertion.getKind() != kind::GEQ)
+  {
+    return false;
+  }
   Assert(assertion.getKind() == kind::GEQ);
 
-  Debug("pbs::rewrites") << "decomposeAssertion" << assertion  << std::endl;
+  Debug("pbs::rewrites") << "decomposeAssertion" << assertion << std::endl;
 
   Node l = assertion[0];
   Node r = assertion[1];
 
-  if( r.getKind() != kind::CONST_RATIONAL ){
-    Debug("pbs::rewrites") << "not rhs constant" << assertion  << std::endl;
+  if (r.getKind() != kind::CONST_RATIONAL)
+  {
+    Debug("pbs::rewrites") << "not rhs constant" << assertion << std::endl;
     return false;
   }
   // don't bother matching on anything other than + on the left hand side
-  if( l.getKind() != kind::PLUS){
-    Debug("pbs::rewrites") << "not plus" << assertion  << std::endl;
+  if (l.getKind() != kind::PLUS)
+  {
+    Debug("pbs::rewrites") << "not plus" << assertion << std::endl;
     return false;
   }
 
-  if(!Polynomial::isMember(l)){
-    Debug("pbs::rewrites") << "not polynomial" << assertion  << std::endl;
+  if (!Polynomial::isMember(l))
+  {
+    Debug("pbs::rewrites") << "not polynomial" << assertion << std::endl;
     return false;
   }
 
@@ -85,20 +109,30 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
   Assert(d_off.value().isIntegral());
 
   int adj = negated ? -1 : 1;
-  for(Polynomial::iterator i=p.begin(), end=p.end(); i != end; ++i){
+  for (Polynomial::iterator i = p.begin(), end = p.end(); i != end; ++i)
+  {
     Monomial m = *i;
     const Rational& coeff = m.getConstant().getValue();
-    if(!(coeff.isOne() || coeff.isNegativeOne())){ return false; }
+    if (!(coeff.isOne() || coeff.isNegativeOne()))
+    {
+      return false;
+    }
     Assert(coeff.sgn() != 0);
 
     const VarList& vl = m.getVarList();
     Node v = vl.getNode();
 
-    if(!isPseudoBoolean(v)){ return false; }
+    if (!isPseudoBoolean(v))
+    {
+      return false;
+    }
     int sgn = adj * coeff.sgn();
-    if(sgn > 0){
+    if (sgn > 0)
+    {
       d_pos.push_back(v);
-    }else{
+    }
+    else
+    {
       d_neg.push_back(v);
     }
   }
@@ -107,27 +141,34 @@ bool PseudoBooleanProcessor::decomposeAssertion(Node assertion, bool negated){
   return true;
 }
 
-bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const{
+bool PseudoBooleanProcessor::isPseudoBoolean(Node v) const
+{
   CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
-  if(ci != d_pbBounds.end()){
-    const PairNode& p = (*ci).second;
+  if (ci != d_pbBounds.end())
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
     return !(p.first).isNull() && !(p.second).isNull();
   }
   return false;
 }
 
-void PseudoBooleanProcessor::addGeqZero(Node v, Node exp){
+void PseudoBooleanProcessor::addGeqZero(Node v, Node exp)
+{
   Assert(isIntVar(v));
   Assert(!exp.isNull());
   CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
 
   Debug("pbs::rewrites") << "addGeqZero " << v << std::endl;
 
-  if(ci == d_pbBounds.end()){
+  if (ci == d_pbBounds.end())
+  {
     d_pbBounds.insert(v, std::make_pair(exp, Node::null()));
-  }else{
-    const PairNode& p = (*ci).second;
-    if(p.first.isNull()){
+  }
+  else
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
+    if (p.first.isNull())
+    {
       Assert(!p.second.isNull());
       d_pbBounds.insert(v, std::make_pair(exp, p.second));
       Debug("pbs::rewrites") << "add pbs " << v << std::endl;
@@ -137,16 +178,21 @@ void PseudoBooleanProcessor::addGeqZero(Node v, Node exp){
   }
 }
 
-void PseudoBooleanProcessor::addLeqOne(Node v, Node exp){
+void PseudoBooleanProcessor::addLeqOne(Node v, Node exp)
+{
   Assert(isIntVar(v));
   Assert(!exp.isNull());
   Debug("pbs::rewrites") << "addLeqOne " << v << std::endl;
   CDNode2PairMap::const_iterator ci = d_pbBounds.find(v);
-  if(ci == d_pbBounds.end()){
+  if (ci == d_pbBounds.end())
+  {
     d_pbBounds.insert(v, std::make_pair(Node::null(), exp));
-  }else{
-    const PairNode& p = (*ci).second;
-    if(p.second.isNull()){
+  }
+  else
+  {
+    const std::pair<Node, Node>& p = (*ci).second;
+    if (p.second.isNull())
+    {
       Assert(!p.first.isNull());
       d_pbBounds.insert(v, std::make_pair(p.first, exp));
       Debug("pbs::rewrites") << "add pbs " << v << std::endl;
@@ -156,7 +202,10 @@ void PseudoBooleanProcessor::addLeqOne(Node v, Node exp){
   }
 }
 
-void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, bool negated, Node orig){
+void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion,
+                                               bool negated,
+                                               Node orig)
+{
   Assert(assertion.getKind() == kind::GEQ);
   Assert(assertion == Rewriter::rewrite(assertion));
 
@@ -164,93 +213,122 @@ void PseudoBooleanProcessor::learnRewrittenGeq(Node assertion, bool negated, Nod
   Node l = assertion[0];
   Node r = assertion[1];
 
-
-  if(r.getKind() == kind::CONST_RATIONAL){
+  if (r.getKind() == kind::CONST_RATIONAL)
+  {
     const Rational& rc = r.getConst<Rational>();
-    if(isIntVar(l)){
-      if(!negated && rc.isZero()){  // (>= x 0)
-	addGeqZero(l, orig);
-      }else if(negated && rc == Rational(2)){
-	addLeqOne(l, orig);
+    if (isIntVar(l))
+    {
+      if (!negated && rc.isZero())
+      {  // (>= x 0)
+        addGeqZero(l, orig);
       }
-    }else if(l.getKind() == kind::MULT && l.getNumChildren() == 2){
+      else if (negated && rc == Rational(2))
+      {
+        addLeqOne(l, orig);
+      }
+    }
+    else if (l.getKind() == kind::MULT && l.getNumChildren() == 2)
+    {
       Node c = l[0], v = l[1];
-      if(c.getKind() == kind::CONST_RATIONAL && c.getConst<Rational>().isNegativeOne()){
-	if(isIntVar(v)){
-	  if(!negated && rc.isNegativeOne()){ // (>= (* -1 x) -1)
-	    addLeqOne(v, orig);
-	  }
-	}
+      if (c.getKind() == kind::CONST_RATIONAL
+          && c.getConst<Rational>().isNegativeOne())
+      {
+        if (isIntVar(v))
+        {
+          if (!negated && rc.isNegativeOne())
+          {  // (>= (* -1 x) -1)
+            addLeqOne(v, orig);
+          }
+        }
       }
     }
   }
 
-  if(!negated){
+  if (!negated)
+  {
     learnGeqSub(assertion);
   }
 }
 
-void PseudoBooleanProcessor::learnInternal(Node assertion, bool negated, Node orig){
-  switch(assertion.getKind()){
-  case kind::GEQ:
-  case kind::GT:
-  case kind::LEQ:
-  case kind::LT:
+void PseudoBooleanProcessor::learnInternal(Node assertion,
+                                           bool negated,
+                                           Node orig)
+{
+  switch (assertion.getKind())
+  {
+    case kind::GEQ:
+    case kind::GT:
+    case kind::LEQ:
+    case kind::LT:
     {
       Node rw = Rewriter::rewrite(assertion);
-      if(assertion == rw){
-	if(assertion.getKind() == kind::GEQ){
-	  learnRewrittenGeq(assertion, negated, orig);
-	}
-      }else{
-	learnInternal(rw, negated, orig);
+      if (assertion == rw)
+      {
+        if (assertion.getKind() == kind::GEQ)
+        {
+          learnRewrittenGeq(assertion, negated, orig);
+        }
+      }
+      else
+      {
+        learnInternal(rw, negated, orig);
       }
     }
     break;
-  case kind::NOT:
-    learnInternal(assertion[0], !negated, orig);
-    break;
-  default:
-    break; // do nothing
+    case kind::NOT: learnInternal(assertion[0], !negated, orig); break;
+    default: break;  // do nothing
   }
 }
 
-void PseudoBooleanProcessor::learn(Node assertion){
-  if(assertion.getKind() == kind::AND){
-    Node::iterator ci=assertion.begin(), cend = assertion.end();
-    for(; ci != cend; ++ci){
+void PseudoBooleanProcessor::learn(Node assertion)
+{
+  if (assertion.getKind() == kind::AND)
+  {
+    Node::iterator ci = assertion.begin(), cend = assertion.end();
+    for (; ci != cend; ++ci)
+    {
       learn(*ci);
     }
-  }else{
+  }
+  else
+  {
     learnInternal(assertion, false, assertion);
   }
 }
 
-Node PseudoBooleanProcessor::mkGeqOne(Node v){
+Node PseudoBooleanProcessor::mkGeqOne(Node v)
+{
   NodeManager* nm = NodeManager::currentNM();
   return nm->mkNode(kind::GEQ, v, mkRationalNode(Rational(1)));
 }
 
-void PseudoBooleanProcessor::learn(const NodeVec& assertions){
-  NodeVec::const_iterator ci, cend;
-  ci = assertions.begin(); cend=assertions.end();
-  for(; ci != cend; ++ci ){
+void PseudoBooleanProcessor::learn(const std::vector<Node>& assertions)
+{
+  std::vector<Node>::const_iterator ci, cend;
+  ci = assertions.begin();
+  cend = assertions.end();
+  for (; ci != cend; ++ci)
+  {
     learn(*ci);
   }
 }
 
-void PseudoBooleanProcessor::addSub(Node from, Node to){
-  if(!d_subCache.hasSubstitution(from)){
+void PseudoBooleanProcessor::addSub(Node from, Node to)
+{
+  if (!d_subCache.hasSubstitution(from))
+  {
     Node rw_to = Rewriter::rewrite(to);
     d_subCache.addSubstitution(from, rw_to);
   }
 }
 
-void PseudoBooleanProcessor::learnGeqSub(Node geq){
+void PseudoBooleanProcessor::learnGeqSub(Node geq)
+{
   Assert(geq.getKind() == kind::GEQ);
   const bool negated = false;
   bool success = decomposeAssertion(geq, negated);
-  if(!success){
+  if (!success)
+  {
     Debug("pbs::rewrites") << "failed " << std::endl;
     return;
   }
@@ -261,7 +339,8 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
 
   // for now special case everything we want
   // target easy clauses
-  if( d_pos.size() == 1 && d_neg.size() == 1 && off.isZero() ){
+  if (d_pos.size() == 1 && d_neg.size() == 1 && off.isZero())
+  {
     // x >= y
     // |- (y >= 1) => (x >= 1)
     Node x = d_pos.front();
@@ -271,7 +350,9 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
     Node yGeq1 = mkGeqOne(y);
     Node imp = yGeq1.impNode(xGeq1);
     addSub(geq, imp);
-  }else if( d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne()){
+  }
+  else if (d_pos.size() == 0 && d_neg.size() == 2 && off.isNegativeOne())
+  {
     // 0 >= (x + y -1)
     // |- 1 >= x + y
     // |- (or (not (x >= 1)) (not (y >= 1)))
@@ -282,7 +363,9 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
     Node yGeq1 = mkGeqOne(y);
     Node cases = (xGeq1.notNode()).orNode(yGeq1.notNode());
     addSub(geq, cases);
-  }else if( d_pos.size() == 2 && d_neg.size() == 1 && off.isZero() ){
+  }
+  else if (d_pos.size() == 2 && d_neg.size() == 1 && off.isZero())
+  {
     // (x + y) >= z
     // |- (z >= 1) => (or (x >= 1) (y >=1 ))
     Node x = d_pos[0];
@@ -292,41 +375,44 @@ void PseudoBooleanProcessor::learnGeqSub(Node geq){
     Node xGeq1 = mkGeqOne(x);
     Node yGeq1 = mkGeqOne(y);
     Node zGeq1 = mkGeqOne(z);
-    NodeManager* nm =NodeManager::currentNM();
+    NodeManager* nm = NodeManager::currentNM();
     Node dis = nm->mkNode(kind::OR, zGeq1.notNode(), xGeq1, yGeq1);
     addSub(geq, dis);
   }
 }
 
-Node PseudoBooleanProcessor::applyReplacements(Node pre){
+Node PseudoBooleanProcessor::applyReplacements(Node pre)
+{
   Node assertion = Rewriter::rewrite(pre);
 
   Node result = d_subCache.apply(assertion);
-  if(Debug.isOn("pbs::rewrites") && result != assertion ){
-    Debug("pbs::rewrites") << "applyReplacements" <<assertion << "-> " << result << std::endl;
+  if (Debug.isOn("pbs::rewrites") && result != assertion)
+  {
+    Debug("pbs::rewrites") << "applyReplacements" << assertion << "-> "
+                           << result << std::endl;
   }
   return result;
 }
 
-bool PseudoBooleanProcessor::likelyToHelp() const{
-  return d_pbs >= 100;
-}
+bool PseudoBooleanProcessor::likelyToHelp() const { return d_pbs >= 100; }
 
-void PseudoBooleanProcessor::applyReplacements(NodeVec& assertions){
-  for(size_t i=0, N=assertions.size(); i < N; ++i){
-    Node assertion = assertions[i];
-    Node res = applyReplacements(assertion);
-    assertions[i] = res;
+void PseudoBooleanProcessor::applyReplacements(
+    AssertionPipeline* assertionsToPreprocess)
+{
+  for (size_t i = 0, N = assertionsToPreprocess->size(); i < N; ++i)
+  {
+    assertionsToPreprocess->replace(
+        i, applyReplacements((*assertionsToPreprocess)[i]));
   }
 }
 
-void PseudoBooleanProcessor::clear() {
+void PseudoBooleanProcessor::clear()
+{
   d_off.clear();
   d_pos.clear();
   d_neg.clear();
 }
 
-
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
diff --git a/src/theory/arith/pseudoboolean_proc.h b/src/preprocessing/passes/pseudo_boolean_processor.h
index 0b91ed074..261470c74 100644
--- a/src/theory/arith/pseudoboolean_proc.h
+++ b/src/preprocessing/passes/pseudo_boolean_processor.h
@@ -1,5 +1,5 @@
 /*********************                                                        */
-/*! \file pseudoboolean_proc.h
+/*! \file pseudo_boolean_processor.h
  ** \verbatim
  ** Top contributors (to current version):
  **   Tim King, Paul Meng
@@ -17,7 +17,8 @@
 
 #include "cvc4_private.h"
 
-#pragma once
+#ifndef __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
+#define __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
 
 #include <unordered_set>
 #include <vector>
@@ -26,44 +27,31 @@
 #include "context/cdo.h"
 #include "context/context.h"
 #include "expr/node.h"
+#include "preprocessing/preprocessing_pass.h"
+#include "preprocessing/preprocessing_pass_context.h"
 #include "theory/substitutions.h"
 #include "util/maybe.h"
 #include "util/rational.h"
 
 namespace CVC4 {
-namespace theory {
-namespace arith {
+namespace preprocessing {
+namespace passes {
 
-class PseudoBooleanProcessor {
-private:
-  // x ->  <geqZero, leqOne>
-  typedef std::pair<Node, Node> PairNode;
-  typedef std::vector<Node> NodeVec;
-  typedef context::CDHashMap<Node, PairNode, NodeHashFunction> CDNode2PairMap;
-  CDNode2PairMap d_pbBounds;
-  SubstitutionMap d_subCache;
-
-  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
-  NodeSet d_learningCache;
+class PseudoBooleanProcessor : public PreprocessingPass
+{
+ public:
+  PseudoBooleanProcessor(PreprocessingPassContext* preprocContext);
 
-  context::CDO<unsigned> d_pbs;
-
-  // decompose into \sum pos >= neg + off
-  Maybe<Rational> d_off;
-  NodeVec d_pos;
-  NodeVec d_neg;
-  void clear();
-  /** Returns true if successful. */
-  bool decomposeAssertion(Node assertion, bool negated);
-
-public:
-  PseudoBooleanProcessor(context::Context* user_context);
+ protected:
+  PreprocessingPassResult applyInternal(
+      AssertionPipeline* assertionsToPreprocess) override;
 
+ private:
   /** Assumes that the assertions have been rewritten. */
-  void learn(const NodeVec& assertions);
+  void learn(const std::vector<Node>& assertions);
 
   /** Assumes that the assertions have been rewritten. */
-  void applyReplacements(NodeVec& assertions);
+  void applyReplacements(AssertionPipeline* assertionsToPreprocess);
 
   bool likelyToHelp() const;
 
@@ -75,23 +63,24 @@ public:
   // exp cannot be null.
   void addGeqZero(Node v, Node exp);
 
-
   // Adds the fact the that integert typed variable v
   //   must be <= 1 to the context.
   // This is explained by the explanation exp.
   // exp cannot be null.
   void addLeqOne(Node v, Node exp);
 
-  static inline bool isIntVar(Node v){
+  static inline bool isIntVar(Node v)
+  {
     return v.isVar() && v.getType().isInteger();
   }
 
-private:
+  void clear();
+
   /** Assumes that the assertion has been rewritten. */
   void learn(Node assertion);
 
   /** Rewrites a node  */
-  Node applyReplacements(Node assertion);
+  Node applyReplacements(Node pre);
 
   void learnInternal(Node assertion, bool negated, Node orig);
   void learnRewrittenGeq(Node assertion, bool negated, Node orig);
@@ -100,9 +89,29 @@ private:
   void learnGeqSub(Node geq);
 
   static Node mkGeqOne(Node v);
+
+  // x ->  <geqZero, leqOne>
+  typedef context::CDHashMap<Node, std::pair<Node, Node>, NodeHashFunction>
+      CDNode2PairMap;
+  CDNode2PairMap d_pbBounds;
+  theory::SubstitutionMap d_subCache;
+
+  typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
+  NodeSet d_learningCache;
+
+  context::CDO<unsigned> d_pbs;
+
+  // decompose into \sum pos >= neg + off
+  Maybe<Rational> d_off;
+  std::vector<Node> d_pos;
+  std::vector<Node> d_neg;
+
+  /** Returns true if successful. */
+  bool decomposeAssertion(Node assertion, bool negated);
 };
 
+}  // namespace passes
+}  // namespace preprocessing
+}  // namespace CVC4
 
-}/* CVC4::theory::arith namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+#endif  // __CVC4__PREPROCESSING__PASSES__PSEUDO_BOOLEAN_PROCESSOR_H
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 2e7a4eaf2..66f4d9297 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -21,10 +21,9 @@
 #ifndef __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 #define __CVC4__PREPROCESSING__PREPROCESSING_PASS_CONTEXT_H
 
+#include "context/context.h"
 #include "decision/decision_engine.h"
 #include "smt/smt_engine.h"
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/booleans/circuit_propagator.h"
 #include "theory/theory_engine.h"
 
 namespace CVC4 {
@@ -37,6 +36,7 @@ class PreprocessingPassContext {
   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; }
 
  private:
   /* Pointer to the SmtEngine that this context was created in. */
diff --git a/src/preprocessing/preprocessing_pass_registry.h b/src/preprocessing/preprocessing_pass_registry.h
index 75c66a035..37cff676b 100644
--- a/src/preprocessing/preprocessing_pass_registry.h
+++ b/src/preprocessing/preprocessing_pass_registry.h
@@ -24,11 +24,7 @@
 #include <string>
 #include <unordered_map>
 
-#include "decision/decision_engine.h"
 #include "preprocessing/preprocessing_pass.h"
-#include "theory/arith/pseudoboolean_proc.h"
-#include "theory/booleans/circuit_propagator.h"
-#include "theory/theory_engine.h"
 
 namespace CVC4 {
 namespace preprocessing {
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 57cf3ac8c..65d3697b7 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -68,8 +68,9 @@
 #include "options/strings_options.h"
 #include "options/theory_options.h"
 #include "options/uf_options.h"
-#include "preprocessing/passes/int_to_bv.h"
 #include "preprocessing/passes/bv_gauss.h"
+#include "preprocessing/passes/int_to_bv.h"
+#include "preprocessing/passes/pseudo_boolean_processor.h"
 #include "preprocessing/preprocessing_pass.h"
 #include "preprocessing/preprocessing_pass_context.h"
 #include "preprocessing/preprocessing_pass_registry.h"
@@ -90,7 +91,6 @@
 #include "smt_util/nary_builder.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arith/arith_msum.h"
-#include "theory/arith/pseudoboolean_proc.h"
 #include "theory/booleans/circuit_propagator.h"
 #include "theory/bv/bvintropow2.h"
 #include "theory/bv/theory_bv_rewriter.h"
@@ -571,7 +571,6 @@ public:
  private:
   std::unique_ptr<PreprocessingPassContext> d_preprocessingPassContext;
   PreprocessingPassRegistry d_preprocessingPassRegistry;
-  theory::arith::PseudoBooleanProcessor d_pbsProcessor;
 
   /** The top level substitutions */
   SubstitutionMap d_topLevelSubstitutions;
@@ -597,8 +596,6 @@ public:
   void removeITEs();
 
   Node realToInt(TNode n, NodeToNodeHashMap& cache, std::vector< Node >& var_eq);
-  Node intToBV(TNode n, NodeToNodeHashMap& cache);
-  Node intToBVMakeBinary(TNode n, NodeToNodeHashMap& cache);
   Node purifyNlTerms(TNode n, NodeToNodeHashMap& cache, NodeToNodeHashMap& bcache, std::vector< Node >& var_eq, bool beneathMult = false);
 
   /**
@@ -685,7 +682,6 @@ public:
     d_exprNames(smt.d_userContext),
     d_iteSkolemMap(),
     d_iteRemover(smt.d_userContext),
-    d_pbsProcessor(smt.d_userContext),
     d_topLevelSubstitutions(smt.d_userContext)
   {
     d_smt.d_nodeManager->subscribeEvents(this);
@@ -2552,10 +2548,15 @@ void SmtEnginePrivate::finishInit() {
   d_preprocessingPassContext.reset(new PreprocessingPassContext(&d_smt));
   // TODO: register passes here (this will likely change when we add support for
   // actually assembling preprocessing pipelines).
-  std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
   std::unique_ptr<BVGauss> bvGauss(new BVGauss(d_preprocessingPassContext.get()));
-  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  std::unique_ptr<IntToBV> intToBV(new IntToBV(d_preprocessingPassContext.get()));
+  std::unique_ptr<PseudoBooleanProcessor> pbProc(
+      new PseudoBooleanProcessor(d_preprocessingPassContext.get()));
+  
   d_preprocessingPassRegistry.registerPass("bv-gauss", std::move(bvGauss));
+  d_preprocessingPassRegistry.registerPass("int-to-bv", std::move(intToBV));
+  d_preprocessingPassRegistry.registerPass("pseudo-boolean-processor",
+                                           std::move(pbProc));
 }
 
 Node SmtEnginePrivate::expandDefinitions(TNode n, unordered_map<Node, Node, NodeHashFunction>& cache, bool expandOnly)
@@ -4268,10 +4269,8 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if( options::pbRewrites() ){
-    d_pbsProcessor.learn(d_assertions.ref());
-    if(d_pbsProcessor.likelyToHelp()){
-      d_pbsProcessor.applyReplacements(d_assertions.ref());
-    }
+    d_preprocessingPassRegistry.getPass("pseudo-boolean-processor")
+        ->apply(&d_assertions);
   }
 
   Trace("smt-proc") << "SmtEnginePrivate::processAssertions() : pre-simplify" << endl;