Skip to content

Commit 09e316a

Browse files
mvcisbackMarissa Ramirez de Chanlatte
authored andcommitted
Fix parsing of degenerate AIGs.
1 parent 177af63 commit 09e316a

File tree

2 files changed

+20
-6
lines changed

2 files changed

+20
-6
lines changed

aiger/parser.py

Lines changed: 4 additions & 6 deletions
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,6 @@ def parse_output(state, line) -> bool:
130130
match = IO_PATTERN.match(line)
131131
if match is None or state.remaining_outputs <= 0:
132132
return False
133-
134133
lit = int(line)
135134
state.outputs.add(lit)
136135
if lit & 1:
@@ -237,12 +236,12 @@ def parse(lines, to_aig: bool = True):
237236

238237
for line in lines:
239238
while not parser(state, line):
240-
parser = next(parsers)
239+
parser = next(parsers, None)
241240

242241
if parser is None:
243242
raise ValueError(NOT_DONE_PARSING_ERROR.format(state))
244243

245-
if parser not in (parse_comment, parse_symbol):
244+
if parser not in (parse_header, parse_output, parse_comment, parse_symbol):
246245
raise ValueError(DONE_PARSING_ERROR.format(state))
247246

248247
assert state.header.num_ands == 0
@@ -257,11 +256,10 @@ def parse(lines, to_aig: bool = True):
257256

258257
# Create expression DAG.
259258
latch_ids = {latch.id: name for name, latch in latches.items()}
260-
lit2expr = {}
261-
259+
lit2expr = {0: A.aig.ConstFalse()}
262260
for lit in toposort_flatten(state.nodes):
263261
if lit == 0:
264-
lit2expr[lit] = A.aig.ConstFalse()
262+
continue
265263
elif lit in state.inputs:
266264
lit2expr[lit] = A.aig.Input(inputs.inv[lit])
267265
elif lit in latch_ids:

tests/test_parser.py

Lines changed: 16 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -73,3 +73,19 @@ def test_smoke2(data):
7373

7474
def test_mutex_example_smoke():
7575
aigp.load('tests/mutex_converted.aag')
76+
77+
78+
def test_degenerate_smoke():
79+
import aiger as A
80+
expr = A.BoolExpr(A.parse("""aag 0 0 0 1 0
81+
0
82+
"""))
83+
assert expr({}) is False
84+
expr = A.BoolExpr(A.parse("""aag 0 0 0 1 0
85+
1
86+
"""))
87+
assert expr({}) is True
88+
circ = A.parse("""aag 0 0 0 0 0
89+
""")
90+
assert len(circ.node_map) == 0
91+
assert circ.inputs == circ.outputs == circ.latches == set()

0 commit comments

Comments
 (0)