-
Notifications
You must be signed in to change notification settings - Fork 38
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
test: prop test for error report and refactor #129
Conversation
7ea5da5
to
4b9dd03
Compare
Rebased + happy clippy + fmt fix |
4b9dd03
to
c751c38
Compare
Pull out some redundant code for checking with sat |
This just affects test code, so hopefully we can keep it moving. |
Nice! |
ping? |
c751c38
to
3e11fca
Compare
Added a profile override to make (sat) tests run faster. Which let me run |
61031d6
to
1761415
Compare
Backed out the override changes, even with the override the test was still too slow to run without |
1761415
to
6fc85a5
Compare
Rebased. And this just affects test code, so starting a 10 day timer. |
6fc85a5
to
42867f9
Compare
42867f9
to
fffa758
Compare
10 day timer is over with no objection. I will muck with settings so that I can self approve. |
Removing a dependency from a dependency provider can only make more resolves succeed. Therefore, an interesting test is to look at our error reporting for some resolve, and we resolve with a dependency provider that only has dependency requirements mentioned in our report. If this subsequent run were to pass, then we have demonstrated that the error report did not include enough information to constitute a proof of unsatisfiability.
While working on the code I moved some code out of the proptest macro, as auto complete and formatting works better on non-macro code.
It would be nice to be able to test our proof of unsatisfiability against the failure information from the SAT solver. I was not able to figure out how to do this. I did find several small things that could be cleaned up about the implementation for SAT embedding.