pyfcstm.solver.safety

Optional expression safety scans for downstream SMT callers.

The core solver and verify algorithms are intentionally full-power by default: they translate the requested expression and let Z3 try the query. This module provides a separate syntactic scanner for callers such as diagnostics adapters that want to apply their own policy before invoking those core algorithms.

Example:

>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> expr = BinaryOp(Variable("x"), "*", Variable("y"))
>>> check_expr_safety(expr).reason
'nonlinear'

SafetyReason

pyfcstm.solver.safety.SafetyReason: alias of Literal[‘bitwise’, ‘transcendental’, ‘double_var_power’, ‘variable_exponent’, ‘nonlinear’]

SafetyCheck

class pyfcstm.solver.safety.SafetyCheck(safe: bool, reason: Literal['bitwise', 'transcendental', 'double_var_power', 'variable_exponent', 'nonlinear'] | None = None, offending_node: Expr | None = None)[source]

Result of an optional solver-safety expression scan.

Parameters:

safe (bool) – Whether the expression or operation block passes the optional downstream policy.
reason (Optional[SafetyReason], optional) – First unsafe reason found, defaults to None.
offending_node (Optional[pyfcstm.model.expr.Expr], optional) – First expression node that triggered the unsafe result, defaults to None.

Example:

>>> check = SafetyCheck(safe=False, reason="nonlinear")
>>> check.safe
False
>>> check.reason
'nonlinear'

check_expr_safety

pyfcstm.solver.safety.check_expr_safety(expr: Expr | None) → SafetyCheck[source]

Run an optional downstream policy scan over an expression.

Parameters:: expr (Optional[pyfcstm.model.expr.Expr]) – Expression to scan, or None for optional missing expressions.
Returns:: Safety-policy result. The first policy-rejected node in pre-order traversal is reported when a hazard is found.
Return type:: SafetyCheck

Example:

>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> check_expr_safety(Integer(1)).safe
True
>>> expr = BinaryOp(Variable("x"), "*", Variable("y"))
>>> check_expr_safety(expr).reason
'nonlinear'

check_expr_safety_for_effect

pyfcstm.solver.safety.check_expr_safety_for_effect(ops: Sequence[OperationStatement]) → SafetyCheck[source]

Run an optional downstream policy scan over an operation block.

Parameters:: ops (Sequence[OperationStatement]) – Operation statements from an enter / during / exit / effect block.
Returns:: First policy-rejected expression result, or a safe result if all scanned expressions are acceptable.
Return type:: SafetyCheck

Example:

>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> from pyfcstm.model.model import Operation
>>> ops = [Operation("x", BinaryOp(Variable("x"), "*", Variable("y")))]
>>> check_expr_safety_for_effect(ops).reason
'nonlinear'