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.

1 files changed, 2 insertions, 2 deletions

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. */