CompiledExpression

pysignet.compilation.compiled_expression.CompiledExpression

Represents a compiled logical expression with variable bindings.

A compiled expression is the result of compiling a logical expression (e.g., And(P(X), Q(Y))) into a differentiable PyTorch computation graph. It supports:

• Evaluation with variable bindings: compiled(X=x, Y=y) -> Tensor
• Partial binding: compiled.partial(X=x) -> CompiledExpression
• Introspection: compiled.free_variables -> Set[str]
• Compiler access: compiled.compiler -> LogicCompiler

CompiledExpression performs PURE EVALUATION - it always returns per-batch results with shape (batch_size,). No batch reduction is applied. For quantification over batch dimensions, wrap with LogicLoss.

Partial binding creates a NEW computation graph with fewer free variables, not just a temporary store of bindings. This enables future optimizations like constant propagation, dead code elimination, and graph rewriting.

IMPORTANT: All inputs must be provided as keyword arguments (e.g., X=tensor). Positional arguments are not supported. This ensures clear, unambiguous variable binding.

Parameters:

Name	Type	Description	Default
compiled_logic	Callable[[dict[str, Tensor]], Tensor]	Callable that evaluates the expression given variable bindings as a dict mapping variable names to tensors	required
free_variables	set[str]	Set of variable names that must be bound for evaluation	required
predicates	dict[str, Predicate]	Dict mapping predicate names to Predicate objects	required
partial_bindings	dict[str, Tensor] | None	Dict of variables already bound in this expression (used internally for partial binding)	None
compiler	LogicCompiler | None	Optional LogicCompiler that produced this expression	None
expr	Basic | None	Optional original SymPy expression (for repr/debugging)	None

Example

# Create compiled expression
compiled = compiler.compile(expr, predicates)

# Evaluate with full bindings - returns (batch_size,)
result = compiled(X=x, Y=y)  # shape: (batch_size,)

# Partial binding
partial = compiled.partial(X=x)
result = partial(Y=y)  # shape: (batch_size,)

# Introspection
print(compiled.free_variables)  # {'X', 'Y'}
print(partial.free_variables)   # {'Y'}
print(compiled.compiler)        # TNormCompiler(...)

compiler property

Return the LogicCompiler that produced this expression.

Returns:

Type	Description
LogicCompiler | None	LogicCompiler instance or None

expr property

Return the original SymPy expression.

Returns:

Type	Description
Basic | None	SymPy expression or None

free_variables property

Return set of variables that still need to be bound.

Returns:

Type	Description
set[str]	Set of variable names not yet bound

Example

compiled.free_variables  # {'X', 'Y'}
partial = compiled.partial(X=x)
partial.free_variables   # {'Y'}

__call__(*, return_boolean=False, log_mode=False, **variable_bindings)

Evaluate compiled expression with variable bindings.

All free variables must be bound (either via partial bindings stored in this expression, or provided here as keyword arguments).

This method performs PURE EVALUATION - it always returns per-batch results with shape (batch_size,). No batch reduction is applied. For quantification over batch dimensions, wrap with LogicLoss.

Parameters:

Name	Type	Description	Default
return_boolean	bool	If True, return boolean satisfaction using hard decisions (threshold at 0.5 for binary, argmax for multiclass). Default is False (soft satisfaction).	False
log_mode	bool	If True, evaluate in log-space using fused ops (logsigmoid, log_softmax) for numerical stability. Returns log-satisfaction values in (-inf, 0]. Default is False.	False
**variable_bindings	Tensor	Variable bindings as keyword arguments (e.g., X=x_tensor, Y=y_tensor)	{}

Returns:

Type	Description
Tensor	If return_boolean is False and log_mode is False: Satisfaction tensor of shape (batch_size,) in [0, 1].
Tensor	If log_mode is True: Log-satisfaction tensor of shape (batch_size,) in (-inf, 0].
Tensor	If return_boolean is True: Boolean tensor of shape (batch_size,) indicating whether the formula is satisfied.

Raises:

Type	Description
ValueError	If any free variable is not bound
ValueError	If return_boolean=True but expression is not available

Example

# Soft satisfaction (default)
result = compiled(X=x, Y=y)  # shape: (batch_size,)

# Log-space satisfaction
result = compiled(log_mode=True, X=x)  # log-probs

# Boolean satisfaction
result = compiled(X=x, Y=y, return_boolean=True)

__init__(compiled_logic, free_variables, predicates, partial_bindings=None, compiler=None, expr=None, compiled_logic_log=None)

Initialize CompiledExpression.

Parameters:

Name	Type	Description	Default
compiled_logic	Callable[[dict[str, Tensor]], Tensor]	Callable that evaluates expression with inputs as a dict mapping variable names to tensors.	required
free_variables	set[str]	Set of variable names in the original expression	required
predicates	dict[str, Predicate]	Dict of predicate objects	required
partial_bindings	dict[str, Tensor] | None	Dict of variables already bound (default: empty)	None
compiler	LogicCompiler | None	Optional LogicCompiler that produced this expression	None
expr	Basic | None	Optional original SymPy expression (for repr/debugging)	None
compiled_logic_log	Callable[[dict[str, Tensor]], Tensor] | None	Optional callable for log-space evaluation using fused ops (logsigmoid, log_softmax).	None

__repr__()

Return string representation of compiled expression.

Returns:

Type	Description
str	String showing expression, free variables, and predicates.

get_trainable_parameters()

Get all trainable parameters from model-based predicates.

Returns:

Type	Description
list[Parameter]	List of torch.nn.Parameter objects from all model-based
list[Parameter]	predicates

Example

params = compiled.get_trainable_parameters()
optimizer = torch.optim.Adam(params, lr=0.001)

partial(**variable_bindings)

Create new CompiledExpression with some variables bound.

This creates a NEW computation graph where the bound variables are substituted with their values. The returned CompiledExpression has fewer free variables.

Future optimizations will use this to: - Constant-fold operations on bound variables - Apply common subexpression elimination - Prune unreachable branches - Rewrite the computation graph for efficiency

Parameters:

Name	Type	Description	Default
**variable_bindings	Tensor	Variable bindings to fix (X=x, Y=y)	{}

Returns:

Type	Description
CompiledExpression	New CompiledExpression with fewer free variables

Raises:

Type	Description
ValueError	If no bindings provided
ValueError	If variable is already bound
ValueError	If variable doesn't exist in expression

Example

# Bind X, leaving Y for later
partial = compiled.partial(X=x)
print(partial.free_variables)  # {'Y'}

# Chain partial bindings
result = compiled.partial(X=x).partial(Y=y)(Z=z)

# Bind multiple at once
partial = compiled.partial(X=x, Y=y)