This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]).
This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations.
Note that this patch is not reverting #1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in #1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y].
The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
Benchmarks: This PR provides a small reasoning boost (+171-48 on the usual QF_BV subset) and a significant performance boost for bit-vector reasoning (-25% on the same QF_BV subset) compared to #1144.
This patch changes the way that bit-vector domains are stored in order to share domains between multiple bit-vectors with the same variable part, including across different bit-width. Currently, if we had terms [x], [00 @ x], and [10 @ x], we would store domains for each of these. With this patch, we only store a domain for [x] and rebuild the domains for [00 @ x] and [10 @ x] dynamically; we do this by computing normal forms composed of a variable part ([x] here) and a constant offset (either [0] or [10]).
This reduces the number of variables handled by the system (which is important for global domains such as global difference) and reduces the number of trivial propagations.
Note that this patch is not reverting #1044. In particular, we are considering [x @ y] as a unique (composite) variable built up from the atomic variables [x] and [y] (in the same way that the polynomial [x + y] is built up from the monomial [x] and [y] in the IntervalCalculus module; in fact, the implementation is intentionally abstracted in order to be useable with polynomials). This is necessary because, as noted in #1044, the interval domain for [x @ y] cannot be built reconstructed precisely from the interval domains for [x] and [y].
The patch includes a bit of refactoring of the way we handle constraints; notably, instead of aggressively substituting constraints, we now store the original constraint and call [Uf.find] at propagation time. This avoids having to define a substitution operation on normal forms and allows storing the constraint dependencies directly inside the domain (in the previous design, we could not do it easily without repeating the expensive substitution of constraint arguments).
Note: depends on https://github.com/OCamlPro/alt-ergo/pull/1144. Only the latest commit with title "feat(BV): Interval domains for bit-vectors" is included in this PR.
Benchmarks: This PR provides a small reasoning boost (+171-48 on the usual QF_BV subset) and a significant performance boost for bit-vector reasoning (-25% on the same QF_BV subset) compared to #1144.