ENH: add dd.sylvan.BDD.count()

[johnyf]

Implemented the method BDD.count() in the Sylvan interface.

(Can be merged as one commit, to keep the git graph linear.)

[slivingston]

Excellent work!

Is there a reason not to create a count method on the Function class for Sylvan? The CUDD interface has Function.count, and this is necessary to follow examples in doc.md. E.g.,

>>> import dd.sylvan as _bdd
>>> bdd = _bdd .BDD()
>>> bdd.declare('x')
>>> u = bdd.add_expr(r'x')
>>> u.count()
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
AttributeError: 'dd.sylvan.Function' object has no attribute 'count'

If you agree, I can make send a pull request.

[johnyf]

Thanks for reviewing.

Adding the method dd.sylvan.Function.count() would be good. Alternatively, the documentation could be changed to use BDD.count().

I have mostly used the Python operators ~, &, | on Function instances, the attributes var, level, low, high, negated (in recursion), and the methods __int__(), __str__() (via int(), str() or string formatting), and tend to use BDD methods for other operations.

This relates to the decision of how many ways to have for performing an operation. Using BDD methods for other operations also simplifies remembering which operations are implemented in Function and which not. For example, I have added the methods let(), exist(), forall(), pick() to dd._abc.Operator (the Protocol from which dd.autoref.Function subclasses), but have always used BDD.let(), BDD.exist(), BDD.forall(), BDD.pick(). (Function.pick() is mentioned in a comment in the documentation.) This also reduces duplication of methods.

On the other hand, the number of satisfying assignments can be considered as a property of (the graph rooted at) a Function, likewise to the attribute dag_size. This is in support of implementing a method Function.count().

In dd.sylvan.BDD.count() the parameter nvars (e.g., as in dd.autoref.BDD.count()) was intentionally not added, because nvars seems to not be used. Its effect can be obtained by computing bdd.count(u) * 2**(nvars-len(bdd.support(u))), which seems more explicit. In any case, if nvars is needed it can be added as a parameter.