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
[Merged by Bors] - perf(linarith): don't repeat nonneg proofs for nat-to-int casts #3226
Conversation
again, linarith improvements find unneeded hypotheses in the trig file
I have absolutely no idea why this changed the behavior in the trig functions file. It should only be about nat preprocessing, and there are no nats there. |
Thanks Kevin -- I was just blindly following the linter when I fixed those, but yes, those and more can go. I've changed those here. But maybe we need a full review of that file (in another PR?). |
bors merge |
This performance issue showed up particularly when using `nlinarith` over `nat`s. Proofs that `(n : int) >= 0` were being repeated many times, which led to quadratic blowup in the `nlinarith` preprocessing. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
Pull request successfully merged into master. Build succeeded: |
…prover-community#3226) This performance issue showed up particularly when using `nlinarith` over `nat`s. Proofs that `(n : int) >= 0` were being repeated many times, which led to quadratic blowup in the `nlinarith` preprocessing. Co-authored-by: Rob Lewis <rob.y.lewis@gmail.com>
This performance issue showed up particularly when using
nlinarith
overnat
s. Proofs that(n : int) >= 0
were being repeated many times, which led to quadratic blowup in thenlinarith
preprocessing.