dd
dd copied to clipboard
AssertionError when using let
Hi, first I wanted to thank you for this library. It's great.
I'm facing an issue when using the let function. Here is my code:
from dd.autoref import BDD
bdd = BDD()
formula, = bdd.load('bdd.json')
negations = {k: ~ bdd.var(k) for k in formula.support}
u = bdd.let(negations, formula)
The bdd.json file is
bdd.json.txt. It's been created with the dump function.
The error I'm getting is this one:
Traceback (most recent call last):
File "/home/santi/emydirectory/fixed-point-proof/src/reproduce.py", line 9, in <module>
u = bdd.let(negations, formula)
File "/home/santi/.local/lib/python3.10/site-packages/dd/autoref.py", line 127, in let
r = self._bdd.let(d, u.node)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 596, in let
return self.compose(u, d)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 84, in _wrapper
return func(bdd, *args, **kwargs)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 622, in compose
r = self._vector_compose(f, dvars, cache)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 668, in _vector_compose
p = self._vector_compose(v, level_sub, cache)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 668, in _vector_compose
p = self._vector_compose(v, level_sub, cache)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 668, in _vector_compose
p = self._vector_compose(v, level_sub, cache)
[Previous line repeated 4 more times]
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 669, in _vector_compose
q = self._vector_compose(w, level_sub, cache)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 668, in _vector_compose
p = self._vector_compose(v, level_sub, cache)
File "/home/santi/.local/lib/python3.10/site-packages/dd/bdd.py", line 661, in _vector_compose
assert r > 0, r
AssertionError: -53