Request: docs for developers

[sschnug]

While the official documentation works good for explaining the basic usage of pyeda, i'm having problems to understand the core-concepts/core-design, needed to expand it.

Simple example: I wanted to add my own cardinality-expression (use-case: replace exponentially-growing OneHot0-expression for many variables). A prototype-like approach, mimicking OneHot0() looks like that (maybe buggy; theory and code based on Sinz: Towards an Optimal CNF Encoding of Boolean Cardinality Constraints ; maybe a more elegant description is possible using pyeda's bitvector-capabilities):

def AtMostN(*xs, k=1, auxvarname='ohc'):
    """
    Return an expression that means
    "at most k input functions are true".
    Returns cnf
    """
    xs = [Expression.box(x).node for x in xs]
    n = len(xs)
    terms = list()
    aux_vars = exprvars(auxvarname, (n-1)*k)

    def s(i,j,k):
        return aux_vars[i*k+j]

    # case: i=1
    terms.append(exprnode.or_(exprnode.not_(xs[0]), s(0,0,k)))
    for i in range(1,k):
        terms.append(exprnode.not_(s(0,i,k)))

    # general case
    for i in range(1,n-1):
        terms.append(exprnode.or_(exprnode.not_(xs[i]),s(i,0,k)))
        terms.append(exprnode.or_(exprnode.not_(s(i-1,0,k), s(i,0,k))))
        for u in range(1,k):
            terms.append(exprnode.or_(exprnode.not_(xs[i]), exprnode.not_(s(i-1,u-1,k)), s(i,u,k)))
            terms.append(exprnode.or_(exprnode.not_(s(i-1,u,k)), s(i,u,k)))
        terms.append(exprnode.or_(exprnode.not_(xs[i]), exprnode.not_(s(i-1,k-1,k))))

    terms.append(exprnode.or_(exprnode.not_(xs[i], exprnode.not_(s(n-2,k-1,k)))))

    y = exprnode.and_(*terms)
    return _expr(y)

This won't work because the auxiliary-vars introduced are not of type ExprNode. Sadly, the documentation doesn't give away anything about this internal stuff (no hits during search for "exprnode").

The next best thing would be to learn from _tseitin(), where auxiliary variables are introduced too, while generating some expression, but it's hard to understand (at least for me). It seems to touch the C-part of the library.

Any plans on extending the documentation with some core-design comments which might help people to add new features (even if these features will live outside of pyeda; i don't know, if these cardinality-constraints, which are very popular in discrete-optimization are useful in circuit-design)?

[cjdrake]

Can you please create a pull request for this? We can probably work on it a bit to get it into shape.

As for the developer docs, the C API is relatively recent, and I just haven't put in the time yet. The exprnode module is the Python module that wraps the boolexpr C API. Every Expression object has an attribute called node that is an ExprNode instance (from C). So I think all you need to do is convert your array of Expression objects to an array of ExprNode objects by getting auxvar.node.

[sschnug]

Added pull request, which needs some debugging/work. See #128.

[cjdrake]

I have this on the boolexpr TODO list: https://github.com/cjdrake/boolexpr/issues/23

Closing it here, as it is now obsolete.