-
Notifications
You must be signed in to change notification settings - Fork 42
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Truncate-of-weighted-sum rewrite is too aggressive #362
Comments
brianhuffman
pushed a commit
that referenced
this issue
Dec 5, 2019
Instead of modifying coefficients in a weighted sum, we now restrict ourselves to zeroing out coefficients that are equivalent to zero modulo 2^n. Fixes #362.
That's a really interesting knock-on effect. Does it makes sense to try to be an intermediate level of aggressive, where we reduce modulo 2^n iff that doesn't increase the distance from 0 in the signed interpretation (i.e. for positive values)? I rather doubt it would help much but shrug. |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Pull request #343 added a rule that simplifies certain bit-selects applied to weighted sums of bitvectors: When the lower n bits are selected, it truncates all coefficients in the weighted sum down to n bits.
It turns out that this is not always desirable, especially when the coefficient is a number like -1. Truncation (for example, from 1024 bits down to 64) can result in a number that is much farther from 0, and that solvers have a hard time dealing with. This problem is showing up in some of the s2n proofs: goals that yices used to handle easily are now transformed into ones that yices takes forever on.
We need to be more conservative with this rewrite: Instead of reducing all coefficients mod 2^n, we should just filter out those terms with coefficients equivalent to 0 mod 2^n.
The text was updated successfully, but these errors were encountered: