-
Notifications
You must be signed in to change notification settings - Fork 9
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
Tseitin Encoding #6
Conversation
It'd be great to get your input on this, as I'm still trying to adapt to the style you've used. Took me a while to figure out what you were doing here... @st.composite
def NNF(draw):
return draw(st.recursive(variables(), internal)) ...but it's some awesome stuff! As I was writing the test case, I found myself needing a "forgetting" mechanism (cf. #7 ). Let me know if it happens to be somewhere there under a different name. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I found some problems but this looks good overall.
@blyxxyz Good to merge with this one? Thanks for bearing with me! |
Ouch... Lgtm. Merge away if you're fine with it. Will make kissat optional tonight on the other branch. |
Merged to have a cleaner PR on the kissat integration. Feel free to re-open if anything remains, but I think we're pretty well set here. |
Closes #5