Fix bugs in lazy unrolling with init=False.

Author: mvcisback

aiger/aig.py

@@ -60,7 +60,6 @@ def children(self):
         return (self.left, self.right)
 
 
-
 @attr.frozen
 class Inverter(Node):
     input: Node
@@ -95,7 +94,7 @@ def children(self):
         return ()
 
     def __eq__(self, other) -> bool:
-        return isinstance(other, ConstFalse) 
+        return isinstance(other, ConstFalse)
 
     def __hash__(self) -> int:
         return hash(False)

aiger/lazy.py

@@ -459,9 +459,13 @@ def __call__(self, inputs, latches=None, *, lift=None):
         if not init:
             assert (circ.latches & circ.inputs) == set()
 
-        latches = circ.latch2init if init else project(inputs, circ.inputs)
         if init:
-            inputs = omit(inputs, circ.inputs)
+            latches = circ.latch2init
+        else:
+            try:
+                latches = {n: inputs[f'{n}##time_0'] for n in circ.latches}
+            except KeyError:
+                raise ValueError('not init, but missing latches from inputs.')
 
         outputs = {}
         for time in range(horizon):

tests/test_common.py

@@ -230,6 +230,25 @@ def unroll_key(key):
     assert sum1 == sum2
 
 
+def test_unroll_without_init():
+    circ = aiger.parse('''aag 3 1 1 1 1
+2
+4 6 1
+6
+6 4 2
+i0 x
+o0 x
+l0 y
+''')
+    circ2 = circ.unroll(2, init=False)
+    assert circ2.inputs == {'x##time_0', 'x##time_1', 'y##time_0'}
+    assert circ2.outputs == {'x##time_1', 'x##time_2'}
+    out, _ = circ2({'x##time_0': 1, 'x##time_1': 1, 'y##time_0': 1})
+    assert out['x##time_2'] and out['x##time_1']
+    out, _ = circ2({'x##time_0': 1, 'x##time_1': 1, 'y##time_0': 0})
+    assert not out['x##time_2'] and not out['x##time_1']
+
+
 @given(aigh.Circuits, st.data())
 def test_feedback_then_cut(circ, data):
     def renamer(_):