projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 9aab4da) | patch
Changing bv_to_int options (#4721)
authoryoni206 <yoni206@users.noreply.github.com>
Sat, 11 Jul 2020 11:39:56 +0000 (04:39 -0700)
committerGitHub <noreply@github.com>
Sat, 11 Jul 2020 11:39:56 +0000 (06:39 -0500)
commitc481454a4b05a78ea99e835ec7427a719a2d5c77
tree9e1b3d680f2ffe418317c014fd4e733ff68cc0a5tree
parent9aab4da2460b62273ac937ad96b7b6695b904e0dcommit | diff
Changing bv_to_int options (#4721)

This PR changes --solve-bv-as-int from a numerical option (specifying the granularity) to an enum (specifying the approach). Currently we support only two modes: OFF and SUM. Future PRs will add more modes.
The numerical value of the granularity is now captured by the new option --bvand-integer-granularity.
Tests are updated accordingly.
19 files changed:
src/options/smt_options.toml diff | blob | history
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/smt/process_assertions.cpp diff | blob | history
src/smt/set_defaults.cpp diff | blob | history
test/regress/regress0/bv/bv_to_int1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int2.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bitwise.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvmul1.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_bvmul2.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_elim_err.smt2 diff | blob | history
test/regress/regress0/bv/bv_to_int_zext.smt2 diff | blob | history
test/regress/regress0/bv/bvuf_to_intuf.smt2 diff | blob | history
test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 diff | blob | history
test/regress/regress0/bv/bvuf_to_intuf_sorts.smt2 diff | blob | history
test/regress/regress2/bv_to_int_ashr.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_1.smt2 diff | blob | history
test/regress/regress2/bv_to_int_mask_array_2.smt2 diff | blob | history
test/regress/regress2/bv_to_int_shifts.smt2 diff | blob | history
test/regress/regress3/bv_to_int_and_or.smt2 diff | blob | history