pyfcstm.solver.operation

Operation parsing and execution utilities for Z3 solver integration.

This module provides functions to parse DSL operation code strings into operation statements and execute them on Z3 variable dictionaries.

The module contains the following main components:

Example:

>>> from pyfcstm.solver.operation import parse_operations, execute_operations
>>> import z3
>>>
>>> # Parse operation statements from DSL string
>>> ops = parse_operations("x = x + 1; y = x * 2;", allowed_vars=['x', 'y'])
>>>
>>> # Execute operations on Z3 variables
>>> z3_vars = {'x': z3.Int('x'), 'y': z3.Int('y')}
>>> z3_state = {'x': z3.IntVal(5), 'y': z3.IntVal(0)}
>>> new_state = execute_operations(ops, z3_state)
>>> # new_state['x'] represents the Z3 expression: 5 + 1
>>> # new_state['y'] represents the Z3 expression: (5 + 1) * 2

OperationSource

pyfcstm.solver.operation.OperationSource = <class 'pyfcstm.solver.domain.DomainSource'>

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'

__all__

pyfcstm.solver.operation.__all__ = ['OperationBranch', 'OperationExecution', 'OperationFailure', 'OperationSource', 'OperationStep', 'execute_operations', 'execute_operations_domain', 'merge_operation_definedness', 'parse_operations']

Built-in mutable sequence.

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

OperationFailure

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

Pure solver-layer operation execution failure.

Parameters:

  • kind (str) – Normalized failure kind.

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

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

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

Example:

>>> failure = OperationFailure("value_error", "bad operation")
>>> failure.kind
'value_error'

OperationStep

class pyfcstm.solver.operation.OperationStep(source: DomainSource | None, before: Mapping[str, ArithRef | BoolRef], after: Mapping[str, ArithRef | BoolRef], path_conditions: Tuple[ExprRef, ...] = (), definedness_constraints: Tuple[DomainConstraint, ...] = ())[source]

One successful assignment step in a domain-aware operation execution.

Parameters:

  • source (Optional[DomainSource]) – Optional source metadata for the assignment.

  • before (Mapping[str, Union[z3.ArithRef, z3.BoolRef]]) – Symbolic environment before the assignment.

  • after (Mapping[str, Union[z3.ArithRef, z3.BoolRef]]) – Symbolic environment after the assignment.

  • path_conditions (Tuple[z3.ExprRef, ...], optional) – Predicates that must hold before this assignment, defaults to ().

  • definedness_constraints (Tuple[DomainConstraint, ...], optional) – Runtime-definedness constraints introduced by this assignment, defaults to ().

Example:

>>> import z3
>>> step = OperationStep(None, {"x": z3.Int("x")}, {"x": z3.IntVal(1)})
>>> step.after["x"]
1

OperationBranch

class pyfcstm.solver.operation.OperationBranch(branch_id: str | None, branch_kind: str, selector: ExprRef, path_conditions: Tuple[ExprRef, ...] = (), status: str = 'sat', result_env: Mapping[str, ArithRef | BoolRef] | None = None, definedness_constraints: Tuple[DomainConstraint, ...] = (), failure: OperationFailure | None = None)[source]

One source branch in a domain-aware operation execution.

Parameters:

  • branch_id (Optional[str]) – Stable branch identifier within the local if block.

  • branch_kind (str) – Branch kind: "if", "elif", or "else".

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

  • path_conditions (Tuple[z3.ExprRef, ...], optional) – Predicates needed to reach the branch, defaults to ().

  • status (str, optional) – Branch reachability status, defaults to "sat".

  • result_env (Optional[Mapping[str, Union[z3.ArithRef, z3.BoolRef]]], optional) – Branch-local result environment, defaults to None.

  • definedness_constraints (Tuple[DomainConstraint, ...], optional) – Runtime-definedness constraints introduced by this branch, defaults to ().

  • failure (Optional[OperationFailure], optional) – Branch-local operation failure, defaults to None.

Example:

>>> import z3
>>> branch = OperationBranch("0", "if", z3.Bool("cond"))
>>> branch.branch_kind
'if'
__post_init__() → None[source]

Validate branch invariants after dataclass initialization.

Returns:

None.

Return type:

None

Raises:

ValueError – If the branch kind, status, or unreachable-branch payload is inconsistent.

Example:

>>> import z3
>>> OperationBranch("0", "if", z3.Bool("c")).status
'sat'

OperationExecution

class pyfcstm.solver.operation.OperationExecution(env: Mapping[str, ArithRef | BoolRef], visible_names: Tuple[str, ...], expr_constraints: Tuple[ExprRef, ...] = (), definedness_constraints: Tuple[DomainConstraint, ...] = (), steps: Tuple[OperationStep, ...] = (), branches: Tuple[OperationBranch, ...] = (), failure: OperationFailure | None = None)[source]

Domain-aware operation block execution result.

The result keeps the final visible environment separate from evidence about steps, branches, and runtime-definedness side conditions. Temporary names created inside a block can appear in internal steps, but env exposes only names visible before execution started.

Parameters:

  • env (Mapping[str, Union[z3.ArithRef, z3.BoolRef]]) – Final visible symbolic environment.

  • visible_names (Tuple[str, ...]) – Names preserved in the public final environment.

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

  • definedness_constraints (Tuple[DomainConstraint, ...], optional) – Runtime-definedness constraints collected during execution, defaults to ().

  • steps (Tuple[OperationStep, ...], optional) – Assignment-step evidence, defaults to ().

  • branches (Tuple[OperationBranch, ...], optional) – Branch reachability evidence, defaults to ().

  • failure (Optional[OperationFailure], optional) – Expected execution failure, defaults to None.

Example:

>>> import z3
>>> result = OperationExecution({"x": z3.IntVal(1)}, ("x",))
>>> result.visible_names
('x',)

parse_operations

pyfcstm.solver.operation.parse_operations(code: str, allowed_vars: List[str] | None = None) → List[OperationStatement][source]

Parse DSL operation code string into a list of operation statements.

This function parses a DSL code string containing operation statements (assignments and if blocks) and converts them into model-layer operation statements. It can optionally validate that expressions only reference variables that are already available at that point in the block. Unknown assignment targets are treated as block-local temporary variables.

Parameters:

  • code (str) – DSL operation code string to parse

  • allowed_vars (Optional[List[str]]) – List of initially available variable names, or None for free mode

Returns:

List of parsed operation statements

Return type:

List[OperationStatement]

Raises:

Example:

>>> ops = parse_operations("x = x + 1; y = 10;", allowed_vars=['x', 'y'])
>>> len(ops)
2
>>> ops[0].var_name
'x'

>>> # Free mode - no variable restrictions
>>> ops = parse_operations("a = b + c;", allowed_vars=None)

>>> # Restricted mode - raises ValueError for variables used before assignment
>>> ops = parse_operations("y = z + 1; z = 1;", allowed_vars=['x', 'y'])
Traceback (most recent call last):
    ...
ValueError: Variable 'z' is not in allowed variables: ['x', 'y']

execute_operations_domain

pyfcstm.solver.operation.execute_operations_domain(operations: OperationStatement | List[OperationStatement], var_exprs: Dict[str, ArithRef | BoolRef], *, assumptions: Sequence[ExprRef] = (), path_conditions: Sequence[ExprRef] = (), source: DomainSource | None = None, prune_unreachable: bool = True, timeout_ms: int | None = None) → OperationExecution[source]

Execute operation statements with runtime-definedness metadata.

This path-sensitive executor preserves legacy symbolic assignment behavior while also returning branch evidence and constraints needed for FCSTM runtime-definedness. The returned environment contains only variables that were visible before execution started; block-local temporaries stay internal.

Parameters:

  • operations (Union[OperationStatement, List[OperationStatement]]) – Single operation statement or statement list.

  • var_exprs (Dict[str, Union[z3.ArithRef, z3.BoolRef]]) – Starting symbolic environment.

  • assumptions (Sequence[z3.ExprRef], optional) – Caller-known facts added to reachability checks, defaults to ().

  • path_conditions (Sequence[z3.ExprRef], optional) – Predicates needed to reach this block, defaults to ().

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

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

  • timeout_ms (Optional[int], optional) – Optional solver timeout in milliseconds.

Returns:

Domain-aware operation execution result.

Return type:

OperationExecution

Example:

>>> import z3
>>> ops = parse_operations("x = x + 1;", allowed_vars=["x"])
>>> result = execute_operations_domain(ops, {"x": z3.Int("x")})
>>> result.failure is None
True
>>> len(result.steps)
1

merge_operation_definedness

pyfcstm.solver.operation.merge_operation_definedness(*items) → Tuple[DomainConstraint, ...][source]

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

Parameters:

items (object) – Domain constraints, operation execution objects, operation steps, operation branches, or iterables of those objects.

Returns:

Flattened runtime-definedness constraints.

Return type:

Tuple[DomainConstraint, …]

Raises:

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

Example:

>>> import z3
>>> item = DomainConstraint(z3.Int("x") != 0)
>>> merge_operation_definedness(item) == (item,)
True

execute_operations

pyfcstm.solver.operation.execute_operations(operations: OperationStatement | List[OperationStatement], var_exprs: Dict[str, ArithRef | BoolRef]) → Dict[str, ArithRef | BoolRef][source]

Execute operation statements on a Z3 variable expression dictionary.

This function takes one operation statement or a statement list and symbolically executes it against a variable-expression dictionary. Assignments update the current symbolic environment directly, while if blocks evaluate each branch from the same pre-if environment and then merge only the names that were already visible before entering the block. Statements are executed in order, so later statements can reference the results of earlier ones.

This performs symbolic execution - expressions are built up symbolically rather than being evaluated to concrete values.

Parameters:

  • operations (Union[OperationStatement, List[OperationStatement]]) – Single statement or list of statements to execute

  • var_exprs (Dict[str, Union[z3.ArithRef, z3.BoolRef]]) – Dictionary mapping variable names to current Z3 expressions

Returns:

New variable expression dictionary with updated global Z3 expressions

Return type:

Dict[str, Union[z3.ArithRef, z3.BoolRef]]

Raises:

ValueError – If a variable referenced in an expression is not available in the current block scope

Example:

>>> import z3
>>> from pyfcstm.model.model import Operation
>>> from pyfcstm.model.expr import Variable, Integer, BinaryOp
>>>
>>> # Create Z3 symbolic variables
>>> x = z3.Int('x')
>>> y = z3.Int('y')
>>> var_exprs = {'x': x, 'y': y}
>>>
>>> # Create operations: x = x + 2; y = y + x;
>>> op1 = Operation(var_name='x', expr=BinaryOp(x=Variable('x'), op='+', y=Integer(2)))
>>> op2 = Operation(var_name='y', expr=BinaryOp(x=Variable('y'), op='+', y=Variable('x')))
>>>
>>> # Execute operations symbolically
>>> new_exprs = execute_operations([op1, op2], var_exprs)
>>> # new_exprs['x'] is the Z3 expression: x + 2
>>> # new_exprs['y'] is the Z3 expression: y + (x + 2)
>>>
>>> # Can verify with solver
>>> solver = z3.Solver()
>>> solver.add(x == 5, y == 10)
>>> solver.add(new_exprs['x'] == 7)  # 5 + 2
>>> solver.add(new_exprs['y'] == 17)  # 10 + 7
>>> solver.check()
sat