In #1192 we add support for the Sign_extend and Repeat symbols, avoiding to build many unnecessary intermediate terms that clutter the union-find. However there are still performance issues, in particular with sign-extensions to (very) large bit-widths because we are still representing the resulting bit-vector as an explicit concatenation at the semantic value level. In particular, this adds a large constant factor to any solving involving such values.
We should consider representing repetitions explicitly in bit-vector semantic values. Since we need semantic values to be canonical, it might be too expensive/complicated to handle arbitrary repetitions, but we can at least handle repetitions of single bits, which would be enough for the sign_extend case.
In #1192 we add support for the
Sign_extendandRepeatsymbols, avoiding to build many unnecessary intermediate terms that clutter the union-find. However there are still performance issues, in particular with sign-extensions to (very) large bit-widths because we are still representing the resulting bit-vector as an explicit concatenation at the semantic value level. In particular, this adds a large constant factor to any solving involving such values.We should consider representing repetitions explicitly in bit-vector semantic values. Since we need semantic values to be canonical, it might be too expensive/complicated to handle arbitrary repetitions, but we can at least handle repetitions of single bits, which would be enough for the
sign_extendcase.