No exception raised when attempting to extract a CNF from an invalid file

[peitl]

I have a script which is supposed to be able to process both DIMACS and another input format (list of graph6 representations of formulas). The method I use to distinguish between the formats is I first try to load from the file with CNF(from_file='filename'), and I rely on it to throw an exception when the file is not valid DIMACS (which I believe is the intended behavior). Turns out that doesn't always happen. I linked a file from which CNF(from_file='filename') loads without raising an exception and returns a CNF with all empty clauses, as many as there were lines in the file. Confirmed with versions 0.1.6.dev9 and 0.1.7.dev15.

graph6_not_dimacs.txt

Python 3.8.10 (default, Nov 26 2021, 20:14:08) 
[GCC 9.3.0] on linux
Type "help", "copyright", "credits" or "license" for more information.
>>> with open('graph6_not_dimacs.txt') as f:
...     print(f.read())
... 
@
G`hRC_
J`?J?qCiAg?
K`?LBAWUCgI_
K`?LA`geBGQ_
K`?LAQWdAgK_
L`?LBPcUAgR?d?
M`?LQhgdCoK_U?h??
Q`?G?E_AagKgeOdOQoAq?YO@e??
Q`?G?EgWcIIGWOc_JOCq?h_@U??

>>> from pysat.formula import CNF
>>> F = CNF(from_file='graph6_not_dimacs.txt')
>>> F.clauses
[[], [], [], [], [], [], [], [], [], []]
>>> import pysat
>>> pysat.__version__
'0.1.7.dev15'

[alexeyignatiev]

Thanks for reporting.

No, there was no intention to detect errors while parsing. Parsing of formulas is already a bottleneck, and making it more clever would only slow this functionality down. So right now we basically rely on exceptions thrown by Python itself, if any.

I agree that checking the format could (and probably should) be done but this would require some sophisticated refactoring to make it scale better while being clever. I will label it as "enhancement".