pyfcstm.solver.operation

Operation parsing and execution utilities for Z3 solver integration.

This module provides functions to parse DSL operation code strings into Operation objects and execute operations on Z3 variable dictionaries.

The module contains the following main components:

Example:

>>> from pyfcstm.solver.operation import parse_operations, execute_operations
>>> import z3
>>>
>>> # Parse operations 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, z3_vars)
>>> # 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[Operation][source]

Parse DSL operation code string into a list of Operation objects.

This function parses a DSL code string containing operation statements (variable assignments) and converts them into Operation objects. It can optionally validate that only allowed variables are used.

Parameters:

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

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

Returns:

List of parsed Operation objects

Return type:

List[Operation]

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 unknown variables
>>> ops = parse_operations("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: Operation | List[Operation], var_exprs: Dict[str, ArithRef | BoolRef]) → Dict[str, ArithRef | BoolRef][source]

Execute operations on a Z3 variable expression dictionary.

This function takes a list of operations and executes them sequentially on a variable expression dictionary. Each operation updates the state by assigning a new Z3 expression to a variable. The operations are executed in order, so later operations can reference the results of earlier operations.

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

Parameters:

  • operations (Union[Operation, List[Operation]]) – Single operation or list of operations 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 Z3 expressions

Return type:

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

Raises:

ValueError – If a variable referenced in an expression is not in var_exprs

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