diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-03-05 17:23:45 -0800 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-03-05 17:23:45 -0800 |
commit | ba6ade0fc3f4cd339885652bb9bf5c87113c498d (patch) | |
tree | 5823f632aca0903109d7ccabedffeae65ac6f637 /src/preprocessing/preprocessing_pass_registry.cpp | |
parent | e1845f92742854a35c294541bd931b898b0211d2 (diff) |
Remove --apply-to-const preprocessing pass (#3919)
Fixes #3914. The pass was only applicable to inputs with UFs that were
exclusively applied to single integer values. This limitation seems to
make the preprocessing pass not very useful in practice and it is
subsumed by our Ackermannization pass, which can remove UFs from more
complex inputs. Thus, this commit removes the preprocessing pass.
Diffstat (limited to 'src/preprocessing/preprocessing_pass_registry.cpp')
-rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 2 |
1 files changed, 0 insertions, 2 deletions
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 154ed9086..9272bbb5a 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -25,7 +25,6 @@ #include "base/output.h" #include "preprocessing/passes/ackermann.h" #include "preprocessing/passes/apply_substs.h" -#include "preprocessing/passes/apply_to_const.h" #include "preprocessing/passes/bool_to_bv.h" #include "preprocessing/passes/bv_abstraction.h" #include "preprocessing/passes/bv_eager_atoms.h" @@ -122,7 +121,6 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("bv-gauss", callCtor<BVGauss>); registerPassInfo("static-learning", callCtor<StaticLearning>); registerPassInfo("ite-simp", callCtor<ITESimp>); - registerPassInfo("apply-to-const", callCtor<ApplyToConst>); registerPassInfo("global-negate", callCtor<GlobalNegate>); registerPassInfo("int-to-bv", callCtor<IntToBV>); registerPassInfo("bv-to-int", callCtor<BVToInt>); |