Understanding difference in count()

[kopeckyf]

Hello :wave:

I noticed there is a difference in the count() functions between the modules autoref and cudd. With autoref, the following code works fine (output is "7"):

from dd.autoref import BDD
bdd = BDD()
bdd.declare('x', 'y', 'z')
u = bdd.add_expr('x | ~y | ~z')
print(bdd.count(u))

But with from dd.cudd import BDD in the first line, the same code returns the error TypeError: count() takes exactly 2 positional arguments (1 given).

With my limited understanding, I believe I may be missing an assert statement somewhere. Could you explain the difference in the behaviour of count(), or would it be possible to patch the function in the cudd module so it works like the one in autoref?

(Edit: running dd Version 0.5.5 and cudd 3.0.0)

[johnyf]

The second argument of the method count is the number of variables that the BDD is assumed to depend on. The method dd.autoref.BDD.count does take a second argument, nvars, which is optional. The default value of the argument nvars is the number of variables in the support of the BDD, i.e., len(bdd.support(u)).

A call to the method dd.autoref.BDD.count that is equivalent to a call to the method dd.cudd.BDD.count is

nvars = len(bdd.support(u))
n = bdd.count(u, nvars=nvars)

A change to the method dd.cudd.BDD.count that would make it equivalent to the method dd.autoref.BDD.count is to make the second argument, nvars, optional, and use as default value of the argument nvars the number of variables in the support of the BDD, i.e.,

    def count(self, Function u, nvars=None):
        """Return number of models of node `u`.

        @param nvars: regard `u` as an operator that
            depends on `nvars` many variables.
        """
        assert u.manager == self.manager
        n = len(self.support(u))
        if nvars is None:
            nvars = n
        assert nvars >= n, (nvars, n)
        r = Cudd_CountMinterm(self.manager, u.node, int(nvars))
        assert r != CUDD_OUT_OF_MEM
        assert r != float('inf'), 'overflow of integer  type double'
        return r

The current implementation emphasizes the second argument.

The method dd.autoref.BDD.count is implemented by the method dd.bdd.BDD.count.

For reference, the count methods discussed above are:

https://github.com/tulip-control/dd/blob/890d191529bf302cdc3bf2afbad0395cf92054c0/dd/cudd.pyx#L857-L869

https://github.com/tulip-control/dd/blob/890d191529bf302cdc3bf2afbad0395cf92054c0/dd/autoref.py#L153-L155

https://github.com/tulip-control/dd/blob/890d191529bf302cdc3bf2afbad0395cf92054c0/dd/bdd.py#L1047-L1100

Please note that the code as of 890d191529bf302cdc3bf2afbad0395cf92054c0 is ahead of the latest release 0.5.5.

[johnyf]

Adressed in 2cb2093e035d65aad799b5162f42d75495dbd2cc, which makes optional the argument nvars in the methods dd.cudd.BDD.count and dd.cudd_zdd.ZDD.count, with default value len(self.support(u)).

[kopeckyf]

Many thanks!