diff options
| author | Ying Sheng <sqy1415@gmail.com> | 2019-10-08 08:18:21 -0700 |
|---|---|---|
| committer | Andres Noetzli <andres.noetzli@gmail.com> | 2019-10-08 08:18:21 -0700 |
| commit | 00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0 (patch) | |
| tree | bc4981945d06c25d57854fbf2651431061e9ae42 /src/preprocessing/preprocessing_pass_registry.cpp | |
| parent | 94feff6c3b03325115e2c1c91121b83945dba4b0 (diff) | |
Make ackermannization generally applicable rather than just BV (#3315)
The ackermannization process is currently already support general theories rather than specifically for BV. In this pull request, an option has been added to turn on ackermannization independently.
Diffstat (limited to 'src/preprocessing/preprocessing_pass_registry.cpp')
| -rw-r--r-- | src/preprocessing/preprocessing_pass_registry.cpp | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/preprocessing/preprocessing_pass_registry.cpp b/src/preprocessing/preprocessing_pass_registry.cpp index 36b3c6392..82132774b 100644 --- a/src/preprocessing/preprocessing_pass_registry.cpp +++ b/src/preprocessing/preprocessing_pass_registry.cpp @@ -23,11 +23,11 @@ #include "base/cvc4_assert.h" #include "base/map_util.h" #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_ackermann.h" #include "preprocessing/passes/bv_eager_atoms.h" #include "preprocessing/passes/bv_gauss.h" #include "preprocessing/passes/bv_intro_pow2.h" @@ -142,7 +142,7 @@ PreprocessingPassRegistry::PreprocessingPassRegistry() registerPassInfo("ite-removal", callCtor<IteRemoval>); registerPassInfo("miplib-trick", callCtor<MipLibTrick>); registerPassInfo("non-clausal-simp", callCtor<NonClausalSimp>); - registerPassInfo("bv-ackermann", callCtor<BVAckermann>); + registerPassInfo("ackermann", callCtor<Ackermann>); registerPassInfo("sym-break", callCtor<SymBreakerPass>); registerPassInfo("ext-rew-pre", callCtor<ExtRewPre>); registerPassInfo("theory-preprocess", callCtor<TheoryPreprocess>); |