"bdd.let" does not work with substitutions with overlapping variables

[progirep]

The following code yields a KeyError (using the current PIP dd installation on Python 3.8.10):

from dd.autoref import BDD

bdd = BDD()
bdd.declare('x', 'y', 'z', 'w')
u = bdd.add_expr('x /\ y')
d = dict(x=bdd.add_expr('z \/ w'),y=bdd.add_expr("!z \/ w"))
v = bdd.let(d, u)

I'm obtaining the following stack trace:

Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/autoref.py", line 124, in let
    r = self._bdd.let(d, u.node)
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/bdd.py", line 537, in let
    return self.compose(u, d)
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/bdd.py", line 85, in _wrapper
    return func(bdd, *args, **kwargs)
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/bdd.py", line 560, in compose
    r = _copy_bdd(f, var_sub, self, self, cache)
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/bdd.py", line 1782, in _copy_bdd
    q = _copy_bdd(w, level_map, old_bdd, bdd, cache)
  File "/home/<user>/.local/lib/python3.8/site-packages/dd/bdd.py", line 1786, in _copy_bdd
    jnew = level_map[jold]

[johnyf]

Thank you for reporting this issue. This was a bug that was corrected in dd version 0.5.6, which was released on PyPI on Nov 23, 2020.

https://pypi.org/project/dd/0.5.6/#files

This bug was present in dd == 0.5.5 and dd == 0.5.4 (not in earlier dd releases), and was corrected in commit cb37e47.

Installing dd == 0.5.6 is expected to avoid this issue. dd == 0.5.6 and branches main and dev support Python 3.8.

Upgrading dd

Installing dd == 0.5.6 is possible using pip to download and install dd from PyPI:

pip install -U dd

Installing dd is also possible using pip to download and install dd from the git repository's branch main:

pip install https://github.com/tulip-control/dd/archive/main.tar.gz

or using pip and git to download and install dd from the git repository's branch main (this alternative requires that git be installed):

pip install git+https://github.com/tulip-control/dd

Another option is to clone the repository with git, and then install with pip:

git clone git@github.com:tulip-control/dd
cd dd
# The below command will install the pure Python version of `dd`.
# Information about compiling extension modules can be found at:
# https://github.com/tulip-control/dd/tree/main#installation
pip install --use-feature=in-tree-build .

(The option --use-feature=in-tree-build is for activating pip behavior that will become the default in the future. Not using this option will result in a deprecation warning when using pip == 21.2.4.)

Finding the version of the currently installed dd

The currently installed version of dd can be found from the command line using pip:

pip show dd

or using python:

python -c 'import dd; print(dd.__version__)'

or similarly from within Python:

import dd

print(dd.__version__)

Test code

With dd == 0.5.6 installed, the code reported in the comment above (#81 (comment)) completes successfully, and the assertions below pass.

from dd.autoref import BDD

bdd = BDD()
bdd.declare('x', 'y', 'z', 'w')
u = bdd.add_expr(r'x /\ y')
d = dict(x=bdd.add_expr(r'z \/ w'),y=bdd.add_expr(r'!z \/ w'))
v = bdd.let(d, u)
# addendum to check the result of `let`
v_ = bdd.add_expr(r'(z \/ w) /\ (w \/ ~ z)')  # the expected
    # BDD represented by Python variable `v` is
    # equivalent to the expression `'w'`
assert v == v_  # this test assumes correctness of
    # the method `dd.bdd.BDD.add_expr`
#
# full test, directly of the BDD (at the layer of `dd.autoref`)
assert v.var == 'w', v.var
assert v.low == bdd.false
assert v.high == bdd.true

The prefix r to string literals signifies raw strings, and in this case will be needed in a future Python version (a relevant dd commit is 2020cff, currently on branch dev).

About how the fixed bug arose

The fixed bug was caused by an attempt to avoid code duplication: currently, the method dd.bdd.BDD._vector_compose and the function dd.bdd._copy_bdd, which was previously used before writing _vector_compose, differ essentially in only two lines, together with the computations that prepare for calling these functions.

A single function could be written to be used in place of _vector_compose and _copy_bdd. There are a number of tradeoffs involved, in terms of:

• precomputation before the structural recursion on the given BDD,
• the repetition or not of mappings between variable names and variable levels during the recursion,
• readability,
• number of branching checks during the recursion, and
• number of dict lookups during the recursion.

One motivation for how the current implementation works is that I think typically the number of variables declared in a BDD manager is one or more orders of magnitude smaller than the size of the BDD given to these functions. In those cases, precomputation can avoid repetition of the same work during the recursion. Another possibility would be to always in the BDD manager create and keep BDDs for the individual variables, similarly to CUDD (each such BDD requires a single node, so the additional space required is not an issue).

Also, the current implementation of each function/method could be optimized further, though these optimizations may not all be transferable to a consolidated version of _vector_compose and _copy_bdd.