Wrong results when using parallel compositions

[MatCos]

I came across some unexplainable behavior when using the parallel composition of two AIGER circuits.

Given the following minimal example:

    circ0 = aiger.parse("aag 2 1 1 1 0\n2\n4 2\n4\ni0 i0\nl0 l0\no0 o0")
    circ1 = aiger.parse("aag 2 1 1 1 0\n2\n4 2\n4\ni0 i1\nl0 l0\no0 o1")

of two AIGER circuits that are copies of each other but with disjunct inputs/outputs. Both circuits have one latch that delays the only input to the output by one step. The composed circuit:

   circ0 | circ1

   aag 3 2 1 2 0
   2
   4
   6 4 0
   6
   6
   i0 i0
   i1 i1
   o0 o0
   o1 o1
   l0 l0

consists of only one latch, hence input i0 is ignored and circ0 is not subsumed by the composed result

[MatCos]

The problem seems to be that the latches have identical names. When losing the definition in the symbol table (or renaming the latches), it works as expected.

   circ2 = aiger.parse("aag 2 1 1 1 0\n2\n4 2\n4\ni0 i0\nl0 l0\no0 o0")
   circ3 = aiger.parse("aag 2 1 1 1 0\n2\n4 2\n4\ni0 i1\nl0 l1\no0 o1")
   circ2 | circ3

  aag 4 2 2 2 0
  2
  4
  6 2 0
  8 4 0
  6
  8
  i0 i0
  i1 i1
  o0 o0
  o1 o1
  l0 l0
  l1 l1

While this makes sense from an implementation perspective, I still see a problem with this interpretation.

If the name of a latch is considered when composing systems, it should not be possible to compose circ0 and circ1, because no circuit can exist that is the composition of the two circuits. It might be dangerous to have undefined behavior in this setting.

I'll leave the issue open and let the developer decide whether this is an issue.

[mvcisback]

Thanks for letting me know. I'll try to find to look into resolving.