🐛 Fix reading sequential AIGER files produced by ABC

[marcelwa]

Part of a three-PR chain, please review in this order:
#700 (this PR) → #701 (register initialization) → #699 (sequential write_aiger).
This one is the base and stands on its own.

Description

A sequential network written by ABC cannot currently be read back correctly. Three
separate defects in the AIGER latch and output handling.

1. Omitted latch reset values are read as undefined

Both the binary and the ASCII reader default to NONDETERMINISTIC when a latch line
carries no reset field. The format specifies the opposite — AIGER's FORMAT document
states "Latches are always assumed to be initialized to zero", and the reset field
added in 1.9 is optional, so its absence means 0.

ABC relies on this and omits the field for zero-initialized latches, so every
zero-initialized register comes back undefined. This affects even the simplest
sequential round trip.

2. The ASCII reader compares the wrong token

if ( tokens[2u] == "0" )      { ... ZERO; }
else if ( tokens[1u] == "1" ) { ... ONE;  }   // tokens[1u] is the next-state literal

An explicit reset of 1 is therefore never recognized, and a latch whose next-state
literal happens to be 1 is wrongly reported as one-initialized.

3. Bad state properties are dropped

A writer emitting the AIGER 1.9 extended header moves the primary outputs into the
bad-state section. ABC does this for any design with a non-zero latch initialization —
from ioWriteAiger.c:

fExtended = Abc_NtkConstrNum(pNtk);
Abc_NtkForEachLatch( pNtk, pObj, i )
    if ( !Abc_LatchIsInit0(pObj) ) { fExtended = 1; break; }

on_bad_state is not overridden, so those outputs disappear and the network comes back
with none at all. They are now kept as primary outputs — which is what they were —
together with their names from the symbol table.

Drive-by

The aiger_reader destructor advances the output index only for outputs that carry a
name, so with a sparse symbol table every name after the first unnamed output lands on
the wrong output.

Verification

End to end against ABC, with a network carrying three registers initialized to 0, 1,
and undefined, put through resyn2:

before:  read ok=1  pis=3 pos=0 regs=3 gates=5  init0=255 init1=1   <- output lost, init corrupted
after:   read ok=1  pis=3 pos=1 regs=3 gates=5  init0=0   init1=1   <- intact

Five new test cases in test/io/aiger_reader.cpp cover omitted, explicit 0/1, and
undefined resets, the extended header with a bad state, and the sparse symbol table.

Notes

• The reset-value fixes touch the vendored copy of lorina in lib/lorina. Happy to open
  the equivalent change against hriener/lorina as well — let me know if you would
  prefer to take it that way round.
• AIGER constraints remain ignored. They are assumptions rather than outputs, so
  mapping them onto primary outputs would change the meaning of the network.

---

Context: this came out of building a Python-side ABC bridge in
aigverse, where sequential designs survived the
trip to ABC but not back. Companion to #699.

🤖 Generated with Claude Code

https://claude.ai/code/session_01GbUqcnZayPooFgekEXVSjz

[codecov]

Codecov Report

❌ Patch coverage is 71.42857% with 2 lines in your changes missing coverage. Please review.
✅ Project coverage is 84.06%. Comparing base (25beb0e) to head (1d810df).

Files with missing lines	Patch %	Lines
include/mockturtle/io/aiger_reader.hpp	71.42%	2 Missing ⚠️

Additional details and impacted files

@@            Coverage Diff             @@
##           master     #700      +/-   ##
==========================================
- Coverage   84.06%   84.06%   -0.01%     
==========================================
  Files         190      190              
  Lines       29468    29474       +6     
==========================================
+ Hits        24773    24777       +4     
- Misses       4695     4697       +2     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.