Refactor IteRemoval preprocessing pass (#1793)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 17 Aug 2018 01:57:24 +0000 (18:57 -0700)
committerGitHub <noreply@github.com>
Fri, 17 Aug 2018 01:57:24 +0000 (18:57 -0700)
commite6fd3c70f8651c6a9055fad8933caf2596b2b651
tree4cc0809a2aa4fed311bca9f41eee04c935578eb7
parent7fc04bf78c6c20f3711d14425469eef2e0c2cd60
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.
src/Makefile.am
src/preprocessing/passes/ite_removal.cpp [new file with mode: 0644]
src/preprocessing/passes/ite_removal.h [new file with mode: 0644]
src/preprocessing/preprocessing_pass.h
src/preprocessing/preprocessing_pass_context.cpp
src/preprocessing/preprocessing_pass_context.h
src/smt/smt_engine.cpp