projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: c101a6b) | patch
Support ackermannization on uninterpreted sorts in BV (#3372)
authorYing Sheng <sqy1415@gmail.com>
Mon, 16 Dec 2019 19:42:36 +0000 (11:42 -0800)
committerAndres Noetzli <andres.noetzli@gmail.com>
Mon, 16 Dec 2019 19:42:36 +0000 (11:42 -0800)
commit49f0f09c6ef1c04fcd5b088456cea9998cff3c91
tree0d5746c90c1e7ca3e336a8cfc7417b05c0eecbe8tree
parentc101a6b42d1f14bc750fb2328ddd83261148d7aecommit | diff
Support ackermannization on uninterpreted sorts in BV (#3372)

Support ackermannization on uninterpreted sorts in BV. For uninterpreted sorts, we create a bit-vector sort to replace it. For an uninterpreted sort `S`, if the number of variables within sort `S` is `n`, the replacing bit-vector will have size (log n)+1.
src/preprocessing/passes/ackermann.cpp diff | blob | history
src/preprocessing/passes/ackermann.h diff | blob | history
src/smt/smt_engine.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/ackermann5.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/ackermann6.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/ackermann7.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/ackermann8.smt2 [new file with mode: 0644] blob
test/unit/theory/theory_bv_white.h diff | blob | history