Error parsing .aag file

[arw12625]

Hello.

I ran into an issue when trying to parse aiger files.
Here is a simple example .aag file.

aag 0 0 0 2 0
0
0

which when loaded produces the following error:

>>> aiger.load("bug.aag")
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/awintenb/projects/py-aiger/aiger/parser.py", line 285, in load
    return parse(''.join(f.readlines()), to_aig=to_aig)
  File "/home/awintenb/projects/py-aiger/aiger/parser.py", line 249, in parse
    assert state.remaining_outputs == 0
AssertionError

This error was produced using version 6.1.24.
The same file is correctly loaded in version 6.1.2 producing the output

>>> aiger.load("bug.aag")
aag 0 0 0 2 0
0
0
o0 o0
o1 o1

It appears the issue is that parser.py uses a SortedSet to store the circuits outputs.
When the same value is assigned to multiple outputs (as in the above example), only one is added to the output set.

[mvcisback]

thank you for letting me know.

Indeed there was a recent change to the parser to address another bug :)

I will look into this

[mvcisback]

Hi, I've been able to reproduce the problem.

Indeed, the problem is that the SortedSet doesn't could the same output twice! I will look into a solution.

The easiest solution is to explicitly record the number of outputs processed. I will look into a Bag (Counter) based approach though.

[mvcisback]

Should be fixed by c9faa1e

Changed to SortedList :)

It's published as 6.1.25

[mvcisback]

also, if yo don't mind sharing. @arw12625 what is your use case for py-aiger. I only really find out people use it when I accidentally introduce bugs 😅

[arw12625]

Haha, thanks for the prompt fix. I am experimenting using a QBF solver (Quabs) for designing controllers for some security problems. The solver can output a certificate of satisfaction as an Aiger file. I was using py-aiger to extract the solution from the certificate.