Python API Reference

BoolExpr is an open source library for symbolic Boolean Algebra.

Data Types:

abstract syntax tree

A nested tuple of entries that represents an expression. Unlike a BoolExpr object, an ast object is serializable.

It is defined recursively:

ast := (BoolExpr.Kind.zero, )
     | (BoolExpr.Kind.one, )
     | (BoolExpr.Kind.log, )
     | (BoolExpr.Kind.comp, ctx, name)
     | (BoolExpr.Kind.var, ctx, name)
     | (BoolExpr.Kind.nor, ast, ...)
     | (BoolExpr.Kind.or_, ast, ...)
     | (BoolExpr.Kind.nand, ast, ...)
     | (BoolExpr.Kind.and_, ast, ...)
     | (BoolExpr.Kind.xnor, ast, ...)
     | (BoolExpr.Kind.xor, ast, ...)
     | (BoolExpr.Kind.neq, ast, ...)
     | (BoolExpr.Kind.eq, ast, ...)
     | (BoolExpr.Kind.nimpl, ast, ast)
     | (BoolExpr.Kind.impl, ast, ast)
     | (BoolExpr.Kind.nite, ast, ast, ast)
     | (BoolExpr.Kind.ite, ast, ast, ast)

ctx := int

name := str

The ctx int is a pointer to a C++ Context object. It must be re-cast to void * before being used.

point

A dictionary of {Variable : Constant} mappings. For example, {a: False, b: True, c: 0, d: 'X'}.

var2bx

A dictionary of {Variable : BoolExpr} mappings. For example, {a: False, b: ~p | q}.

Symbolic Variable Context

class boolexpr.Context

A context for Boolean variables

get_var(name)

Return a Variable with a given name.

get_vars(name, *dims)

Return a multi-dimensional array of variables.

The name argument is a str.

The variadic dims input is a sequence of dimension specs. A dimension spec is a two-tuple: (start index, stop index). If a dimension is given as a single int, it will be converted to (0, stop).

The dimension starts at index start, and increments by one up to, but not including, stop. This follows the Python slice convention.

Boolean Expression Class Hierarchy

Note

For the sake of space, this diagram omits the Nor, Nand, Xnor, Unequal, NotImplies, and NotIfThenElse classes. They are derived from Operator.

Base Class

class boolexpr.BoolExpr(cdata)

Wrap boolexpr::BoolExpr class

class Kind

BoolExpr Kind Codes

BoolExpr.to_ast()

Convert to an abstract syntax tree (AST).

classmethod BoolExpr.from_ast(ast)

Convert an abstract syntax tree (AST) to a BoolExpr.

BoolExpr.to_dot()

Convert to DOT language representation.

BoolExpr.__invert__()

Boolean negation operator

\(f\)	\(f'\)
0	1
1	0

BoolExpr.__or__(other)

Boolean disjunction (sum, OR) operator

\(f\)	\(g\)	\(f + g\)
0	0	0
0	1	1
1	0	1
1	1	1

BoolExpr.__and__(other)

Boolean conjunction (product, AND) operator

\(f\)	\(g\)	\(f \cdot g\)
0	0	0
0	1	0
1	0	0
1	1	1

BoolExpr.__xor__(other)

Boolean exclusive or (XOR) operator

\(f\)	\(g\)	\(f \oplus g\)
0	0	0
0	1	1
1	0	1
1	1	0

BoolExpr.kind

Return the Kind code.

The expression “kind” is one byte of information. See include/boolexpr/boolexpr.h for the full table of kinds codes. For convenience, this value is wrapped by a Python Enum.

BoolExpr.depth()

Return the depth of the expression.

1. An Atom has zero depth.
2. An Operator has depth equal to the maximum depth of its arguments plus one.

BoolExpr.size()

Return the size of the expression.

1. An Atom has size one.
2. An Operator has size equal to the sum of its arguments’ sizes plus one.

BoolExpr.is_cnf()

Return True if the expression is in conjunctive normal form (CNF).

A CNF is defined as a conjunction of clauses, where a clause is defined as either a Literal, or a disjunction of literals.

Boolean True (And identity) is also considered to be a CNF.

BoolExpr.is_dnf()

Return True if the expression is in disjunctive normal form (DNF).

A DNF is defined as a disjunction of clauses, where a clause is defined as either a Literal, or a disjunction of literals.

Boolean False (Or identity) is also considered to be a DNF.

BoolExpr.simplify()

Return a simplified expression.

Simplification uses Boolean algebra identities to reduce the size of the expression.

BoolExpr.to_binop()

Return an expression that uses only binary operators.

BoolExpr.to_latop()

Convert all operators to Or / And (lattice operator) form.

BoolExpr.to_posop()

Return an expression with NOT bubbles pushed down through dual ops.

Specifically, perform the following transformations:

\[ \begin{align}\begin{aligned}\overline{a + b + \ldots} &\iff \overline{a\vphantom{b}} \cdot \overline{b} \cdot \ldots\\\overline{a \cdot b \cdot \ldots} &\iff \overline{a\vphantom{b}} + \overline{b} + \ldots\\\overline{a \oplus b \oplus \ldots} &\iff \overline{a} \oplus b \oplus \ldots\\\overline{eq(a, b, \ldots)} &\iff eq(\overline{a}, b, \ldots)\\\overline{p \implies q} &\iff p \cdot \overline{q}\\\overline{ite(s, d1, d0)} &\iff ite(s, \overline{d1}, \overline{d0})\end{aligned}\end{align} \]

BoolExpr.tseytin(ctx, auxvarname='a')

Return the Tseytin transformation.

The ctx parameter is a Context object that will be used to store auxiliary variables.

The auxvarname parameter is the prefix of auxiliary variable names. The suffix will be in the form _0, _1, etc.

BoolExpr.compose(var2bx)

Substitute a subset of support variables with other Boolean expressions.

Returns a new expression: \(f(g_i, \ldots)\)

\(f_1 \: | \: x_i = f_2\)

BoolExpr.restrict(point)

Restrict a subset of support variables to \(\{0, 1\}\).

Returns a new function: \(f(x_i, \ldots)\)

\(f \: | \: x_i = b\)

BoolExpr.sat()

Return a tuple (sat, point).

The sat value is True if the expression is satisfiable. If the expression is not satisfiable, the point will be None. Otherwise, it will return a satisfying input point.

BoolExpr.iter_sat()

Iterate through all satisfying input points.

BoolExpr.to_cnf()

Convert the expression to conjunctive normal form (CNF).

BoolExpr.to_dnf()

Convert the expression to disjunctive normal form (DNF).

BoolExpr.to_nnf()

Convert the expression to negation normal form (NNF).

Negation formal form is defined as:

• Only Or or And operators
• All NOT bubbles are pushed down to the literals
• Simple

BoolExpr.equiv(other)

Return True if the two expressions are formally equivalent.

Note

While in practice this check can be quite fast, SAT is an NP-complete problem, so some inputs will require exponential runtime.

BoolExpr.support()

Return the support set of the expression.

BoolExpr.degree()

Return the degree of a function.

A function from \(B^{N} \Rightarrow B\) is called a Boolean function of degree \(N\).

BoolExpr.expand(xs)

Return the Shannon expansion with respect to a sequence of variables.

BoolExpr.smoothing(xs)

Return the smoothing over a sequence of N variables.

The xs argument is a sequence of \(N\) Boolean variables.

The smoothing of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(S_{x_i}(f) = f_{x_i} + f_{x_i'}\)

This is the same as the existential quantification operator: \(\exists \{x_1, x_2, \dots\} \: f\)

BoolExpr.consensus(xs)

Return the consensus over a sequence of N variables.

The xs argument is a sequence of \(N\) Boolean variables.

The consensus of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(C_{x_i}(f) = f_{x_i} \cdot f_{x_i'}\)

This is the same as the universal quantification operator: \(\forall \{x_1, x_2, \dots\} \: f\)

BoolExpr.derivative(xs)

Return the derivative over a sequence of N variables.

The xs argument is a sequence of \(N\) Boolean variables.

The derivative of \(f(x_1, x_2, \dots, x_i, \dots, x_n)\) with respect to variable \(x_i\) is: \(\frac{\partial}{\partial x_i} f = f_{x_i} \oplus f_{x_i'}\)

This is also known as the Boolean difference.

BoolExpr.iter_dfs()

Iterate through all expression nodes in DFS order.

BoolExpr.iter_domain()

Iterate through all points in the domain.

BoolExpr.iter_cfs(xs)

Iterate through all cofactors over a sequence of variables.

Atom Nodes

class boolexpr.Atom(cdata)

Bases: boolexpr.wrap.BoolExpr

Boolean Atom

class boolexpr.Constant(cdata)

Bases: boolexpr.wrap.Atom

Boolean Constant Atom

class boolexpr.Known(cdata)

Bases: boolexpr.wrap.Constant

Boolean Known Constant

class boolexpr.Zero(cdata)

Bases: boolexpr.wrap.Known

Boolean Zero

class boolexpr.One(cdata)

Bases: boolexpr.wrap.Known

Boolean One

class boolexpr.Unknown(cdata)

Bases: boolexpr.wrap.Constant

Boolean Unknown Constant

class boolexpr.Logical(cdata)

Bases: boolexpr.wrap.Unknown

Boolean Logical Unknown

class boolexpr.Literal(cdata)

Bases: boolexpr.wrap.Atom

Boolean Literal Atom

__abs__()

Absolute value operator

class boolexpr.Complement(cdata)

Bases: boolexpr.wrap.Literal

Boolean Complement

class boolexpr.Variable(cdata)

Bases: boolexpr.wrap.Literal

Boolean Variable

class boolexpr.Operator(cdata)

Bases: boolexpr.wrap.BoolExpr

Boolean Operator

simple

Return True if the operator is simple.

An operator is only deemed simple if it has been returned by the simplify method.

args

Return a tuple of the operator’s arguments.

is_clause()

Return True if the operator is a clause.

A clause is defined as having only Literal arguments.

Operator Nodes

class boolexpr.NegativeOperator(cdata)

Bases: boolexpr.wrap.Operator

Negative Operator

class boolexpr.LatticeOperator(cdata)

Bases: boolexpr.wrap.Operator

Boolean Lattice Operator

class boolexpr.Nor(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Nor Operator

class boolexpr.Nand(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Nand Operator

class boolexpr.Xnor(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Xnor Operator

class boolexpr.Unequal(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Unequal Operator

class boolexpr.NotImplies(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Not Implies Operator

class boolexpr.NotIfThenElse(cdata)

Bases: boolexpr.wrap.NegativeOperator

Boolean Not IfThenElse Operator

class boolexpr.Or(cdata)

Bases: boolexpr.wrap.LatticeOperator

Boolean Or Operator

class boolexpr.And(cdata)

Bases: boolexpr.wrap.LatticeOperator

Boolean And Operator

class boolexpr.Xor(cdata)

Bases: boolexpr.wrap.Operator

Boolean Xor Operator

class boolexpr.Equal(cdata)

Bases: boolexpr.wrap.Operator

Boolean Equal Operator

class boolexpr.Implies(cdata)

Bases: boolexpr.wrap.Operator

Boolean Implies Operator

class boolexpr.IfThenElse(cdata)

Bases: boolexpr.wrap.Operator

Boolean IfThenElse Operator

Constant Singletons

boolexpr.ZERO = 0

Boolean Zero

boolexpr.ONE = 1

Boolean One

boolexpr.LOGICAL = X

Boolean Logical Unknown

boolexpr.ILLOGICAL = ?

Boolean Illogical Unknown

Operator Functions

Fundamental Operators

boolexpr.not_(arg)

Boolean Not operator.

boolexpr.nor(*args)

Boolean Nor operator.

boolexpr.or_(*args)

Boolean Or operator.

boolexpr.nand(*args)

Boolean Nand operator.

boolexpr.and_(*args)

Boolean And operator.

boolexpr.xnor(*args)

Boolean Xnor operator.

boolexpr.xor(*args)

Boolean Xor operator.

boolexpr.neq(*args)

Boolean Unequal operator.

boolexpr.eq(*args)

Boolean Equal operator.

boolexpr.impl(p, q)

Boolean Implies operator.

boolexpr.ite(s, d1, d0)

Boolean IfThenElse operator.

Simplifying Operators

boolexpr.nor_s(*args)

Simplifying Boolean Nor operator.

boolexpr.or_s(*args)

Simplifying Boolean Or operator.

boolexpr.nand_s(*args)

Simplifying Boolean Nand operator.

boolexpr.and_s(*args)

Simplifying Boolean And operator.

boolexpr.xnor_s(*args)

Simplifying Boolean Xnor operator.

boolexpr.xor_s(*args)

Simplifying Boolean Xor operator.

boolexpr.neq_s(*args)

Simplifying Boolean Unequal operator.

boolexpr.eq_s(*args)

Simplifying Boolean Equal operator.

boolexpr.impl_s(p, q)

Simplifying Boolean Implies operator.

boolexpr.ite_s(s, d1, d0)

Simplifying Boolean IfThenElse operator.

High Order Operators

boolexpr.onehot0(*args)

Return an expression that means “at most one input function is true”.

boolexpr.onehot(*args)

Return an expression that means “exactly one input function is true”.

boolexpr.nhot(n, *args)

Return a CNF expression that means “exactly N input functions are true”.

boolexpr.majority(*args)

Return a CNF expression that means “the majority of input functions are true”.

boolexpr.achilles_heel(*args)

Return the Achille’s Heel function, defined as: \(\prod_{i=0}^{n/2-1}{X_{2i} + X_{2i+1}}\).

boolexpr.mux(a, sel)

Return an expression that multiplexes an input array over a select array.

boolexpr.exists(xs, f)

Return an expression that means “there exists a variable in xs such that f true.”

This is identical to f.smoothing(xs).

boolexpr.forall(xs, f)

Return an expression that means “for all variables in xs, f is true.”

This is identical to f.consensus(xs).

Multidimensional Arrays

class boolexpr.Array(cdata)

Wrap boolexpr::Array class

boolexpr.zeros(*dims)

Return a multi-dimensional array of zeros.

The variadic dims input is a sequence of dimension specs. A dimension spec is a two-tuple: (start index, stop index). If a dimension is given as a single int, it will be converted to (0, stop).

The dimension starts at index start, and increments by one up to, but not including, stop. This follows the Python slice convention.

For example, to create a 4x4 array of zeros:

>>> zeros(2, 4)
array([[0, 0, 0, 0],
       [0, 0, 0, 0]])

boolexpr.ones(*dims)

Return a multi-dimensional array of ones.

The variadic dims input is a sequence of dimension specs. A dimension spec is a two-tuple: (start index, stop index). If a dimension is given as a single int, it will be converted to (0, stop).

The dimension starts at index start, and increments by one up to, but not including, stop. This follows the Python slice convention.

For example, to create a 4x4 array of ones:

>>> ones(2, 4)
array([[1, 1, 1, 1],
       [1, 1, 1, 1]])

boolexpr.logicals(*dims)

Return a multi-dimensional array of X’s.

The variadic dims input is a sequence of dimension specs. A dimension spec is a two-tuple: (start index, stop index). If a dimension is given as a single int, it will be converted to (0, stop).

The dimension starts at index start, and increments by one up to, but not including, stop. This follows the Python slice convention.

For example, to create a 4x4 array of X’s:

>>> logicals(2, 4)
array([[X, X, X, X],
       [X, X, X, X]])

boolexpr.uint2nda(num, length=None)

Convert unsigned num to an array of expressions.

The num argument is a non-negative integer.

If no length parameter is given, the return value will have the minimal required length. Otherwise, the return value will be zero-extended to match length.

For example, to convert the byte 42 (binary 0b00101010):

>>> uint2nda(42, 8)
array([0, 1, 0, 1, 0, 1, 0, 0])

boolexpr.int2nda(num, length=None)

Convert num to an array of expressions.

The num argument is an int. Negative numbers will be converted using twos-complement notation.

If no length parameter is given, the return value will have the minimal required length. Otherwise, the return value will be sign-extended to match length.

For example, to convert the bytes 42 (binary 0b00101010), and -42 (binary 0b11010110):

>>> int2nda(42, 8)
array([0, 1, 0, 1, 0, 1, 0, 0])
>>> int2nda(-42, 8)
array([0, 1, 1, 0, 1, 0, 1, 1])

boolexpr.array(objs, shape=None)

Return an N-dimensional array of Boolean expressions.

The objs argument is a nested sequence of homogeneous Boolean expressions. That is, both [a, b, c, d] and [[a, b], [c, d]] are valid inputs.

The optional shape parameter is a tuple of dimension specs, which are (int, int) tuples. It must match the volume of objs. The shape can always be automatically determined from objs, but you can supply it to automatically reshape a flat input.

class boolexpr.ndarray(bxa, shape=None)

N-dimensional array of Boolean expressions

shape

Return the Array shape.

reshape(*dims)

Return an equivalent array with a modified shape.

ndim

Return the number of dimensions.

size

Return the size of the array.

The size of a multi-dimensional array is the product of the sizes of its dimensions.

flat

Return a 1D iterator over the array.

simplify()

Apply the simplify method to all expressions.

Returns a new array.

compose(var2bx)

Apply the compose method to all expressions.

Returns a new array.

restrict(point)

Apply the restrict method to all expressions.

Returns a new array.

equiv(other)

Return True if two arrays are equivalent.

Note

While in practice this check can be quite fast, SAT is an NP-complete problem, so some inputs will require exponential runtime.

zext(num)

Zero-extend this array by num bits.

Returns a new array.

sext(num)

Sign-extend this array by num bits.

Returns a new array.

nor_reduce()

NOR reduction operator

or_reduce()

OR reduction operator

nand_reduce()

NAND reduction operator

and_reduce()

AND reduction operator

xnor_reduce()

XNOR reduction operator

xor_reduce()

XOR reduction operator

lsh(a)

Left shift the a array into this array.

Returns a two-tuple (array, array)

rsh(a)

Right shift the a array into this array.

Returns a two-tuple (array, array)

arsh(num)

Arithmetically right shift the array by num places.

The num argument must be a non-negative int.

The shift-in will be the value of the most significant bit.

Returns a two-tuple (array, array)