Compilers

pysignet.compilation.TNormCompiler

Bases: LogicCompiler

Compiles logic expressions using t-norm relaxations.

TNormCompiler uses continuous t-norm relaxations (Product, Lukasiewicz, Godel, etc.) to convert crisp logical operators into differentiable operations over [0,1].

The compile() method returns a CompiledExpression that evaluates the expression when called with inputs.

Parameters:

Name	Type	Description	Default
tnorm	TNorm | None	T-norm instance for relaxation (default: MixedTNorm)	None
jit	bool	If True, wrap the combinator-dispatch step in torch.compile for formulas with at least JIT_SIZE_THRESHOLD leaf atoms. Default False (opt-in; see TODO.md 2.21). Predicate calls are never traced -- only the connective combination of already-evaluated leaf tensors is compiled.	False

Example

compiler = TNormCompiler()  # uses MixedTNorm by default
compiled = compiler.compile(expr, predicates)
satisfaction = compiled(X=x)  # Returns tensor in [0, 1]

recommended_postprocessing property

Delegate to t-norm's recommendation.

tnorm property

The TNorm that is used for this relaxation

__init__(tnorm=None, jit=False)

Initialize TNormCompiler with a t-norm.

Parameters:

Name	Type	Description	Default
tnorm	TNorm | None	T-norm for logical operator relaxation. If None, uses MixedTNorm as default (matches compile_logic default).	None
jit	bool	Opt-in torch.compile path for large formulas. Default False. See class docstring.	False

compile(expr, predicates)

Compile a logic expression into a differentiable CompiledExpression.

Parameters:

Name	Type	Description	Default
expr	Basic	SymPy logic expression (e.g., sp.And(P, sp.Or(Q, sp.Not(R))))	required
predicates	dict[str, Predicate | Callable[..., Tensor]]	Dict mapping predicate names to Predicate objects. Raw callables (functions, nn.Modules) are automatically wrapped in Predicate objects.	required

Returns:

Type	Description
CompiledExpression	CompiledExpression that can be evaluated with variable bindings,
CompiledExpression	supports partial binding, and provides introspection.

Raises:

Type	Description
ValueError	If symbols in expr have no corresponding predicates
TypeError	If predicate values are not callable or Predicate

conjunction(values)

Delegate to t-norm conjunction.

disjunction(values)

Delegate to t-norm disjunction.

equivalence(a, b)

Delegate to t-norm equivalence.

implication(a, b)

Delegate to t-norm implication.

negation(a)

Delegate to t-norm negation.

pysignet.compilation.LinearThresholdUnitCompiler

Bases: LogicCompiler

Compiles logic expressions using linear threshold units.

This compiler represents logical operations as linear threshold units: - Conjunction of n literals: sgn(sum(literals) - (n - 0.5)) - Disjunction of n literals: sgn(sum(literals) - 0.5) - Negation: 1 - literal - Implication: compiled as (NOT L) OR R - Equivalence: compiled as (L => R) AND (R => L)

Parameters:

Name	Type	Description	Default
mode	str	'soft' (sigmoid, differentiable) or 'hard' (sign, non-differentiable). Default: 'soft'	'soft'
alpha	float	Multiplier for sigmoid if mode = 'soft'. Default: 1.0 When alpha is large, the sigmoids become closer to thresholds and have larger gradients around zero.	1.0
jit	bool	If True, wrap the combinator-dispatch step in torch.compile for formulas with at least JIT_SIZE_THRESHOLD leaf atoms. Default False (opt-in; see TODO.md 2.21). Predicate calls are never traced -- only the connective combination of already-evaluated leaf tensors is compiled.	False

Example

compiler = LinearThresholdUnitCompiler(mode='soft')
compiled = compiler.compile(expr, predicates)
satisfaction = compiled(X=x)  # Returns tensor in [0, 1]

recommended_postprocessing property

LTU recommends linear post-processing.

__init__(mode='soft', alpha=1.0, jit=False)

Initialize LinearThresholdUnitCompiler.

Parameters:

Name	Type	Description	Default
mode	str	'soft' for sigmoid (differentiable) or 'hard' for sign (non-differentiable). Default: 'soft'	'soft'
alpha	float	Multiplier for sigmoid if mode = 'soft'. Default: 1.0. When alpha is large, the sigmoids become closer to thresholds and have larger gradients around zero. Ignored when mode = "hard"	1.0
jit	bool	Opt-in torch.compile path for large formulas. Default False. See class docstring.	False

Raises:

Type	Description
ValueError	If mode is not 'soft' or 'hard'

compile(expr, predicates)

Compile a logic expression into a CompiledExpression.

Parameters:

Name	Type	Description	Default
expr	Basic	SymPy logic expression	required
predicates	dict[str, Predicate | Callable[..., Tensor]]	Dict mapping predicate names to Predicate objects or callables	required

Returns:

Type	Description
CompiledExpression	CompiledExpression that can be evaluated with variable
CompiledExpression	bindings, supports partial binding, and provides
CompiledExpression	introspection.

Raises:

Type	Description
ValueError	If symbols in expr have no corresponding predicates
TypeError	If predicate values are not callable

conjunction(values)

LTU conjunction: threshold(sum(values) - (n - 0.5)).

Parameters:

Name	Type	Description	Default
values	Tensor	Tensor of shape (n, ...) with values in [0, 1].	required

Returns:

Type	Description
Tensor	Tensor of shape (...) with conjunction applied.

disjunction(values)

LTU disjunction: threshold(sum(values) - 0.5).

Parameters:

Name	Type	Description	Default
values	Tensor	Tensor of shape (n, ...) with values in [0, 1].	required

Returns:

Type	Description
Tensor	Tensor of shape (...) with disjunction applied.