feat(BV): Add support for bv2nat/int2bv normal forms #1154
Merged
Commits on Aug 19, 2024
-
feat(BV): Add support for bv2nat/int2bv normal forms
Currently, Alt-Ergo knows the value of [bv2nat] and [int2bv] on constants. We also perform some simplifications during semantic value creation; however, these simplifications are not integrated into the rest of the solver. For instance, we know that [bv2nat(x @ y)] is equal to [bv2nat(x) * 2^n + bv2nat(y)] (where [n] is the bit-width of [y]), but we don't know that [z] is equal to the same under the hypothesis that [z = x @ y]. This patch moves these simplifications to the [Bitv_rel] module, making them an integral part of the solving process. Since we can't compute [bv2nat] (or [int2bv]) of an arbitrary semantic value, we generate fresh variables to represent them when needed.
-
-
-
-
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.