projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 94feff6) | patch
Make ackermannization generally applicable rather than just BV (#3315)
authorYing Sheng <sqy1415@gmail.com>
Tue, 8 Oct 2019 15:18:21 +0000 (08:18 -0700)
committerAndres Noetzli <andres.noetzli@gmail.com>
Tue, 8 Oct 2019 15:18:21 +0000 (08:18 -0700)
commit00ccc01140bcdeaadedf8ae1b9f224ccdc812bc0
treebc4981945d06c25d57854fbf2651431061e9ae42tree
parent94feff6c3b03325115e2c1c91121b83945dba4b0commit | 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.
16 files changed:
src/CMakeLists.txt diff | blob | history
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/ackermann.cpp [new file with mode: 0644] blob
src/preprocessing/passes/ackermann.h [new file with mode: 0644] blob
src/preprocessing/passes/bv_ackermann.cpp [deleted file] blob | history
src/preprocessing/passes/bv_ackermann.h [deleted file] blob | history
src/preprocessing/preprocessing_pass_registry.cpp diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/arith/ackermann.real.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann1.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann2.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann3.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann4.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann5.smt2 [new file with mode: 0644] blob
test/regress/regress0/arith/integers/ackermann6.smt2 [new file with mode: 0644] blob