alt-ergo
alt-ergo copied to clipboard
Improving reasoning for the BV theory
This umbrella issue tracks the progression of the BV theory reasoning. Please add related issue here and what we plan to improve in the future.
- [X] Support of
bvnot
reasoning, see #800 and #856. - [X] Constraint propagation for
bvand
,bvor
,bvxor
, etc (see #944) - [ ] Constraint simplification (from
(bvand (concat a b) (concat c d))
to(concat (bvand a c) (bvand b d))
) - [ ] Constraint propagation for
bv2nat
andint2bv
Some updates here:
- Doing constraint propagation on
bv2nat
andint2bv
is not easy to do properly, because we don't have access to the arithmetic domains fromBitv_rel
- This is even more true if we want to do interreductions between arithmetic and bitwise domains
- The plan is now to instead add separate interval domains for bitvectors to
Bitv_rel
and to perform interreductions following Sharpening Constraint Programming approaches for Bit-Vector Theory - #1040 #1044 #1054 #1055 #1056 do some groundwork to prepare the addition of the new domains, including reworking some of the constraint APIs to be easier to use with multiple domains
- Additional PRs are currently being tested that actually add the interval domains & arithmetic propagators following the paper above
- At some point we might want to figure out how to reconcile the BV and Arith interval domains
- No progress on the "constraint simplification" part yet