search

ekmett / ersatz

A monad for interfacing with external SAT solvers
Other
62 stars 15 forks source link

QSAT model parser should ignore comments (e.g., printed by caqe) #91

Closed jwaldmann closed 4 months ago

jwaldmann commented 4 months ago

depqbf output looks like this

$ depqbf --qdo --no-dynamic-nenofex 5-2.cnf 
s cnf 1 97 353
V 1 0
V -2 0
...
V 13 0
V 15 0

and ersatz handles this fine.

caqe output is

$ caqe --qdo 5-2.cnf 
c CommonSolverConfig { ... }
s cnf 1 97 353
V 1 0
V -2 0
...
V -35 0
V -36 0

c Satisfiable

and ersatz does not like it. We should simply ignore comment lines (starting with c) and perhaps empty lines as well (line before c Satisfiable)