dd icon indicating copy to clipboard operation
dd copied to clipboard

Fixes for algebraic cudd

Open CazSaa opened this issue 11 months ago • 2 comments

This pull request includes several changes to the dd/cudd_add.pyx file.

Changes to function definitions and error handling:

  • Changed the return type of Cudd_addLeq from DdNode* to int to reflect its actual return type. (The library did not compile for me without this fix)
  • Replaced the implementation of comparison operators (<, <=, >, >=) with NotImplementedError because the implementation does not work with this return type.

Enhancements to file type support:

  • Added support for the 'dot' file type in ADD.dump.

Improvements to the Function class:

  • Added a value property to the Function class to return the value of a leaf ADD node.

Modifications to _to_dot_recurse function:

  • Updated the label for leaf nodes to display their value instead of 'TRUE' or 'FALSE'.
  • Removed taillabel attributes from edges in the _to_dot_recurse because it is redundant with the edge style.

Remove erroneous shortcut in find_or_add:

While i was playing around with this library I found out that for an ADD i constructed, the structure was different from the one I created using PyCUDD. I traced it down to this erroneous shortcut. I'm guessing you tried to mimic the behaviour of one of the shortcuts that is implemented inside CUDD, but i think there was a mistake.

CazSaa avatar Mar 07 '25 12:03 CazSaa

Thank you for finding these issues, I will review the changes.

johnyf avatar Mar 07 '25 13:03 johnyf

Posting here because I'm unsure where it originated from, but there is an errant reference bug in (it seems) cudd_add.ADD.let. - it can be observed in examples/algebraic_decision_diagrams.py running @CazSaa 's repo. The minimal example I've found is

import dd.cudd_add as _agd

manager = _agd.ADD()
var_names = ['x', 'y', 'z'] # no exception if 'x' is removed even though it doesn't appear in expr
manager.declare(*var_names)
expr = manager.add_expr('y')

map_exists = {'y': 'y', 'z': 'z'} # no exception if either mapping is removed
w = manager.let(map_exists, expr)
AssertionError: Still 2 nodes referenced upon shutdown.
Exception ignored in: 'dd.cudd_add.ADD.__dealloc__'
AssertionError: Still 2 nodes referenced upon shutdown.

I've tried looking for possible causes but my setup is currently not fit to debug cython properly, hopefully it helps at least a little. Guessing it's the source for some other issues, as I've tried running a more complex program and ran into

cuddGarbageCollect: problem in table 70
  dead count != deleted
  This problem is often due to a missing call to Cudd_Ref
  or to an extra call to Cudd_RecursiveDeref.
  See the CUDD Programmer's Guide for additional details.Aborted (core dumped)

zisserj avatar Jul 23 '25 11:07 zisserj