Skip to content

Conversation

@CazSaa
Copy link

@CazSaa CazSaa commented Mar 7, 2025

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.

@johnyf
Copy link
Member

johnyf commented Mar 7, 2025

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

@johnyf johnyf mentioned this pull request Jun 26, 2025
@zisserj
Copy link

zisserj commented Jul 23, 2025

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)

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants