Add some functions that are used by EdiSyn

[bcrwlngs]

This adds some functions that are used by EdiSyn (https://gitlab.eecs.umich.edu/M-DES-tools/EdiSyn). There may be a better way to do these computations using dd's existing functionality; I'm open to suggestions.

[coveralls]

Coverage remained the same at 80.721% when pulling 8de116c on blakecraw:edisyn into a05f750 on johnyf:master.

[johnyf]

Thank you for the pull request. In summary, the cofactor method can be used to get the functionality of cofactor_function, and sat_iter for pick_one_minterm. Motivated by this PR, a2dfd2a adds the method dd.cudd.BDD.pick (relevant to #27).

cofactor_function

The cofactor_function method is similar to the cofactor method. The cofactor method takes a dict that maps variables to Boolean values and calls cube to create the BDD of the conjunction of those variables. The conjunction is passed to Cudd_Cofactor. The cofactor_function takes the conjunction as input. Cudd_Cofactor takes only cubes as input, so the range of inputs is the same (in other words, cofactor does not compute generalized cofactors, I believe Cudd_bddConstrain and Cudd_bddRestrict do).

In general

def pick(g):
    return next(bdd.sat_iter(g), None)

bdd.cofactor(f, pick(g))

would have the same effect, because g should be a cube. In general the conversion from g to a dict and back to a cube would be slightly less efficient, but the overhead is negligible compared to BDD operations on BDDs in practical problems.

This double conversion would arise if one works in Python by representing assignments to variables with BDDs, because dd is designed assuming that a dict would be more appropriate (in C dict is not builtin as in Python, so it is less convenient there).

Looking at the code of edisyn, indeed the calls to cofactor_function are preceded by tran_to_cube, which takes a variable assignment represented in an enumerated form in Python, and converts it to a cube. I would recommend instead forming a dict that contains the assignment, and pass that to cofactor directly. cofactor will call cube, and also do error handling.

#12 is relevant for future API changes, which will likely replace the methods cofactor, rename, compose, and evaluate (the latter in dd.bdd) with let.

pick_one_minterm

The functionality of this method is available via the method sat_iter, as follows:

bdd.cube(next(bdd.sat_iter(u, care_bits=bdd.vars), None))

# or equivalently, using `pick` from above

bdd.cube(bdd.pick(u, care_bits=bdd.vars))

This also handles the case u = bdd.false (CUDD fails in that case and returns NULL). It may not be necessary to call bdd.cube if the result is then converted to a dict, because bdd.sat_iter returns an assignment of Boolean values to variables as a dict.

By default care_vars = support(u) in sat_iter (as of dd >= 0.5.0). This is probably sufficient, but I passed bdd.vars above to obtain the same result with pick_one_minterm.
Examples to motivate the above:

from dd.cudd import BDD

b = BDD()
[b.add_var(s) for s in ['x', 'y', 'z']]

u = b.add_expr('x \/ y')

>>> b.sat_iter(u)
<generator at 0x7f53e3444730>

>>> next(b.sat_iter(u, care_bits=b.vars), None)
{'x': False, 'y': True, 'z': False}

>>> next(b.sat_iter(u), None)
{'x': False, 'y': True, 'z': False}

>>> assert None is next(b.sat_iter(b.false), None)

>>> next(b.sat_iter(b.false))
---------------------------------------------------------------------------
StopIteration                             Traceback (most recent call last)
<ipython-input-13-3928dfa0a339> in <module>()
----> 1 next(b.sat_iter(b.false))

Regarding efficiency, picking is by definition enumerative, so the additional conversion should not cause runtime issues.

The function Cudd_bddPickOneMinterm can return r = NULL when it fails. One reason it can fail is f = FALSE (another is passing a subset of support(f), which cannot happen in this case, because all declared variables are passed). Cudd_bddPickOneMinterm calls Cudd_PickOneCube, which is called directly by sat_iter.

Subclassing dd.cudd.BDD

The solution seems to be to use the newly added method dd.cudd.BDD.pick and refactor edisyn based on the comments above.

Another approach along the same lines is to import dd.cudd.BDD in edisyn and create a lightweight subclass that implements the methods cofactor_function and pick_one_minterm using pick and cofactor, and cube if needed, based on the comments above. For example:

from dd import cudd

class BDD(cudd.BDD):

    def cofactor_function(self, f, g):
        return self.cofactor(f, self.pick(g))

    def pick_some_minterm(self, u):
        return self.cube(self.pick(u))  # possibly pass `care_vars`, depending on use case

[bcrwlngs]

Thanks, I've patched EdiSyn more or less as you suggested (using sat_iter), so this is no longer needed.