Source code for pyeda.boolalg.boolfunc

"""
The :mod:`pyeda.boolalg.boolfunc` module implements the fundamentals of
Boolean space, variables and functions.

Data Types:

point
    A dictionary of ``Variable => {0, 1}`` mappings.
    For example, ``{a: 0, b: 1, c: 0, d: 1}``.
    An N-dimensional *point* corresponds to one vertex of an N-dimensional
    *cube*.

untyped point
    An untyped, immutable representation of a *point*,
    represented as ``(frozenset([int]), frozenset([int]))``.
    The integers are Variable uniqids.
    Index zero contains a frozenset of variables mapped to zero,
    and index one contains a frozenset of variables mapped to one.
    This representation is easier to manipulate than the *point*,
    and it is hashable for caching purposes.

term
    A tuple of :math:`N` Boolean functions,
    intended to be used as the input of either an OR or AND function.
    An OR term is called a *maxterm* (product of sums),
    and an AND term is called a *minterm* (sum of products).

Interface Functions:

* :func:`num2point` --- Convert an integer into a point in an N-dimensional
  Boolean space.
* :func:`num2upoint` --- Convert an integer into an untyped point in an
  N-dimensional Boolean space.
* :func:`num2term` --- Convert an integer into a min/max term in an
  N-dimensional Boolean space.

* :func:`point2upoint` --- Convert a point into an untyped point.
* :func:`point2term` --- Convert a point into a min/max term.

* :func:`iter_points` --- Iterate through all points in an N-dimensional
  Boolean space.
* :func:`iter_upoints` --- Iterate through all untyped points in an
  N-dimensional Boolean space.
* :func:`iter_terms` --- Iterate through all min/max terms in an N-dimensional
  Boolean space.

* :func:`vpoint2point` --- Convert a vector point into a point in an
  N-dimensional Boolean space.

Interface Classes:

* :class:`Variable`
* :class:`Function`
"""

import functools
import operator
import threading

from pyeda.util import bit_on, cached_property

VARIABLES = dict()


def var(name, index=None):
    """Return a unique Variable instance.

    .. note::
       Do **NOT** call this function directly.
       Instead, use one of the concrete implementations:

       * :func:`pyeda.boolalg.bdd.bddvar`
       * :func:`pyeda.boolalg.expr.exprvar`,
       * :func:`pyeda.boolalg.table.ttvar`.
    """
    tname = type(name)
    if tname is str:
        names = (name, )
    elif tname is tuple:
        names = name
    else:
        fstr = "expected name to be a str or tuple, got {0.__name__}"
        raise TypeError(fstr.format(tname))

    if not names:
        raise ValueError("expected at least one name")

    for name in names:
        tname = type(name)
        if tname is not str:
            fstr = "expected name to be a str, got {0.__name__}"
            raise TypeError(fstr.format(tname))

    if index is None:
        indices = tuple()
    else:
        tindex = type(index)
        if tindex is int:
            indices = (index, )
        elif tindex is tuple:
            indices = index
        else:
            fstr = "expected index to be an int or tuple, got {0.__name__}"
            raise TypeError(fstr.format(tindex))

    for index in indices:
        tindex = type(index)
        if tindex is not int:
            fstr = "expected index to be an int, got {0.__name__}"
            raise TypeError(fstr.format(tindex))
        if index < 0:
            fstr = "expected index to be >= 0, got {}"
            raise ValueError(fstr.format(index))

    try:
        v = VARIABLES[(names, indices)]
    except KeyError:
        v = Variable(names, indices)
        VARIABLES[(names, indices)] = v
    return v


[docs]def num2point(num, vs): """Convert *num* into a point in an N-dimensional Boolean space. The *vs* argument is a sequence of :math:`N` Boolean variables. There are :math:`2^N` points in the corresponding Boolean space. The dimension number of each variable is its index in the sequence. The *num* argument is an int in range :math:`[0, 2^N)`. For example, consider the 3-dimensional space formed by variables :math:`a`, :math:`b`, :math:`c`. Each vertex corresponds to a 3-dimensional point as summarized by the table:: 6-----------7 ===== ======= ================= /| /| num a b c point / | / | ===== ======= ================= / | / | 0 0 0 0 {a:0, b:0, c:0} 4-----------5 | 1 1 0 0 {a:1, b:0, c:0} | | | | 2 0 1 0 {a:0, b:1, c:0} | | | | 3 1 1 0 {a:1, b:1, c:0} | 2-------|---3 4 0 0 1 {a:0, b:0, c:1} | / | / 5 1 0 1 {a:1, b:0, c:1} c b | / | / 6 0 1 1 {a:0, b:1, c:1} |/ |/ |/ 7 1 1 1 {a:1, b:1, c:1} +-a 0-----------1 ===== ======= ================= .. note:: The ``a b c`` column is the binary representation of *num* written in little-endian order. """ if not isinstance(num, int): fstr = "expected num to be an int, got {0.__name__}" raise TypeError(fstr.format(type(num))) n = len(vs) if not 0 <= num < 2**n: fstr = "expected num to be in range [0, {}), got {}" raise ValueError(fstr.format(2**n, num)) return {v: bit_on(num, i) for i, v in enumerate(vs)}
[docs]def num2upoint(num, vs): """Convert *num* into an untyped point in an N-dimensional Boolean space. The *vs* argument is a sequence of :math:`N` Boolean variables. There are :math:`2^N` points in the corresponding Boolean space. The dimension number of each variable is its index in the sequence. The *num* argument is an int in range :math:`[0, 2^N)`. See :func:`num2point` for a description of how *num* maps onto an N-dimensional point. This function merely converts the output to an immutable (untyped) form. """ return point2upoint(num2point(num, vs))
[docs]def num2term(num, fs, conj=False): """Convert *num* into a min/max term in an N-dimensional Boolean space. The *fs* argument is a sequence of :math:`N` Boolean functions. There are :math:`2^N` points in the corresponding Boolean space. The dimension number of each function is its index in the sequence. The *num* argument is an int in range :math:`[0, 2^N)`. If *conj* is ``False``, return a minterm. Otherwise, return a maxterm. For example, consider the 3-dimensional space formed by functions :math:`f`, :math:`g`, :math:`h`. Each vertex corresponds to a min/max term as summarized by the table:: 6-----------7 ===== ======= ========== ========== /| /| num f g h minterm maxterm / | / | ===== ======= ========== ========== / | / | 0 0 0 0 f' g' h' f g h 4-----------5 | 1 1 0 0 f g' h' f' g h | | | | 2 0 1 0 f' g h' f g' h | | | | 3 1 1 0 f g h' f' g' h | 2-------|---3 4 0 0 1 f' g' h f g h' | / | / 5 1 0 1 f g' h f' g h' h g | / | / 6 0 1 1 f' g h f g' h' |/ |/ |/ 7 1 1 1 f g h f' g' h' +-f 0-----------1 ===== ======= ========= =========== .. note:: The ``f g h`` column is the binary representation of *num* written in little-endian order. """ if not isinstance(num, int): fstr = "expected num to be an int, got {0.__name__}" raise TypeError(fstr.format(type(num))) n = len(fs) if not 0 <= num < 2**n: fstr = "expected num to be in range [0, {}), got {}" raise ValueError(fstr.format(2**n, num)) if conj: return tuple(~f if bit_on(num, i) else f for i, f in enumerate(fs)) else: return tuple(f if bit_on(num, i) else ~f for i, f in enumerate(fs))
[docs]def point2upoint(point): """Convert *point* into an untyped point.""" upoint = [set(), set()] for v, val in point.items(): upoint[val].add(v.uniqid) upoint[0] = frozenset(upoint[0]) upoint[1] = frozenset(upoint[1]) return tuple(upoint)
[docs]def point2term(point, conj=False): """Convert *point* into a min/max term. If *conj* is ``False``, return a minterm. Otherwise, return a maxterm. """ if conj: return tuple(~v if val else v for v, val in point.items()) else: return tuple(v if val else ~v for v, val in point.items())
[docs]def iter_points(vs): """Iterate through all points in an N-dimensional Boolean space. The *vs* argument is a sequence of :math:`N` Boolean variables. """ for num in range(1 << len(vs)): yield num2point(num, vs)
[docs]def iter_upoints(vs): """Iterate through all untyped points in an N-dimensional Boolean space. The *vs* argument is a sequence of :math:`N` Boolean variables. """ for num in range(1 << len(vs)): yield num2upoint(num, vs)
[docs]def iter_terms(fs, conj=False): """Iterate through all min/max terms in an N-dimensional Boolean space. The *fs* argument is a sequence of :math:`N` Boolean functions. If *conj* is ``False``, yield minterms. Otherwise, yield maxterms. """ for num in range(1 << len(fs)): yield num2term(num, fs, conj)
[docs]def vpoint2point(vpoint): """Convert *vpoint* into a point in an N-dimensional Boolean space. The *vpoint* argument is a mapping from multi-dimensional arrays of variables to matching arrays of :math:`{0, 1}`. Elements from the values array will be converted to :math:`{0, 1}` using the `int` builtin function. For example:: >>> from pyeda.boolalg.expr import exprvar >>> a = exprvar('a') >>> b00, b01, b10, b11 = map(exprvar, "b00 b01 b10 b11".split()) >>> vpoint = {a: 0, ((b00, b01), (b10, b11)): ["01", "01"]} >>> point = vpoint2point(vpoint) >>> point[a], point[b00], point[b01], point[b10], point[b11] (0, 0, 1, 0, 1) The vpoint mapping is more concise if ``B`` is an farray:: >>> from pyeda.boolalg.expr import exprvar >>> from pyeda.boolalg.bfarray import exprvars >>> a = exprvar('a') >>> B = exprvars('b', 2, 2) >>> vpoint = {a: 0, B: ["01", "01"]} >>> point = vpoint2point(vpoint) >>> point[a], point[B[0,0]], point[B[0,1]], point[B[1,0]], point[B[1,1]] (0, 0, 1, 0, 1) The shape of the array must match the shape of its values:: >>> from pyeda.boolalg.bfarray import exprvars >>> X = exprvars('x', 2, 2) >>> vpoint = {X: "0101"} >>> point = vpoint2point(vpoint) Traceback (most recent call last): ... ValueError: expected 1:1 mapping from Variable => {0, 1} """ point = dict() for v, val in vpoint.items(): point.update(_flatten(v, val)) return point
def _flatten(v, val): """Recursively flatten vectorized var => {0, 1} mappings.""" if isinstance(v, Variable): yield v, int(val) else: if len(v) != len(val): raise ValueError("expected 1:1 mapping from Variable => {0, 1}") for _var, _val in zip(v, val): yield from _flatten(_var, _val) _UNIQIDS = dict() _COUNT = 1
[docs]class Variable: r""" Base class for a symbolic Boolean variable. A Boolean *variable* is an abstract numerical quantity that may assume any value in the set :math:`B = \{0, 1\}`. .. note:: Do **NOT** instantiate a ``Variable`` directly. Instead, use one of the concrete implementations: :func:`pyeda.boolalg.bdd.bddvar` :func:`pyeda.boolalg.expr.exprvar`, :func:`pyeda.boolalg.table.ttvar`. A variable is defined by one or more *names*, and zero or more *indices*. Multiple names establish hierarchical namespaces, and multiple indices group several related variables. Each variable has a unique, positive integer called the *uniqid*. This integer may be used to identify a variable that is represented by more than one data structure. For example, ``bddvar('a', 0)`` and ``exprvar('a', 0)`` will refer to two different Variable instances, but both will share the same uniqid. All variables are implicitly ordered. If two variable names are identical, compare their indices. Otherwise, do a string comparison of their names. This is only useful where variable order matters, and is not meaningful in any algebraic sense. For example, the following statements are true: * ``a == a`` * ``a < b`` * ``a[0] < a[1]`` * ``a[0][1] < a[0][2]`` """ def __init__(self, names, indices): global _UNIQIDS, _COUNT with threading.Lock(): try: uniqid = _UNIQIDS[(names, indices)] except KeyError: uniqid = _COUNT _COUNT += 1 _UNIQIDS[(names, indices)] = uniqid self.names = names self.indices = indices self.uniqid = uniqid def __repr__(self): return self.__str__() def __str__(self): if self.indices: suffix = "[" + ",".join(str(idx) for idx in self.indices) + "]" return self.qualname + suffix else: return self.qualname
[docs] def __lt__(self, other): if self.names == other.names: return self.indices < other.indices else: return self.names < other.names
@property def name(self): """Return the innermost variable name.""" return self.names[0] @property def qualname(self): """Return the fully qualified name.""" return ".".join(reversed(self.names))
[docs]class Function: """ Abstract base class that defines an interface for a symbolic Boolean function of :math:`N` variables. """ # Operators
[docs] def __invert__(self): """Boolean negation operator +-----------+------------+ | :math:`f` | :math:`f'` | +===========+============+ | 0 | 1 | +-----------+------------+ | 1 | 0 | +-----------+------------+ """ raise NotImplementedError()
[docs] def __or__(self, g): """Boolean disjunction (sum, OR) operator +-----------+-----------+---------------+ | :math:`f` | :math:`g` | :math:`f + g` | +===========+===========+===============+ | 0 | 0 | 0 | +-----------+-----------+---------------+ | 0 | 1 | 1 | +-----------+-----------+---------------+ | 1 | 0 | 1 | +-----------+-----------+---------------+ | 1 | 1 | 1 | +-----------+-----------+---------------+ """ raise NotImplementedError()
def __ror__(self, g): return self.__or__(g)
[docs] def __and__(self, g): r"""Boolean conjunction (product, AND) operator +-----------+-----------+-------------------+ | :math:`f` | :math:`g` | :math:`f \cdot g` | +===========+===========+===================+ | 0 | 0 | 0 | +-----------+-----------+-------------------+ | 0 | 1 | 0 | +-----------+-----------+-------------------+ | 1 | 0 | 0 | +-----------+-----------+-------------------+ | 1 | 1 | 1 | +-----------+-----------+-------------------+ """ raise NotImplementedError()
def __rand__(self, g): return self.__and__(g)
[docs] def __xor__(self, g): r"""Boolean exclusive or (XOR) operator +-----------+-----------+--------------------+ | :math:`f` | :math:`g` | :math:`f \oplus g` | +===========+===========+====================+ | 0 | 0 | 0 | +-----------+-----------+--------------------+ | 0 | 1 | 1 | +-----------+-----------+--------------------+ | 1 | 0 | 1 | +-----------+-----------+--------------------+ | 1 | 1 | 0 | +-----------+-----------+--------------------+ """ raise NotImplementedError()
def __rxor__(self, g): return self.__xor__(g)
[docs] def __add__(self, other): """Concatenation operator The *other* argument may be a Function or an farray. """ from pyeda.boolalg.bfarray import farray if other in {0, 1}: return farray([self] + [self.box(other)]) elif isinstance(other, Function): return farray([self] + [other]) elif isinstance(other, farray): return farray([self] + list(other.flat)) else: raise TypeError("expected Function or farray")
def __radd__(self, other): from pyeda.boolalg.bfarray import farray if other in {0, 1}: return farray([self.box(other)] + [self]) else: raise TypeError("expected Function or farray")
[docs] def __mul__(self, num): """Repetition operator""" from pyeda.boolalg.bfarray import farray if not isinstance(num, int): raise TypeError("expected multiplier to be an int") if num < 0: raise ValueError("expected multiplier to be non-negative") return farray([self] * num)
def __rmul__(self, num): return self.__mul__(num) @property def support(self): r"""Return the support set of a function. Let :math:`f(x_1, x_2, \dots, x_n)` be a Boolean function of :math:`N` variables. The unordered set :math:`\{x_1, x_2, \dots, x_n\}` is called the *support* of the function. """ raise NotImplementedError() @cached_property def usupport(self): """Return the untyped support set of a function.""" return frozenset(v.uniqid for v in self.support) @property def inputs(self): """Return the support set in name/index order.""" raise NotImplementedError() @property def top(self): """Return the first variable in the ordered support set.""" if self.inputs: return self.inputs[0] else: return None @property def degree(self): r"""Return the degree of a function. A function from :math:`B^{N} \Rightarrow B` is called a Boolean function of *degree* :math:`N`. """ return len(self.support) @property def cardinality(self): r"""Return the cardinality of the relation :math:`B^{N} \Rightarrow B`. Always equal to :math:`2^{N}`. """ return 1 << self.degree
[docs] def iter_domain(self): """Iterate through all points in the domain.""" yield from iter_points(self.inputs)
[docs] def iter_image(self): """Iterate through all elements in the image.""" for point in iter_points(self.inputs): yield self.restrict(point)
[docs] def iter_relation(self): """Iterate through all (point, element) pairs in the relation.""" for point in iter_points(self.inputs): yield (point, self.restrict(point))
[docs] def restrict(self, point): r""" Restrict a subset of support variables to :math:`\{0, 1\}`. Returns a new function: :math:`f(x_i, \ldots)` :math:`f \: | \: x_i = b` """ raise NotImplementedError()
[docs] def vrestrict(self, vpoint): """Expand all vectors in *vpoint* before applying ``restrict``.""" return self.restrict(vpoint2point(vpoint))
[docs] def compose(self, mapping): r""" Substitute a subset of support variables with other Boolean functions. Returns a new function: :math:`f(g_i, \ldots)` :math:`f_1 \: | \: x_i = f_2` """ raise NotImplementedError()
[docs] def satisfy_one(self): """ If this function is satisfiable, return a satisfying input point. A tautology *may* return a zero-dimensional point; a contradiction *must* return None. """ raise NotImplementedError()
[docs] def satisfy_all(self): """Iterate through all satisfying input points.""" raise NotImplementedError()
[docs] def satisfy_count(self): """Return the cardinality of the set of all satisfying input points.""" return sum(1 for _ in self.satisfy_all())
[docs] def iter_cofactors(self, vs=None): r"""Iterate through the cofactors of a function over N variables. The *vs* argument is a sequence of :math:`N` Boolean variables. The *cofactor* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i` is: :math:`f_{x_i} = f(x_1, x_2, \dots, 1, \dots, x_n)` The *cofactor* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i'` is: :math:`f_{x_i'} = f(x_1, x_2, \dots, 0, \dots, x_n)` """ vs = self._expect_vars(vs) for point in iter_points(vs): yield self.restrict(point)
[docs] def cofactors(self, vs=None): r"""Return a tuple of the cofactors of a function over N variables. The *vs* argument is a sequence of :math:`N` Boolean variables. The *cofactor* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i` is: :math:`f_{x_i} = f(x_1, x_2, \dots, 1, \dots, x_n)` The *cofactor* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i'` is: :math:`f_{x_i'} = f(x_1, x_2, \dots, 0, \dots, x_n)` """ return tuple(cf for cf in self.iter_cofactors(vs))
[docs] def smoothing(self, vs=None): r"""Return the smoothing of a function over a sequence of N variables. The *vs* argument is a sequence of :math:`N` Boolean variables. The *smoothing* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i` is: :math:`S_{x_i}(f) = f_{x_i} + f_{x_i'}` This is the same as the existential quantification operator: :math:`\exists \{x_1, x_2, \dots\} \: f` """ return functools.reduce(operator.or_, self.iter_cofactors(vs))
[docs] def consensus(self, vs=None): r"""Return the consensus of a function over a sequence of N variables. The *vs* argument is a sequence of :math:`N` Boolean variables. The *consensus* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i` is: :math:`C_{x_i}(f) = f_{x_i} \cdot f_{x_i'}` This is the same as the universal quantification operator: :math:`\forall \{x_1, x_2, \dots\} \: f` """ return functools.reduce(operator.and_, self.iter_cofactors(vs))
[docs] def derivative(self, vs=None): r"""Return the derivative of a function over a sequence of N variables. The *vs* argument is a sequence of :math:`N` Boolean variables. The *derivative* of :math:`f(x_1, x_2, \dots, x_i, \dots, x_n)` with respect to variable :math:`x_i` is: :math:`\frac{\partial}{\partial x_i} f = f_{x_i} \oplus f_{x_i'}` This is also known as the Boolean *difference*. """ return functools.reduce(operator.xor, self.iter_cofactors(vs))
[docs] def is_zero(self): """Return whether this function is zero. .. note:: This method will only look for a particular "zero form", and will **NOT** do a full search for a contradiction. """ raise NotImplementedError()
[docs] def is_one(self): """Return whether this function is one. .. note:: This method will only look for a particular "one form", and will **NOT** do a full search for a tautology. """ raise NotImplementedError()
[docs] @staticmethod def box(obj): """Convert primitive types to a Function.""" raise NotImplementedError()
[docs] def unbox(self): """Return integer 0 or 1 if possible, otherwise return the Function.""" if self.is_zero(): return 0 elif self.is_one(): return 1 else: return self
@staticmethod def _expect_vars(vs=None): """Verify the input type and return a list of Variables.""" if vs is None: return list() elif isinstance(vs, Variable): return [vs] else: checked = list() # Will raise TypeError if vs is not iterable for v in vs: if isinstance(v, Variable): checked.append(v) else: fstr = "expected Variable, got {0.__name__}" raise TypeError(fstr.format(type(v))) return checked