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

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

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