refactor(bv): Simplify bv2nat mapping using right shifts#1320
refactor(bv): Simplify bv2nat mapping using right shifts#1320bclement-ocp wants to merge 3 commits into
Conversation
bclement-ocp
force-pushed
the
bclement/bv2nat-asr
branch
from
08b8ca3 to
bf052b9
Compare
bclement-ocp
force-pushed
the
bclement/bv2nat-asr
branch
9 times, most recently
from
9bc2300 to
eb35a3a
Compare
|
|
||
| (* Add the equality [nat_r = bv2nat(bv_r)]. *) | ||
| let add_bv2nat ~ex nat_r bv_r t = | ||
| match BitvNormalForm.normal_form bv_r with |
There was a problem hiding this comment.
What is the motivation of this change? If I understand well, you replace the normal form of Bitv_rel by the normal form of Bitv?
There was a problem hiding this comment.
(Sorry, realized I have left this comment as "pending" — hopefully it still makes some sense…)
It's not really useful to compute the BitvNormalForm here, the loop in add_bv2nat_abstract already processes this and it's simpler.
The BitvNormalForm distinguishes between constants / variables (concatenation of constants and exactly one variable) / composites (arbitrary concatenations), which is useful when doing reductions. But here we don't really care about this distinction, we just need to be able to iterate on the components of the concatenation to decompose the bv2nat expression — I think I failed to recognise this when writing the code initially and it ended up more convoluted than necessary.
bclement-ocp
force-pushed
the
bclement/bv2nat-asr
branch
from
eb35a3a to
7bf6e2a
Compare
And add it to the lockfile, so that the workflows that use a lock file can build (:
To simplify review of the next commit.
The bv2nat mapping is able to record an integer expression for each bit-vector extraction, but we only need to record arithmetic right shifts since we encode an extraction `bv<i, j>` as `(bv asr j) - (bv asr i) * 2^(j - i + 1)`. This ensures we can't accidentally leave bogus extractions in the map.
bclement-ocp
force-pushed
the
bclement/bv2nat-asr
branch
from
7bf6e2a to
4fd9d98
Compare
2 participants
The bv2nat mapping is able to record an integer expression for each bit-vector extraction, but we only need to record arithmetic right shifts since we encode an extraction
bv<i, j>as(bv asr j) - (bv asr i) * 2^(j - i + 1).This ensures we can't accidentally leave bogus extractions in the map.