projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: abc5af4) | patch
bv2int: improvement in lazy failures (#5020)
authoryoni206 <yoni206@users.noreply.github.com>
Thu, 10 Sep 2020 01:32:55 +0000 (18:32 -0700)
committerGitHub <noreply@github.com>
Thu, 10 Sep 2020 01:32:55 +0000 (20:32 -0500)
commit98f808f01735c6cebfbf945fcb072da3ba6cff6c
tree028c36481b9d5fdf9d942f258356cc2fae61e5a1tree
parentabc5af448a464615018c020c9ec6bb1e8dd4d48ccommit | diff
bv2int: improvement in lazy failures (#5020)

Previously, in case we encountered a term we cannot translate to integers (e.g. a bit-vector array), we would fail.
This PR improves that behavior by keeping the original term, and potentially wrapping it BV_TO_NAT and INT_TO_BV operators.

A test which includes a bit-vector array is included, which was not supported before.

In addition, the treatment of uninterpreted functions is refactored and documented better.
src/preprocessing/passes/bv_to_int.cpp diff | blob | history
src/preprocessing/passes/bv_to_int.h diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress2/bv_to_int_mask_array_3.smt2 [new file with mode: 0644] blob