[bitv] Expand the pattern after B-variable splitting #686
Conversation
bclement-ocp
force-pushed
the
bclement/bsubs
branch
2 times, most recently
from
678d5a0
to
a2a2dac
Compare
|
I messed up the rebase and forgot the tests, should be good now @hra687261 |
|
The build failure is due to Gbury/dolmen#162 being merged. I wlil make a PR shortly to remove |
This patch rewrites the `slice_composition` function to take care of two edge cases: - First, it may happen that spliting a B variable causes another instance of the same B variable to become smaller than its expected size in the pattern. When that happens, we record the information, recompute the pattern, then re-slice the whole system. - Second, it may happen that we split the *second* (or third or...) occurence of a B variable. In this case, `slice_composition` is currently only substituting on the remainder of the composition, and so the first occurence is not substituted. To fix that case, we keep the substitution of B variables around, and apply it to the whole equation once it has been sliced. This can again change the pattern and cause re-slicing. Note that this keeps the "one-var-to-two-vars" implementation of substitutions. As discussed in OCamlPro#680, we should switch to a non-recursive version, but this is unrelated to the issues fixed by this patch. Fixes OCamlPro#645
bclement-ocp
force-pushed
the
bclement/bsubs
branch
from
a2a2dac
to
0a7afc2
Compare
src/lib/reasoners/bitv.ml
Outdated
| Splits involving A variables are not recorded, because A variables are | ||
| guaranteed to have unique occurences. | ||
|
|
||
| Splits involving B and C variables are accumulated in [subs]. |
There was a problem hiding this comment.
Hm, difference will probably be insignificant, but would there be a point in splitting subs into b_subs and c_subs? Since B variables can appear multiple times but only in a single composition, while C variables can appear multiple time but not in the same composition, I don't think that it is needed to have both substitutions in the same place.
There was a problem hiding this comment.
Unless I am mistaken/misremembering, subs should be a pair (b_subs, c_subs) for this exact reason. I could clarify the comment.
This patch rewrites the
slice_compositionfunction to take care of two edge cases:First, it may happen that spliting a B variable causes another instance of the same B variable to become smaller than its expected size in the pattern. When that happens, we record the information, recompute the pattern, then re-slice the whole system.
Second, it may happen that we split the second (or third or...) occurence of a B variable. In this case,
slice_compositionis currently only substituting on the remainder of the composition, and so the first occurence is not substituted. To fix that case, we keep the substitution of B variables around, and apply it to the whole equation once it has been sliced. This can again change the pattern and cause re-slicing.Note that this keeps the "one-var-to-two-vars" implementation of substitutions. As discussed in #680, we should switch to a non-recursive version, but this is unrelated to the issues fixed by this patch.
Fixes #645