pyfcstm.solver

Z3 solver integration for pyfcstm expressions.

This module provides utilities for converting pyfcstm expression objects to Z3 solver expressions, enabling constraint solving and symbolic execution capabilities for state machine models.

The module contains the following main components:

  • expr_to_z3() - Convert pyfcstm expressions to Z3 expressions

  • create_z3_vars_from_models() - Create Z3 variables from model objects

  • solve() - Solve Z3 constraint expressions with flexible solution enumeration

  • SolveResult - Dataclass containing solve results

  • parse_operations() - Parse DSL operation code string to list of Operations

  • execute_operations() - Execute operations on Z3 variable expression dictionary (symbolic execution)

Example:

>>> from pyfcstm.solver import expr_to_z3, create_z3_vars_from_models, solve
>>> from pyfcstm.model.expr import Variable, Integer, BinaryOp
>>> import z3
>>>
>>> # Create Z3 variables
>>> z3_vars = {'x': z3.Int('x'), 'y': z3.Int('y')}
>>>
>>> # Convert expression to Z3
>>> expr = BinaryOp(x=Variable('x'), op='+', y=Integer(5))
>>> z3_expr = expr_to_z3(expr, z3_vars)
>>>
>>> # Solve constraints
>>> result = solve([z3_expr == 10, z3_vars['y'] > 0], max_solutions=5)
>>> result.status
'sat'
>>>
>>> # Parse and execute operations symbolically
>>> from pyfcstm.solver import parse_operations, execute_operations
>>> ops = parse_operations("x = x + 2; y = y + x;", allowed_vars=['x', 'y'])
>>> x, y = z3.Int('x'), z3.Int('y')
>>> var_exprs = {'x': x, 'y': y}
>>> new_exprs = execute_operations(ops, var_exprs)
>>> # new_exprs['x'] is: x + 2
>>> # new_exprs['y'] is: y + (x + 2)