diff options
| author | Yancheng Ou <ou2@ualberta.ca> | 2021-04-05 06:21:40 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-05 08:21:40 -0500 |
| commit | 3f1ab5672ca746a4a6573e1ebf9f74d72978d1cf (patch) | |
| tree | 86518c88e615cbf7cc0cc3d37cc9866d1bfbb6c4 /src/CMakeLists.txt | |
| parent | 69b463e1b1150715b2f4179786ddab8ba0c43b37 (diff) | |
Optimizer for BitVectors (#6213)
Adds support for BitVector optimization, which is done via offline binary search. Units tests included.
Also mildly refactors the optimizer architecture.
Diffstat (limited to 'src/CMakeLists.txt')
| -rw-r--r-- | src/CMakeLists.txt | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 490d335a2..6c2af8226 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -47,6 +47,12 @@ libcvc4_add_sources( lib/replacements.h lib/strtok_r.c lib/strtok_r.h + omt/bitvector_optimizer.cpp + omt/bitvector_optimizer.h + omt/integer_optimizer.cpp + omt/integer_optimizer.h + omt/omt_optimizer.cpp + omt/omt_optimizer.h preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h preprocessing/passes/ackermann.cpp |