Description
Hi, I am using py-aiger to perform some AIG manipulation.
In particular, I am trying to convert AIG to PySMT formulas.
I have found an example of AIG waking in
Line 41 in f501715
I have tried to adapt this to my scenario, but I have noticed this gets very slow on medium-big instances.
And I mean very slow, like hours instead of seconds.
E.g. https://github.com/yogevshalmon/allsat-circuits/blob/b57c2d6cba244460008dc6400beef2604a720c24/benchmarks/random_aig/large_cir_or/bench1/bench1.aag
It seems to me that the bottleneck is somewhere in aiger.common.dfs function, likely operations on sets of nodes.
I suppose that this can be due to the computation of hash for nodes (generated by @attr.frozen), which traverses the whole subgraph each time, for each node.
I attach code to replicate the issue.
import aiger
import funcy as fn
def gates(circ):
gg = []
count = 0
class NodeAlg:
def __init__(self, lit: int):
self.lit = lit
@fn.memoize
def __and__(self, other):
nonlocal count
nonlocal gg
count += 1
new = NodeAlg(count << 1)
right, left = sorted([self.lit, other.lit])
gg.append((new.lit, left, right))
return new
@fn.memoize
def __invert__(self):
return NodeAlg(self.lit ^ 1)
def lift(obj) -> NodeAlg:
if isinstance(obj, bool):
return NodeAlg(int(obj))
elif isinstance(obj, NodeAlg):
return obj
raise NotImplementedError
start = 1
inputs = {k: NodeAlg(i << 1) for i, k in enumerate(sorted(circ.inputs), start)}
count += len(inputs)
omap, _ = circ(inputs=inputs, lift=lift)
return gg
def main():
circ = aiger.to_aig("bench1.aag")
gg = gates(circ)
print(len(gg))
if __name__ == '__main__':
main()