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
SMT-Lib printing: Handle predicate objects from new assumptions #25245
Conversation
✅ Hi, I am the SymPy bot (v170). I'm here to help you write a release notes entry. Please read the guide on how to write release notes. Your release notes are in good order. Here is what the release notes will look like: This will be added to https://github.com/sympy/sympy/wiki/Release-Notes-for-1.13. Click here to see the pull request description that was parsed.
Update The release notes on the wiki have been updated. |
@kunalsheth I know you wrote the original SMT-LIB printing code in SymPy. You may be interested in some of the changes being made here. |
I need to remove the "Started to implement EncodedCNF printing" commit before this ready to merge. |
c7e0aec
to
d782cd7
Compare
How do I cancel a review request? That happened automatically. I messed up my git rebase and it forgot I merged master which caused it to think there are like 50 more commits than there actually should be. |
The smtlib_code function will no longer throw an error when it tries to print some predicate from the new assumptions. The printer throws an error if given a predicate that can’t be translated to SMT-Lib or could be but hasn’t been Implemented. While it’s possible to handle even, odd, and some other predicate, this isn’t really all that important so this functionality was dropped. Example: In [1]: from sympy.printing.smtlib import smtlib_code In [2]: from sympy.assumptions.ask import Q In [3]:smtlib_code(Q.positive(x)) Out[3]]: '(declare-const x Real)\n(assert (> x 0))'
d782cd7
to
d20130a
Compare
@moorepants you can ignore this pull request. |
Benchmark results from GitHub Actions Lower numbers are good, higher numbers are bad. A ratio less than 1 Significantly changed benchmark results (PR vs master) Significantly changed benchmark results (master vs previous release) before after ratio
[8059df73] [42803477]
<sympy-1.12^0>
- 82.8±1ms 54.9±0.2ms 0.66 integrate.TimeIntegrationRisch02.time_doit(10)
Full benchmark results can be found as artifacts in GitHub Actions |
The smtlib_code function will no longer throw an error when it tries to print some predicate from the new assumptions. The printer throws an error if given a predicate that can’t be translated to SMT-Lib or could be but hasn’t been Implemented. While it’s possible to handle even, odd, and some other predicate, this isn’t really all that important so this functionality was dropped.
Example:
In [1]: from sympy.printing.smtlib import smtlib_code
In [2]: from sympy.assumptions.ask import Q
In [3]:smtlib_code(Q.positive(x))
Out[3]]: '(declare-const x Real)\n(assert (> x 0))'
References to other Issues or PRs
This is a continuation of this pull request #25232. I worked on a lot of stuff that didn't seem to be a priority so this pull request contains the most essential bits of that one without any distracting commits or comments.
Other Comments
@kunalsheth if you want to review this it would be appreciated.
Release Notes