Fixes for algebraic cudd
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_addLeqfromDdNode*tointto reflect its actual return type. (The library did not compile for me without this fix) - Replaced the implementation of comparison operators (
<,<=,>,>=) withNotImplementedErrorbecause 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
valueproperty to theFunctionclass 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
taillabelattributes from edges in the_to_dot_recursebecause 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.
Thank you for finding these issues, I will review the changes.
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)