-
Notifications
You must be signed in to change notification settings - Fork 10
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
Panic at CreuSAT/src/parser.rs:130:14 on simple formula #44
Comments
Hi, thank you. This does not look like a valid cnf formula to me — there is no |
(and yes the parser should ideally not panic. I have never bothered to make a very nice parser, and I also believe the current one has some bugs. I did make a nicer parser for a different project at some point, but never got around to including it here.) |
Thanks @sarsko for the speedy reply; the corrected formula still leads to the panic.
We (+ @SunHao-0) had a quick look. The issue might be related to the invariants in |
Oh, indeed, I didn't pay attention to the error line. Looks like the first formula is also accepted by the parser. Hmm, yes, I now remember. I added invariant establishing with a mix of needed invariants and convenient invariants, but never bothered to add and prove "formula fixing" (eg for this case remove the clause, for duplicated literals reduce the clause to only contain one of the literals) for the convenient ones. The idea was to at some point go and implement a better "mid-layer" with that + some actual preprocessing stuff, but well, I never got around to it. Dunno where that leaves this issue. Thanks, and sorry. I'd like to improve this, but not sure I will anytime soon. |
b36aacd
The text was updated successfully, but these errors were encountered: