diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2018-08-29 14:38:33 -0700 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-08-29 16:38:33 -0500 |
commit | 3eac9d04c5d4bfba81142d4a5fe91b86590b32ae (patch) | |
tree | e3ed07e7268d57ce27c2f748524bd9ff45859579 /src/preprocessing/preprocessing_pass_context.h | |
parent | 1ae13e7e30aaaa088de057496c649649067867dc (diff) |
Refactor MipLibTrick preprocessing pass. (#2359)
Diffstat (limited to 'src/preprocessing/preprocessing_pass_context.h')
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 21 |
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 |