Add rational parsing to RARE #11282
Merged
Add rational parsing to RARE #11282
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Also adds a several initial rewrites that are possible now, and some basic support for transcendental elimination rules.
Note this PR also makes it so that
cvc5_proof_rule.his not automatically clang-formatted, since it breaks the documentation in that include file.This PR also fixes our printer for RARE rules in Eunoia and removes several rules that are subsumed by ARITH_POLY_NORM and had usages of
(- 1)which were not being translated to Eunoia properly.This furthermore fixes an inconsistency with
printArithLitTokenwhich would print decimals for integral rationals whereas non-integral rationals would be printed as rationals; now both are printed as rationals.This fills in 29 trusted proof steps in our regressions.