Closed progirep closed 3 years ago
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 cb37e477da07c8059a0d1830c605c2d9cf510ec5.
Installing dd == 0.5.6
is expected to avoid this issue. dd == 0.5.6
and branches main
and dev
support Python 3.8.
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
.)
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__)
With dd == 0.5.6
installed, the code reported in the comment above (https://github.com/tulip-control/dd/issues/81#issue-974021581) 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 2020cff281d7bc0e819559b798f5bcfbf8469b34, currently on branch dev
).
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:
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
.
The following code yields a KeyError (using the current PIP dd installation on Python 3.8.10):
I'm obtaining the following stack trace: