-
Notifications
You must be signed in to change notification settings - Fork 7.1k
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
fix: CNF with mutually exclusive atoms reduction #64256
Conversation
This is an automated comment for commit c7aa283 with description of existing statuses. It's updated for the latest CI running ❌ Click here to open a full report in a separate page
Successful checks
|
Co-authored-by: Antonio Andelic <[email protected]>
Stress tests failure looks unrelated -- same reason as #64053 |
@antonio2368 is it ok if I merge->rebase? Auto merge might not be triggered due to the failures, and there were some modifications for upgrade check last week, probably fixing an issue with the job in this PR |
@korowa I tried to restart our private workflow which is blocking the merge. If it doesn't work you can merge master into this to restart the CI |
@antonio2368 got it, thank you. Will do, then, if it still will be open. |
f2d4ec3
Changelog category (leave one):
Changelog entry (a user-readable short description of the changes that goes to CHANGELOG.md):
Fixed CNF simplification, in case any OR group contains mutually exclusive atoms.
Documentation entry for user-facing changes
CI Settings
NOTE: If your merge the PR with modified CI you MUST KNOW what you are doing
NOTE: Checked options will be applied if set before CI RunConfig/PrepareRunConfig step
Run these jobs only (required builds will be added automatically):
Deny these jobs:
Extra options:
Only specified batches in multi-batch jobs:
Closes #57400
Currently reduceOnceCNFStatemtns may produce incorrect result in case any of statements is OR group with mutually exclusive atoms (e.g.
x OR !x
). Added an additional check to prevent incorrect results + prior filtering of such groups as "always true".