projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 155e35e) | patch
bv2int: implementing the iand-sum mode (#5265)
authoryoni206 <yoni206@users.noreply.github.com>
Wed, 14 Oct 2020 19:40:13 +0000 (12:40 -0700)
committerGitHub <noreply@github.com>
Wed, 14 Oct 2020 19:40:13 +0000 (14:40 -0500)
commit42dd10f9936c6a9be158842f482cc7ebd4a972ed
treef55e21c2367039abd214e3880644fa769548ed84tree
parent155e35ec2b38771917312d35f784a2e35b4b41d3commit | diff
bv2int: implementing the iand-sum mode (#5265)

There are 3 potential modes to lazily treat the iand operator:
(1) by value (typical CEGAR loop)
(2) by sum (lazily expanding each iand node into a sum of ITEs)
(3) by bit-wise equalities (lazily expanding each iand node into bit-wise equalities)

This PR implements (2).

The relevant option is added to existing tests, and a new test is added. In a few other tests, some options are removed to make them run faster.
18 files changed:
src/theory/arith/inference_id.cpp diff | blob | history
src/theory/arith/inference_id.h diff | blob | history
src/theory/arith/nl/iand_solver.cpp diff | blob | history
src/theory/arith/nl/iand_solver.h diff | blob | history
src/theory/arith/nl/iand_table.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv_to_int1.smt2 diff | blob | history
test/regress/regress1/nl/iand-native-1.smt2 diff | blob | history
test/regress/regress1/nl/iand-native-2.smt2 [new file with mode: 0644] blob
test/regress/regress2/bv_to_int2.smt2 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_bvmul1.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/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_input_mouser_detect.c.smt2.minimized.smt2 diff | blob | history