Side effects when using cofactors twice using python bindings

[JasmijnB]

When using the cofactors function on a bdd which is obtained by the cofactors function, the value of this bdd changes.
The expected behavior is that this bdd value should not change.

See the following example:

from oxidd.bdd import BDDManager

def using_cofactors(): 
    m = BDDManager(1_000_000, 1_000_000, 1)
    a = m.new_var()
    b = m.new_var()
    c = a & b

    co_true, _ = c.cofactors()
    print("level before:", co_true.level(), "\tvalid:", co_true.valid())
    _, _ = co_true.cofactors()
    print("level after:", co_true.level(), "\tvalid:", co_true.valid())

using_cofactors()

Which prints:

level before: 1 	valid: False
level after: None 	valid: True

This behavior does not take place when using cofactor_true or cofactor_false instead of cofactors in any of the steps.

I suspect that the second cofactors call changes the value of co_true to the newly obtained true cofactor.

[nhusung]

That’s concerning 😨 Thank you for reporting. I could reproduce the bug, and it seems to affect the Python bindings only. I added the following debug prints in the implementation of BDDFunction.cofactors():

print(f"start: ({self._func._p}, {self._func._i})")
raw_pair = _lib.oxidd_bdd_cofactors(self._func)
print(f"mid: ({self._func._p}, {self._func._i})")

Even with just the following code, I could observe the error:

from oxidd.bdd import BDDManager

m = BDDManager(1_000_000, 1_000_000, 1)
a = m.new_var()
b = m.new_var()
c = a & b

co_true, _ = c.cofactors()
_, _ = co_true.cofactors()

Output (the first component of each tuple is the pointer referencing the manager, the second is the index of the node):

start: (<cdata 'void *' 0x55a6010c3b00>, 3)
mid: (<cdata 'void *' 0x55a6010c3b00>, 3)
start: (<cdata 'void *' 0x55a6010c3b00>, 2)
mid: (<cdata 'void *' 0x55a6010c3b00>, 0)

This change should not happen at all. Note also that the C ABI function oxidd_bdd_cofactors() takes the oxidd_bdd_t (which corresponds to self._func) by value, so it cannot modify it. As expected, the issue does not show when calling the respective functions from C. _lib is the module generated by CFFI, so I suspect the bug to be on the site of CFFI. But before opening an issue there, I’ll need to have a look at the code generated by CFFI (and also my build script).

The bug also affects the Python bindings for BCDDs.