dd icon indicating copy to clipboard operation
dd copied to clipboard

AssertionError when using let

Open sdandois opened this issue 3 years ago • 0 comments

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

sdandois avatar Apr 21 '22 16:04 sdandois