pyfcstm.solver.domain

Runtime-definedness translation for solver-layer expressions.

This module keeps FCSTM expression runtime-domain constraints separate from the Z3 value expression. Z3 arithmetic operators are total, while FCSTM runtime expression evaluation is not: division by zero, modulo by zero, and square root of a negative value are runtime-domain failures. Callers decide when to add the returned definedness constraints to a solver.

Example:

>>> import z3
>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> from pyfcstm.solver.domain import translate_expr_domain
>>> # Division produces both a value expression and a divisor guard.
>>> expr = BinaryOp(x=Variable("x"), op="/", y=Integer(2))
>>> result = translate_expr_domain(expr, {"x": z3.Int("x")})
>>> result.failure is None
True
>>> len(result.definedness_constraints)
1

__all__

pyfcstm.solver.domain.__all__ = ['BranchFeasibility', 'DomainConstraint', 'DomainSource', 'ExprDomain', 'TranslationFailure', 'merge_definedness_constraints', 'translate_expr_domain']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

DomainSource

class pyfcstm.solver.domain.DomainSource(label: str | None = None, step: int | None = None, snapshot: str | None = None, prefix_id: str | None = None)[source]

Pure source metadata for domain constraints and failures.

This object records where a solver-layer runtime-definedness constraint or translation failure came from without importing verification or diagnostics types. All fields are optional so callers can attach only the provenance they know at the current expression point.

Parameters:

  • label (Optional[str], optional) – Human-readable source label, defaults to None.

  • step (Optional[int], optional) – Operation-step index associated with the source, defaults to None.

  • snapshot (Optional[str], optional) – Name of the symbolic snapshot, defaults to None.

  • prefix_id (Optional[str], optional) – Path or branch prefix identifier, defaults to None.

Example:

>>> # Callers attach only the source fields they know.
>>> source = DomainSource(label="guard", step=0)
>>> source.label
'guard'

DomainConstraint

class pyfcstm.solver.domain.DomainConstraint(constraint: ExprRef, source: DomainSource | None = None)[source]

Runtime-definedness constraint plus optional source metadata.

Parameters:

  • constraint (z3.ExprRef) – Z3 predicate that must hold for FCSTM runtime expression evaluation to be defined.

  • source (Optional[DomainSource], optional) – Optional source metadata for diagnostics or evidence, defaults to None.

Example:

>>> import z3
>>> x = z3.Int("x")
>>> # The constraint records the runtime precondition for a divisor.
>>> item = DomainConstraint(x != 0, DomainSource(label="divisor"))
>>> item.source.label
'divisor'

TranslationFailure

class pyfcstm.solver.domain.TranslationFailure(kind: str, reason: str, source: DomainSource | None = None)[source]

Expected expression translation failure in pure solver-layer form.

Parameters:

  • kind (str) – Normalized failure kind such as "not_implemented" or "z3_error".

  • reason (str) – Human-readable failure reason.

  • source (Optional[DomainSource], optional) – Optional source metadata, defaults to None.

Example:

>>> # Failures remain pure solver-layer data without verify imports.
>>> failure = TranslationFailure("value_error", "bad expression")
>>> failure.kind
'value_error'

BranchFeasibility

class pyfcstm.solver.domain.BranchFeasibility(selector: ExprRef, status: str, source: DomainSource | None = None)[source]

Recorded branch reachability query for conditional expressions.

Parameters:

  • selector (z3.ExprRef) – Z3 predicate selecting the branch.

  • status (str) – Normalized reachability status: "sat", "unsat", or "unknown".

  • source (Optional[DomainSource], optional) – Optional source metadata, defaults to None.

Example:

>>> import z3
>>> # A satisfiable selector means the branch may contribute evidence.
>>> check = BranchFeasibility(z3.BoolVal(True), "sat")
>>> check.status
'sat'

ExprDomain

class pyfcstm.solver.domain.ExprDomain(z3_expr: ArithRef | BoolRef | None, expr_constraints: Tuple[ExprRef, ...] = (), assumptions: Tuple[ExprRef, ...] = (), definedness_constraints: Tuple[DomainConstraint, ...] = (), failure: TranslationFailure | None = None, feasibility_checks: Tuple[BranchFeasibility, ...] = ())[source]

Domain-aware translation result for one expression.

expr_constraints is reserved for future solver-only value constraints. The current translator does not populate it; every path returns ().

Parameters:

  • z3_expr (Optional[Union[z3.ArithRef, z3.BoolRef]]) – Translated Z3 value expression, or None when translation failed.

  • expr_constraints (Tuple[z3.ExprRef, ...], optional) – Solver-only constraints associated with the value expression, defaults to ().

  • assumptions (Tuple[z3.ExprRef, ...], optional) – Caller-supplied facts preserved on the result, defaults to ().

  • definedness_constraints (Tuple[DomainConstraint, ...], optional) – Runtime-definedness constraints that must hold before using z3_expr, defaults to ().

  • failure (Optional[TranslationFailure], optional) – Expected translation failure, defaults to None.

  • feasibility_checks (Tuple[BranchFeasibility, ...], optional) – Branch reachability checks performed while pruning conditional expressions, defaults to ().

Example:

>>> import z3
>>> # A minimal successful result only needs a translated value.
>>> result = ExprDomain(z3.IntVal(1))
>>> result.z3_expr
1

translate_expr_domain

pyfcstm.solver.domain.translate_expr_domain(expr: Expr, z3_vars: Dict[str, ArithRef | BoolRef], *, assumptions: Sequence[ExprRef] = (), path_conditions: Sequence[ExprRef] = (), source: DomainSource | None = None, prune_unreachable: bool = True, timeout_ms: int | None = None) → ExprDomain[source]

Translate an expression and return runtime-definedness metadata.

Parameters:

  • expr (pyfcstm.model.expr.Expr) – Expression to translate.

  • z3_vars (Dict[str, Union[z3.ArithRef, z3.BoolRef]]) – Symbolic variable mapping.

  • assumptions (Sequence[z3.ExprRef], optional) – Caller-known facts preserved on the result.

  • path_conditions (Sequence[z3.ExprRef], optional) – Current path predicates used only for branch feasibility pruning; they are not stored on the result.

  • source (Optional[DomainSource], optional) – Optional pure source metadata.

  • prune_unreachable (bool, optional) – Whether to skip value branches proved unreachable, defaults to True.

  • timeout_ms (Optional[int], optional) – Optional timeout for branch reachability checks.

Returns:

Domain-aware expression translation.

Return type:

ExprDomain

Example:

>>> import z3
>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> # Runtime-definedness stays separate from the Z3 value expression.
>>> expr = BinaryOp(x=Variable("x"), op="/", y=Integer(3))
>>> result = translate_expr_domain(expr, {"x": z3.Int("x")})
>>> result.failure is None
True
>>> bool(result.definedness_constraints)
True

merge_definedness_constraints

pyfcstm.solver.domain.merge_definedness_constraints(*items) → Tuple[DomainConstraint, ...][source]

Flatten expression-domain and domain-constraint inputs in order.

Each returned constraint must hold at the evaluation point. The helper does not run a solver and does not remove contradictory constraints.

Parameters:

items (object) – Domain constraints, ExprDomain objects, or iterables of domain constraints to flatten.

Returns:

Domain constraints in source order.

Return type:

Tuple[DomainConstraint, …]

Raises:

TypeError – If any item is not a supported domain-constraint shape.

Example:

>>> import z3
>>> # Flattening preserves the exact constraint object supplied.
>>> item = DomainConstraint(z3.Int("x") != 0)
>>> merge_definedness_constraints(item) == (item,)
True