w4_abc_{aiger,verilog}: Handle variable-less properties correctly
#1943
Conversation
This file contains hidden or 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
Previously, any proofs involving the `w4_abc_aiger` (a.k.a., `abc`) or `w4_abc_verilog` proof scripts would succeed if they did not involve any variables, even false properties (e.g., `False`). This happened for a very silly reason: the counterexamples that the `abc` would generate contained a blank output (since there are no variables to describe), and SAW was misinterpreting this as a successful proof. Oops! With this patch, SAW now properly distinguishes between an successful proof (in which case no counterexample file will be generated) and a unsuccessful proof involving no variables (in which case a blank counterexample file will be generated). This is admittedly a bit fiddly, as it requires making some assumptions about the format of the counterexample files that `abc` produces. Nevertheless, this does work on all the examples that I have tried. Fixes #1938.
qsctr
approved these changes
Sep 20, 2023
Collaborator
qsctr
left a comment
qsctr
left a comment
There was a problem hiding this comment.
Thanks for fixing this! I don't know too much about SAW backend stuff but based on what you said in the ticket this looks good to me.
RyanGlScott
added
the
PR: ready to merge
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.
Previously, any proofs involving the
w4_abc_aiger(a.k.a.,abc) orw4_abc_verilogproof scripts would succeed if they did not involve any variables, even false properties (e.g.,False). This happened for a very silly reason: the counterexamples that theabcwould generate contained a blank output (since there are no variables to describe), and SAW was misinterpreting this as a successful proof. Oops!With this patch, SAW now properly distinguishes between an successful proof (in which case no counterexample file will be generated) and a unsuccessful proof involving no variables (in which case a blank counterexample file will be generated). This is admittedly a bit fiddly, as it requires making some assumptions about the format of the counterexample files that
abcproduces. Nevertheless, this does work on all the examples that I have tried.Fixes #1938.