Functions

The recommended entry points for most users.

pysignet.api.compile_logic(expr, predicates, mode='tnorm', tnorm=None, alpha=1.0)

Compile logic expression into a CompiledExpression.

This is the main entry point for most users. It compiles a SymPy logic expression into a CompiledExpression that can evaluate satisfaction degrees per-batch. Wrap the result in LogicLoss for loss computation and batch quantification.

Parameters:

Name	Type	Description	Default
expr	Basic	SymPy logic expression (e.g., sp.And(P(X), Q(X)))	required
predicates	dict[str, Predicate | Callable[..., Tensor]]	Dict mapping predicate names to Predicate objects or callables that produce torch Tensors	required
mode	str	Compilation mode - 'tnorm' (default) or 'ltu'	'tnorm'
tnorm	TNorm | None	T-norm for mode='tnorm' (default: MixedTNorm). Ignored for other modes.	None
alpha	float	Sigmoid sharpness for mode='ltu' (default: 1.0). Larger values make AND/OR thresholds sharper.	1.0

Returns:

Type	Description
CompiledExpression	CompiledExpression instance for evaluating satisfaction degrees

Raises:

Type	Description
ValueError	If unknown mode specified, or tnorm= given with mode='ltu'

Examples:

Default (MixedTNorm):

P, Q = Symbol("P Q")
X = Variable("X")
expr = sp.And(P(X), Q(X))
compiled = compile_logic(expr, {"P": model_p, "Q": model_q})
satisfaction = compiled(X=x)  # shape: (batch_size,)

With a custom t-norm:

from pysignet.tnorms import LukasiewiczTNorm
compiled = compile_logic(expr, predicates, tnorm=LukasiewiczTNorm())

With the LTU compiler:

compiled = compile_logic(expr, predicates, mode='ltu', alpha=2.0)

pysignet.api.logic_to_loss(expr, predicates, mode='tnorm', tnorm=None, alpha=1.0, post_processing=None)

Compile logic expression and wrap in LogicLoss.

Convenience function that compiles a logic expression and wraps it in a LogicLoss for training. Equivalent to:

compiled = compile_logic(expr, predicates, mode=mode, tnorm=tnorm,
                         alpha=alpha)
LogicLoss(compiled, post_processing=post_processing)

Parameters:

Name	Type	Description	Default
expr	Basic	SymPy logic expression (e.g., sp.And(P(X), Q(X)))	required
predicates	dict[str, Predicate | Callable[..., Tensor]]	Dict mapping predicate names to Predicate objects or callables that produce torch Tensors	required
mode	str	Compilation mode - 'tnorm' (default) or 'ltu'	'tnorm'
tnorm	TNorm | None	T-norm for mode='tnorm' (default: MixedTNorm). Ignored for other modes.	None
alpha	float	Sigmoid sharpness for mode='ltu' (default: 1.0).	1.0
post_processing	str | Callable[[Tensor], Tensor] | None	Post-processing mode - 'log', 'linear', callable, or None to use the compiler's recommendation (default)	None

Returns:

Type	Description
LogicLoss	LogicLoss instance ready for computing satisfaction and loss

Examples:

P, Q = Symbol("P Q")
X = Variable("X")
expr = sp.Implies(P(X), Q(X))
logic_loss = logic_to_loss(expr, {"P": model_p, "Q": model_q})
loss = logic_loss.loss(X=x)

With LTU compiler:

logic_loss = logic_to_loss(expr, predicates, mode='ltu', alpha=2.0)

pysignet.api.consistency_report(expression, predicates)

Create a ConsistencyReport for measuring formula consistency.

Convenience function that auto-wraps raw callables in Predicate objects and creates a ConsistencyReport. Equivalent to:

ConsistencyReport(expression, predicates)

Accepts a single SymPy expression or a dict mapping constraint names to expressions for multi-constraint reporting.

The antecedent for conditional violation is auto-detected: Implies(A, B) uses A; any other formula uses sp.true.

Parameters:

Name	Type	Description	Default
expression	Basic | dict[str, Basic]	SymPy logic expression or dict of named expressions (e.g., {"sym": expr1, "trans": expr2}).	required
predicates	dict[str, Predicate | Callable[..., Tensor]]	Dict mapping predicate names to Predicate objects or callables that produce torch Tensors	required

Returns:

Type	Description
ConsistencyReport	ConsistencyReport instance for accumulating and querying metrics

Example

P, Q = Symbol("P Q")
X = Variable("X")
expr = sp.Implies(P(X), Q(X))
report = consistency_report(expr, {"P": model_p, "Q": model_q})
for x_batch in dataloader:
    report.eval(X=x_batch)
print(report.global_violation())