Panic at CreuSAT/src/parser.rs:130:14 on simple formula

[wintered]

b36aacd

$./CreuSAT --file f.cnf                                                            
c Reading file 'f.cnf'                                                             
c Parsed formula with 1 clauses and 1 literals                                     
thread 'main' panicked at CreuSAT/src/parser.rs:130:14:                            
Sarek should really make the parser non-binary                                     
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace   
$minisat f.cnf|tail -n 1                                                           
SATISFIABLE                                                                        
$cat f.cnf                                                                         
cnf 1 1                                                                            
-1 1 0                                                                            

[sarsko]

Hi, thank you.

This does not look like a valid cnf formula to me — there is no p line. I believe it should work if cnf 1 1 is substituted with p cnf 1 1

[sarsko]

(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.)

[wintered]

Thanks @sarsko for the speedy reply; the corrected formula still leads to the panic.

$CreuSAT --file f.cnf 
c Reading file 'f.cnf'
c Parsed formula with 1 clauses and 1 literals
thread 'main' panicked at CreuSAT/src/parser.rs:130:14:
Sarek should really make the parser non-binary
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
$cat f.cnf 
p cnf 1 1
-1 1 0
$

We (+ @SunHao-0) had a quick look. The issue might be related to the invariants in src/clause.rs. I.e., src/clause.rs:no_duplicates returns false for this and other formulas where the positive and negative literals of the same variable share a clause.

[sarsko]

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.

[wintered]

@sarsko I'll close this now. Feel free to reopen, should it become relevant.