diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2018-08-16 18:57:24 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2018-08-16 18:57:24 -0700 |
commit | e6fd3c70f8651c6a9055fad8933caf2596b2b651 (patch) | |
tree | 4cc0809a2aa4fed311bca9f41eee04c935578eb7 /src/preprocessing/preprocessing_pass_context.h | |
parent | 7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (diff) |
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.
Diffstat (limited to 'src/preprocessing/preprocessing_pass_context.h')
-rw-r--r-- | src/preprocessing/preprocessing_pass_context.h | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/src/preprocessing/preprocessing_pass_context.h b/src/preprocessing/preprocessing_pass_context.h index 9927cd8fb..b50421e6c 100644 --- 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 |