projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 6097316) | patch
bv-to-int: use pow2 operator (#7812)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 16 Dec 2021 16:49:30 +0000 (18:49 +0200)
committerGitHub <noreply@github.com>
Thu, 16 Dec 2021 16:49:30 +0000 (16:49 +0000)
commitadd28ea44dd1c63191c9ca8b4efc114dfb9d95d7
treee8d9098c8def82f46f9cedb19f9a72362531bc4ctree
parent60973169af7ad8653436fc6497e13e25897ed578commit | diff
bv-to-int: use pow2 operator (#7812)

Currently, the int-blaster translates shifts using an ite whose size is the bit-width.
This PR adds an option to use the internal pow2 operator instead.
src/options/smt_options.toml diff | blob | history
src/theory/bv/int_blaster.cpp diff | blob | history
test/regress/regress2/bv_to_int_ashr.smt2 diff | blob | history
test/regress/regress2/bv_to_int_bitwise.smt2 diff | blob | history
test/regress/regress2/bv_to_int_shifts.smt2 diff | blob | history
test/regress/regress3/bv_to_int_check_bvsge_bvashr0_4bit.smt2.minimized.smt2 diff | blob | history
test/regress/regress3/bv_to_int_check_bvsgt_bvlshr0_4bit.smt2.minimized.smt2 diff | blob | history
test/regress/regress3/bv_to_int_quant1.smt2 diff | blob | history