Skip to content
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

Merged
merged 19 commits into from
Jul 31, 2020
Merged

Tseitin Encoding #6

merged 19 commits into from
Jul 31, 2020

Conversation

haz
Copy link
Collaborator

@haz haz commented Jul 23, 2020

Closes #5

@haz haz changed the title [WIP] Tseitin Encoding Tseitin Encoding Jul 24, 2020
@haz haz requested a review from blyxxyz July 24, 2020 03:10
@haz
Copy link
Collaborator Author

haz commented Jul 24, 2020

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.

Copy link
Collaborator

@blyxxyz blyxxyz left a 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.

nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
test_nnf.py Outdated Show resolved Hide resolved
nnf/tseitin.py Outdated Show resolved Hide resolved
@haz
Copy link
Collaborator Author

haz commented Jul 30, 2020

@blyxxyz Good to merge with this one? Thanks for bearing with me!

@haz
Copy link
Collaborator Author

haz commented Jul 30, 2020

Ouch...T.models vs models is what I get for last minute commits.

Lgtm. Merge away if you're fine with it. Will make kissat optional tonight on the other branch.

@haz haz merged commit 9d34688 into master Jul 31, 2020
@haz
Copy link
Collaborator Author

haz commented Jul 31, 2020

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.

@haz haz mentioned this pull request Jul 31, 2020
@blyxxyz blyxxyz deleted the tseitin branch July 31, 2020 23:04
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Include a Tseiten encoding
2 participants