summaryrefslogtreecommitdiff
path: root/src/preprocessing/preprocessing_pass_context.cpp
diff options
context:
space:
mode:
authorAndres Noetzli <andres.noetzli@gmail.com>2018-08-16 18:57:24 -0700
committerGitHub <noreply@github.com>2018-08-16 18:57:24 -0700
commite6fd3c70f8651c6a9055fad8933caf2596b2b651 (patch)
tree4cc0809a2aa4fed311bca9f41eee04c935578eb7 /src/preprocessing/preprocessing_pass_context.cpp
parent7fc04bf78c6c20f3711d14425469eef2e0c2cd60 (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.cpp')
-rw-r--r--src/preprocessing/preprocessing_pass_context.cpp6
1 files changed, 4 insertions, 2 deletions
diff --git a/src/preprocessing/preprocessing_pass_context.cpp b/src/preprocessing/preprocessing_pass_context.cpp
index 1f3d245d7..31987b00b 100644
--- a/src/preprocessing/preprocessing_pass_context.cpp
+++ b/src/preprocessing/preprocessing_pass_context.cpp
@@ -20,8 +20,10 @@ namespace CVC4 {
namespace preprocessing {
PreprocessingPassContext::PreprocessingPassContext(
- SmtEngine* smt, ResourceManager* resourceManager)
- : d_smt(smt), d_resourceManager(resourceManager)
+ SmtEngine* smt,
+ ResourceManager* resourceManager,
+ RemoveTermFormulas* iteRemover)
+ : d_smt(smt), d_resourceManager(resourceManager), d_iteRemover(iteRemover)
{
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback