boundlab.expr.Expr

class boundlab.expr.Expr

Bases: object

Abstract base class for all symbolic expressions in BoundLab.

Each expression represents a node in a directed acyclic graph (DAG) of computations. Expressions are immutable after construction, and each instance is assigned a unique time-ordered UUID to enable deterministic topological ordering during bound propagation.

Subclasses must implement shape, children, and backward() to define the expression’s semantics.

Methods

__init__
backward	Perform backward-mode bound propagation through this expression.
bound_width	Compute the width of the bounds for this expression.
center	Compute the center of the bounds for this expression.
diag
expand
flatten
flip
gather
get_const	Return the concrete tensor if self is a pure constant expression, else None.
jacobian_ops_	Recursively compute Jacobian ops for affine expressions.
lb	Compute a lower bound for this expression.
narrow
permute
repeat
reshape
roll
scatter
squeeze
tile
to_string	Return string representation with child strings substituted.
transpose
ub	Compute an upper bound for this expression.
ublb	Compute both an upper bound and a lower bound for this expression.
unflatten
unsqueeze
with_children	Return a new expression with the same type and flags but new children.
zeros_set

__init__(flags=<ExprFlags.NONE: 0>)

id: int

Unique identifier for the expression, used for topological sorting.

flags: ExprFlags

Flags indicating expression properties for optimization.

with_children(*new_children)

Return a new expression with the same type and flags but new children.

property shape: torch.Size

The shape of the output(s) produced by this expression.

property children: tuple[Expr, ...]

The child expressions that serve as inputs to this expression.

backward(weights, direction='==')

Perform backward-mode bound propagation through this expression.

Given an accumulated weight weights (usually a EinsumOp) from the output back to this node, backward propagation derives child weights and a bias:

\[\mathbf{w}^\top f(x_1, \ldots, x_n) \;\square\; b + \sum_i \mathbf{w}_i^\top x_i\]

Parameters:

• weights (LinearOp) – A EinsumOp accumulated weight from the root expression to this node.

• direction (Literal['>=', '<=', '==']) – Bound direction — ">=" (lower), "<=" (upper), or "==" (exact).

Returns:

A tuple (bias, child_weights) where bias is a torch.Tensor or 0, and child_weights is a list of EinsumOp (one per child). Returns None if this expression cannot contribute to the bound in the given direction.

Return type:

tuple[torch.Tensor, list[LinearOp]] | None

to_string(*children_str)

Return string representation with child strings substituted.

__add__(other)

__mul__(other)

Element-wise multiplication (no broadcast).

reshape(*shape)

permute(*dims)

transpose(dim0, dim1)

property T: Expr

Convenience for transpose of the last two dimensions.

flatten(start_dim=0, end_dim=-1)

unflatten(dim, sizes)

squeeze(dim=None)

unsqueeze(dim)

narrow(dim, start, length)

expand(*sizes)

repeat(*sizes)

tile(*sizes)

flip(dims)

roll(shifts, dims)

diag(diagonal=0)

zeros_set(output_shape)

scatter(indices, output_shape)

gather(indices)

ub()

Compute an upper bound for this expression.

lb()

Compute a lower bound for this expression.

ublb()

Compute both an upper bound and a lower bound for this expression.

center()

Compute the center of the bounds for this expression.

bound_width()

Compute the width of the bounds for this expression.

get_const()

Return the concrete tensor if self is a pure constant expression, else None.

Works for ConstVal and any AffineSum that has no symbolic children.

jacobian_ops_()

Recursively compute Jacobian ops for affine expressions.