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.

Sign up for GitHub

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

Jump to bottom

Segfault when attempting 0/1 equiv 0/1 #15

Closed
cjdrake opened this issue Apr 25, 2016 · 1 comment
Closed

Segfault when attempting 0/1 equiv 0/1 #15

cjdrake opened this issue Apr 25, 2016 · 1 comment
Labels
bug

Comments

@cjdrake
Copy link
Owner

cjdrake commented Apr 25, 2016 •
edited 

>>> from boolexpr import ZERO
>>> ZERO.equiv(ZERO)
Segmentation fault (core dumped)

>>> from boolexpr import ONE
>>> ONE.equiv(ONE)
Segmentation fault (core dumped)
@cjdrake cjdrake added the bug label Apr 25, 2016
@cjdrake cjdrake changed the title Segfault when attempting ZERO.equiv(ZERO) Segfault when attempting 0/1 equiv 0/1 Apr 25, 2016
@cjdrake
Copy link
Owner Author

cjdrake commented Apr 25, 2016

Problem is in Operator::sat(). Since Tseytin transform doesn't simplify, you end up with 0/1 at the leaf nodes, and the code assumes literals.

cjdrake added a commit that referenced this issue Apr 26, 2016
@cjdrake
Fix issue #15, segfault w/ non-simple tseytin
c90fe0c 
Restructure sat so that it simplifies first,
then calls _sat underneath.
This guarantees that Operator::_sat has no constants in the tree,
which was problematic for the call to CryptoMiniSat below.
@cjdrake cjdrake closed this as completed Apr 26, 2016
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@cjdrake