search

tulip-control / dd

Binary Decision Diagrams (BDDs) in pure Python and Cython wrappers of CUDD, Sylvan, and BuDDy
https://pypi.org/project/dd
Other
181 stars 39 forks source link

NeedsReordering exception #93

Closed dvcopae closed 5 months ago

dvcopae commented 6 months ago

Hello!

I'm encountering an issue when I'm trying to use the following variable ordering to reorder a bdd. I apologize that the exemple is not minimal but I can't pinpoint exactly what part causes the algorithm to break. Calling _bdd.reorder(bdd) instead of _bdd.reorder(bdd, order=custom_order) works fine and doesn't cause any errors.

The stack trace is as follows:

Traceback (most recent call last):
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/sample.py", line 59, in <module>
    _bdd.reorder(bdd, order=custom_order)  # _NeedsReordering()
    ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/.venv/lib/python3.12/site-packages/dd/bdd.py", line 2936, in reorder
    _sort_to_order(bdd, order)
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/.venv/lib/python3.12/site-packages/dd/bdd.py", line 3071, in _sort_to_order
    bdd.swap(i, i + 1, levels)
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/.venv/lib/python3.12/site-packages/dd/bdd.py", line 1780, in swap
    p = self.find_or_add(
        ^^^^^^^^^^^^^^^^^
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/.venv/lib/python3.12/site-packages/dd/bdd.py", line 1483, in find_or_add
    _request_reordering(self)
  File "/Users/ketamon/Documents/Twente/thesis_adtrees/.venv/lib/python3.12/site-packages/dd/bdd.py", line 72, in _request_reordering
    raise _NeedsReordering()
dd.bdd._NeedsReordering

For reference, I'm using Python 3.12.3.

import dd.bdd as _bdd

bdd = _bdd.BDD()
bdd.configure(reordering=True)
bdd.declare(
    "a1", "a2", "a3", "a4", "a5", "a6", "a7", "a8", "a9", "a10", "a11",
    "d2", "d3", "d4", "d5", "d6", "d7", "d8", "d9", "d10", "d11",
)

custom_order = {
    "d2": 0, "d3": 1, "d4": 2, "d5": 3, "d6": 4, "d7": 5, "d8": 6, "d9": 7, "d10": 8, "d11": 9,
    "a1": 10, "a2": 11, "a3": 12, "a4": 13, "a5": 14, "a6": 15, "a7": 16, "a8": 17, "a9": 18, "a10": 19, "a11": 20,
}

expr = "((a2 & !((((d10 & !((((a10 & !((((d5 & !((a6 & a8) & !d9)) & d6) & d4) & !a4)) & ((a7 & !((d7 & d8) & !a5)) & a9)) & a11) & !d3)) & d11) & d2) & !a1)) & a3)"

TREE = bdd.add_expr(expr)

bdd.incref(TREE)

_bdd.reorder(bdd, order=custom_order)  # raises _NeedsReordering()

bdd.decref(TREE)

I can't figure it out if I'm doing something wrong, or this is a bug within the library.

johnyf commented 6 months ago

If reordering to given variable levels, bdd.configure(reordering=False) is needed, so that the variables are shifted to the given levels, without using automated reordering. The following works without errors:

bdd.configure(reordering=False)
_bdd.reorder(bdd, order=custom_order)
assert bdd.vars == custom_order, bdd.vars
bdd.configure(reordering=True)

Methods that may run automated reordering when it is active (with bdd.configure(reordering=True)) are decorated with dd.bdd._try_to_reorder(), which catches the exception _NeedsReordering and then runs automated reordering. The function dd.bdd._sort_to_order() called in this case does not have @_try_to_reorder because levels there are swapped until the given variable levels are obtained.

dvcopae commented 6 months ago

Thanks so much for your quick response. I confirm that changing the reordering parameter to False works as expected.