projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a3b9a99) | patch
bv_to_int preprocessing pass
authoryoni206 <yoni206@users.noreply.github.com>
Tue, 25 Feb 2020 03:58:01 +0000 (19:58 -0800)
committerGitHub <noreply@github.com>
Tue, 25 Feb 2020 03:58:01 +0000 (19:58 -0800)
commit6e17dd6d5e3ec043e5edd097ac6a736f6a41c753
tree5faac828524e121bcba8cd2d4f1c09bb46cadcfetree
parenta3b9a99404ee00bde5db42aab63ab08df3712ba3commit | diff
bv_to_int preprocessing pass

Introduces a preprocessing pass that translates bv problems to integer problems.
19 files changed:
src/CMakeLists.txt diff | blob | history
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/bv_to_int.cpp [new file with mode: 0644] blob
src/preprocessing/passes/bv_to_int.h [new file with mode: 0644] blob
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/bv/bv_to_int1.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int2.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_bitwise.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_bvmul1.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_bvmul2.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bv_to_int_zext.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bvuf_to_intuf.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 [new file with mode: 0644] blob
test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 [new file with mode: 0644] blob
test/regress/regress2/bv_to_int_ashr.smt2 [new file with mode: 0644] blob
test/regress/regress2/bv_to_int_shifts.smt2 [new file with mode: 0644] blob
test/regress/regress3/bv_to_int_and_or.smt2 [new file with mode: 0644] blob