Refactor MipLibTrick preprocessing pass. (#2359)

1 files changed, 18 insertions, 3 deletions

diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h
index 96e554680..a2e83aa4c 100644
--- a/src/preprocessing/preprocessing_pass_context.h
+++ b/src/preprocessing/preprocessing_pass_context.h
@@ -26,6 +26,7 @@
 #include "preprocessing/util/ite_utilities.h"
 #include "smt/smt_engine.h"
 #include "smt/term_formula_removal.h"
+#include "theory/booleans/circuit_propagator.h"
 #include "theory/theory_engine.h"
 #include "util/resource_manager.h"
 
@@ -35,9 +36,12 @@ namespace preprocessing {
 class PreprocessingPassContext
 {
  public:
-  PreprocessingPassContext(SmtEngine* smt,
-                           ResourceManager* resourceManager,
-                           RemoveTermFormulas* iteRemover);
+  PreprocessingPassContext(
+      SmtEngine* smt,
+      ResourceManager* resourceManager,
+      RemoveTermFormulas* iteRemover,
+      theory::booleans::CircuitPropagator* circuitPropagator);
+
   SmtEngine* getSmt() { return d_smt; }
   TheoryEngine* getTheoryEngine() { return d_smt->d_theoryEngine; }
   DecisionEngine* getDecisionEngine() { return d_smt->d_decisionEngine; }
@@ -46,6 +50,11 @@ class PreprocessingPassContext
   context::Context* getDecisionContext() { return d_smt->d_context; }
   RemoveTermFormulas* getIteRemover() { return d_iteRemover; }
 
+  theory::booleans::CircuitPropagator* getCircuitPropagator()
+  {
+    return d_circuitPropagator;
+  }
+
   void spendResource(unsigned amount)
   {
     d_resourceManager->spendResource(amount);
@@ -56,6 +65,9 @@ class PreprocessingPassContext
   /* Widen the logic to include the given theory. */
   void widenLogic(theory::TheoryId id);
 
+  /* Enable Integers. */
+  void enableIntegers();
+
  private:
   /* Pointer to the SmtEngine that this context was created in. */
   SmtEngine* d_smt;
@@ -63,6 +75,9 @@ class PreprocessingPassContext
 
   /** Instance of the ITE remover */
   RemoveTermFormulas* d_iteRemover;
+
+  /** Instance of the circuit propagator */
+  theory::booleans::CircuitPropagator* d_circuitPropagator;
 };  // class PreprocessingPassContext
 
 }  // namespace preprocessing