Python API

Construct circuits on a shared Vtree; combine them with operators or the named functions below. Transformation methods consume their circuit inputs. Query methods borrow them. See Using and reusing circuits for the rules that apply across the API, and What are we counting? for observations, substitution and projection.

Domains and values

class tididi.Vtree

A shared variable decomposition. Reuse one vtree for circuits you will combine.

static balanced(n)

Build a balanced vtree over variables 1 through n. n must be positive.

static balanced_over(variables)

Build a balanced vtree with leaves in the supplied order of distinct positive IDs.

clear_scratch()

Release idle operation scratch without changing any circuit.

static from_text(text)

Parse .vtree text. Reuse the returned object when loading related circuits.

static join(left, right)

Join disjoint vtrees under a new root, leaving both inputs usable.

static leaf(variable)

Build a one-variable vtree.

static linear(variables)

Build a right-linear vtree with leaves in the supplied order.

to_dot()

Return Graphviz DOT describing this vtree.

to_text()

Serialize the shape and variable IDs as .vtree text.

variables

Variable IDs in left-to-right leaf order.

class tididi.Literal(variable, sign=True)

An immutable named literal value. Positive integers mean true, negative integers false. Unlike a Circuit, a Literal is never consumed.

sign

True for a positive literal, false for a negated one.

variable

The positive, one-based variable ID.

Construction

tididi.literal(vtree, value, *, limits=None)

Construct a literal circuit from a signed integer or an immutable Literal value.

tididi.cube(vtree, literals, *, limits=None)

Construct a conjunction of signed integers or Literal values. Omitted variables are free. Each variable may occur once; an empty iterable constructs true.

tididi.clause(vtree, literals, *, limits=None)

Construct a disjunction of literals. An empty iterable constructs false.

tididi.from_models(vtree, variables, rows, *, limits=None)

Construct the set of Boolean rows over variables, leaving other variables free. Every row must contain one bool per variable. Repeated rows count once. Empty rows denote false; one empty row over no variables denotes true.

tididi.one(vtree)

Construct true over every variable of vtree.

tididi.zero(vtree)

Construct false over every variable of vtree.

Boolean composition

tididi.and_(left, right, *, limits=None)

Conjoin two circuits, consuming both. Equivalent to left & right, with optional limits. Copy operands first if they must remain usable, including for retry after a resource error.

tididi.or_(left, right, *, limits=None)

Disjoin two circuits, consuming both. Equivalent to left | right, with optional limits.

tididi.xor(left, right, *, limits=None)

Exclusive-or two circuits, consuming both. Also available as left ^ right.

tididi.ite(condition, then_branch, else_branch, *, limits=None)

Build (condition & then_branch) | (~condition & else_branch), consuming all three inputs.

tididi.or_many(circuits, *, limits=None)

Union a nonempty iterable of circuits, consuming every element. Duplicate handles are rejected; pass explicit copies when reusing a circuit.

tididi.and_exists(left, right, variables, *, limits=None)

Conjoin, then existentially quantify variables in one call, consuming both circuits. This computes the same function as (left & right).exists(variables).

Circuits and counters

class tididi.Circuit

An owned Boolean circuit. Construct one with literal, cube, clause, from_models, one or zero.

&, |, ^, ~ and transformation methods consume their circuit operands. Queries borrow. copy() explicitly duplicates storage while sharing the vtree. Reusing a consumed object raises ConsumedCircuitError, including through an alias.

condition(literals, *, limits=None)

Substitute the given literal values, consuming this circuit. Repeated literals are ignored; opposite signs for one variable produce false. Assigned variables become free in the resulting function’s counting universe. To count assignments consistent with evidence, use counter() instead.

copy()

Duplicate diagram storage, leaving the original usable. The vtree is shared.

counter()

Copy first to retain an independently usable circuit while the counter is open.

equivalent(other, *, limits=None)

Compare Boolean functions without consuming either circuit. Both must share a vtree.

evaluate(algebra)

Evaluate a Python algebra with zero(), leaf(variable, sign), add(a, b), mul(a, b). sign is True, False, or None for a free variable. Values must be immutable; add and mul return new values. Borrows the circuit and propagates callback errors. Python callbacks run attached to the interpreter; use weighted_count for a native exact sum.

evaluator(weights)

Move this circuit into a reusable evidence counter. Call counter.finish() to recover it. Consume this circuit into an exact weighted evaluator. Copy first to retain the circuit. Supply every variable’s (negative, positive) int or Fraction weights.

exists(variables, *, limits=None)

Existentially quantify variables, consuming this circuit. Quantified variables remain free in the vtree; use projected_model_count to count distinct projections.

static from_bytes(vtree, data)

Load serialized circuit bytes onto an existing vtree.

implied_literals(*, limits=None)

Literals true in every model. False implies both signs of every vtree variable.

implies(other, *, limits=None)

Whether every model of this circuit satisfies other. Borrows both circuits.

is_consumed

Whether this wrapper has given up its circuit. This property remains readable afterward.

is_sat(*, limits=None)

Whether at least one assignment satisfies this circuit. Borrows the circuit.

static load(vtree, path)

Read a circuit file onto an existing vtree.

minimize(*, limits=None)

Minimize and return this circuit, consuming the old wrapper. The result is canonical for its vtree; its Boolean function is unchanged.

model_count(*, limits=None)

Count satisfying assignments over all vtree variables. Returns an arbitrary-precision int.

negate(*, limits=None)

Complement this circuit, consuming it. Equivalent to ~circuit, with optional limits.

node_count()

Number of stored circuit nodes, excluding implicit leaf nodes.

node_sizes()

Snapshot of (vtree_node, local_node, pair_count) for every stored internal node. Storage IDs are local to this circuit and may change after transformation.

pair_count()

Number of stored child pairs.

projected_model_count(variables, *, limits=None)

Count distinct assignments to variables that extend to a satisfying assignment.

rename(mapping, *, limits=None)

Simultaneously rename variables using a dict {source: target}, consuming this circuit. Swaps and cycles are simultaneous; several sources may map to the same target. The vtree and its counting universe stay unchanged.

satisfying_assignment(*, limits=None)

One complete satisfying assignment as Literal values, or None if unsatisfiable.

save(path)

Write this circuit to a path, leaving it usable. Save its vtree separately.

support(*, limits=None)

Variable IDs on which the function depends, without consuming the circuit.

to_bytes()

Serialize to bytes. Save the vtree too; related circuits must reload onto one shared vtree.

to_dot()

Return Graphviz DOT for inspecting this circuit.

update(*, insert=None, remove=None, limits=None)

Insert cubes, then remove cubes, returning a minimized circuit and consuming this one. Each cube is an iterable of signed integers or Literal values. Omitted variables are free; an empty cube matches every assignment. Contradictory cubes change nothing. Limits apply to each update and to the final minimization separately.

vtree

The shared vtree. Circuits built on this value can be combined with this circuit.

weighted_count(weights, *, limits=None)

Exact weighted sum as fractions.Fraction. Supply {variable: (negative, positive)} weights, each an int or Fraction, for every vtree variable. Borrows the circuit.

class tididi.Counter

Reuse cached counts while observations change. Created by Circuit.counter(), which consumes it. observe() replaces pins for the named variables; other pins remain. finish() returns the original circuit.

clear(variable)

Remove one observation, leaving that variable free again.

clear_observations()

Remove all observations.

finish()

Discard cached counts and observations, returning the original circuit. Closes this counter.

model_count(*, limits=None)

Count assignments consistent with the observations. Borrows the owned circuit.

observe(literals)

Set observations from signed integers or Literal values without changing the circuit. A later observation for a variable replaces its previous value.

class tididi.Evaluator

Cache exact weighted sums under changing evidence. Circuit.evaluator(weights) consumes the circuit. value() returns the joint weight of the circuit and observations. finish() returns the circuit.

clear(variable)

Clear one observation.

clear_observations()

Clear all observations, retaining cached storage.

finish()

Close this evaluator and return the original circuit without its observations.

observe(literals)

Observe signed integers or Literal values. Invalid input preserves all observations.

set_weights(weights)

Replace every variable’s (negative, positive) weights, retaining observations. Weights are int or Fraction values. Invalid input leaves previous weights in place.

value(*, limits=None)

Return the exact weighted sum under observations, refreshing only affected ancestors. Probability weights give joint probability; no normalization is performed.

Custom evaluation

class tididi.Algebra(*args, **kwargs)

Evaluate disjoint alternatives with add and independent groups with mul.

Values must be immutable. Both operations must be associative and commutative; mul distributes over add. zero is the identity for add and absorbing for mul. For each variable, leaf(variable, None) must equal add(leaf(variable, False), leaf(variable, True)): a free variable includes both assignments. Violating these laws can make equivalent circuits evaluate differently. Floating-point arithmetic only approximates the algebraic laws; use exact values when exact results matter.

zero()

The value of an impossible event (the additive identity).

Return type:

_T

leaf(variable, sign)

Evaluate a positive, negative, or free leaf.

Parameters:

• variable (int)

• sign (bool | None)

Return type:

_T

add(a, b)

Combine disjoint alternatives without mutating either argument.

Parameters:

• a (_T)

• b (_T)

Return type:

_T

mul(a, b)

Combine independent variable groups without mutating either argument.

Parameters:

• a (_T)

• b (_T)

Return type:

_T

Execution and errors

class tididi.Limits(*, memory_bytes=None, output_nodes=None, timeout=None)

Optional resource bounds for one operation. Unspecified bounds are unlimited. memory_bytes bounds charged operation storage, not the process’s total memory. timeout is in seconds and is checked at cooperative polling points.

exception tididi.ConsumedCircuitError

A circuit was already consumed. Copy it before a consuming operation to retain it.

exception tididi.ResourceLimitError

An operation exceeded its output-node cap or reached its deadline.