abc claims the aig is empty starting with version 6.1.7

[jbroot]

Step 1: write aig to file with aig.write(file) (pyaiger function)
Step 2: convert ascii aig to binary aig with aigtoaig
Step 3: read binary aig with abc
abc claims the aig is an empty network. These same steps worked in pyaiger version 6.1.6
using Python 3.8

[mvcisback]

Hi @jbroot ,

Sorry about that. I recently rewrote the parser/writer to not use a PEG grammar due to performance issues.

Looking at the commits, I think this was what changed in 6.1.7.

Do you have a small executable example I could use to reproduce the regression?

In particular, I'm curious what aag is output for 6.1.6 vs latest py-aiger version.

[jbroot]

Sure, here is my smallest file that produces the error.
Note: abc and aigtoaig must be installed and symlinked inside /bin/ or /usr/bin/ or the equivalent of your OS. Ubuntu 20.04 with Python 3.8 was used for this error.

xorAigs.txt

[jbroot]

Exact abc error:

ABC command line: "read /tmp/a06d4685-a7f3-478c-be1e-6032cbabac03bin.aig; show".
The number of objects does not match.
Reading AIG from file has failed.
Error: Empty network.

Here are the contents of the /tmp/...aig file:

aig 10 2 0 1 7
19

i0 a
i1 b
o0 out

[mvcisback]

Thanks!

I will look into reproducing and extracting a regression test later today.

[mvcisback]

So I've confirmed that this occurs. No need to get abc involved. The problem seems to be with the following aag:

aag 9 2 0 1 6
2
4
17
6 4 2
8 7 4
10 5 2
12 10 9
14 7 4
16 15 13
i0 a
i1 b
o0 out

aigtoaig succeeds into going from aag to aig, but when converting back it declares

*** [aigtoaig] line 2: invalid maximal variable index

I don't readily see the problem, but I'll look into it more later today.

[mvcisback]

I wrote out the corresponding circuit by hand it seems fine to me.

One thing I noticed is that aigtoaig outputs a weird file.

Namely, it has a header:

aig 20 2 0 1 6

compared to the input header

aag 9 2 0 1 6

AFAIK aigtoaig checks the AIG is well formed when taking it in so I think this is a bug with aigtoaig.

[mvcisback]

I will report this to Armin Biere.

@jbroot if you can confirm that this is a correct AAG file, please let me know.

[jbroot]

I haven't investigated aags much. After surveying http://fmv.jku.at/aiger/FORMAT.aiger I found the following: The aag header has format "aag M I L O A" where M is the maximal variable index, I=inputs, L=latches, O=outputs, and A=ands. If all variables and all AND gates are used, then M = I + L + A. This likely implies that M <= I + L + A The aig header has "aig M I L O A" format following aag syntax. However, it says that all literals must be defined so M must be M = I + L + A. In the aig and aag headers you gave, M > I + L + A so the syntax is invalid. Running xorComplex in version 6.1.6 gives an aag of: aag 9 2 0 1 7 2 4 19 6 2 4 8 2 7 10 2 4 12 2 11 14 3 4 16 13 14 18 9 17 i0 b i1 a o0 out and an aig of: aig 5 2 0 1 3 10 i0 a i1 b o0 out c In both cases, M = I + L + A which satisfies M <= I + L + A for aag and M = I + L + A for aig.

…

On Mon, Feb 8, 2021 at 2:33 PM Marcell Vazquez-Chanlatte < ***@***.***> wrote: I will report this to Armin Biere. @jbroot <https://github.com/jbroot> if you can confirm that this is a correct AAG file, please let me know. — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub <#121 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AFNLHAAE4DIUL56FE7LPQULS6BKBZANCNFSM4W6AATGQ> .

[jbroot]

So I've confirmed that this occurs. No need to get abc involved. The problem seems to be with the following aag:

> aag 9 2 0 1 6
> 2
> 4
> 17
> 6 4 2
> 8 7 4
> 10 5 2
> 12 10 9
> 14 7 4
> 16 15 13
> i0 a
> i1 b
> o0 out

I changed the maximum variable index from 9 to 8 since all ANDs and inputs are used and 8 = I+L+A. aigtoaig and ABC accepted this change and would not allow the prior. The xorComplex produced in 6.1.6 had header 9 2 0 1 7. All AND gates and inputs were used and 9 = 2 + 0 + 7.

[mvcisback]

@jbroot I think you may have flipped >= and <=.

I believe the spec is supposed to be M >= I + L + A with equality only being a restriction on the binary format. M <= I + L + A wouldn't make sense since then you couldn't handle unused inputs.

This constraint is supposed to be checked at runtime in py-aiger.

The thing that I'm worried about is that aigtoaig is generating:

aig 20 2 0 1 6

Thus it is violating this equality constraint. In implementing the new parser/writer, I added infrastructure to soon support the binary format. What I'm thinking might be happening is that there is a weird code path being triggered since the aag input almost matches what needs to happen in the aig output.

[mvcisback]

So the 20 was my fault when messing with aigtoaig, but I think this is indeed a bug.

This aag doesn't work

aag 9 2 0 1 6
2
4
17
6 4 2
8 7 4
10 5 2
12 10 9
14 7 4
16 15 13
i0 a
i1 b
o0 out

But this one does

aag 9 2 0 1 6
2
4
17
6 2 4 <--------------------- This line changed. Flipped 4 and 2.
8 7 4
10 5 2
12 10 9
14 7 4
16 15 13
i0 a
i1 b
o0 out

I think there's an optimization to avoid recomputing the header if the body corresponds with the body for an aig.

[mvcisback]

regarding py-aiger, I think the simplest fix is to force the equality constraint. Will apply patch soon.

[mvcisback]

@jbroot

The latest version of py-aiger should have a tight literal count.

If this works for you please close the issue.

Also, if you're using py-aiger in any academic work, please use the citation at the bottom of the README :)

[mvcisback]

Armin Biere responded and added it on the TODO for AIGER :)

Closing.