pyfcstm.solver.expr

Expression conversion utilities for Z3 solver integration.

This module provides functions to convert pyfcstm expression objects into Z3 solver expressions, enabling constraint solving and symbolic execution. It supports all expression types including literals, variables, operators, and mathematical functions.

The module contains the following main components:

Example:

>>> from pyfcstm.model.expr import Variable, Integer, BinaryOp
>>> from pyfcstm.solver.expr import expr_to_z3, create_z3_vars_from_models
>>> from pyfcstm.model.model import VarDefine
>>> import z3
>>>
>>> # Create variable definitions
>>> var_defs = [
...     VarDefine(name='x', type='int', init=Integer(0)),
...     VarDefine(name='y', type='float', init=Float(0.0))
... ]
>>>
>>> # Create Z3 variables
>>> z3_vars = create_z3_vars_from_models(var_defs)
>>>
>>> # Convert expression to Z3
>>> expr = BinaryOp(x=Variable('x'), op='+', y=Integer(5))
>>> z3_expr = expr_to_z3(expr, z3_vars)

expr_to_z3

pyfcstm.solver.expr.expr_to_z3(expr: Expr, z3_vars: Dict[str, ArithRef | BoolRef]) → ArithRef | BoolRef[source]

Convert a pyfcstm expression to a Z3 solver expression.

This function recursively converts pyfcstm expression objects into equivalent Z3 expressions. It supports literals, variables, arithmetic operators, bitwise operators, logical operators, conditional expressions, and mathematical functions.

Parameters:

  • expr (Expr) – The pyfcstm expression to convert

  • z3_vars (Dict[str, Union[z3.ArithRef, z3.BoolRef]]) – Dictionary mapping variable names to Z3 expression objects

Returns:

The equivalent Z3 expression

Return type:

Union[z3.ArithRef, z3.BoolRef]

Raises:

  • ValueError – If the expression type is unsupported or variable is not found

  • NotImplementedError – If a mathematical function is not supported

Example:

>>> import z3
>>> from pyfcstm.model.expr import Variable, Integer, BinaryOp
>>> z3_vars = {'x': z3.Int('x')}
>>> expr = BinaryOp(x=Variable('x'), op='+', y=Integer(5))
>>> z3_expr = expr_to_z3(expr, z3_vars)
>>> solver = z3.Solver()
>>> solver.add(z3_expr == 10)
>>> solver.check()
sat
>>> solver.model()[z3_vars['x']]
5

create_z3_vars_from_models

pyfcstm.solver.expr.create_z3_vars_from_models(models: StateMachine | VarDefine | List[VarDefine]) → Dict[str, ArithRef | BoolRef][source]

Create a dictionary of Z3 variables from model objects.

This function creates Z3 variables from various model input types: - StateMachine: extracts variables from the state machine - VarDefine: creates a single Z3 variable - List[VarDefine]: creates Z3 variables for all definitions in the list

Integer types map to Z3 Int, float types map to Z3 Real.

Parameters:

models (Union[StateMachine, VarDefine, List[VarDefine]]) – Model object(s) containing variable definitions

Returns:

Dictionary mapping variable names to Z3 expression objects

Return type:

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

Raises:

  • ValueError – If a variable type is unsupported

  • TypeError – If the input type is not supported

Example:

>>> from pyfcstm.model.model import VarDefine, StateMachine, State
>>> from pyfcstm.model.expr import Integer, Float
>>>
>>> # From a list of VarDefine
>>> var_defs = [
...     VarDefine(name='counter', type='int', init=Integer(0)),
...     VarDefine(name='temperature', type='float', init=Float(25.0))
... ]
>>> z3_vars = create_z3_vars_from_models(var_defs)
>>> 'counter' in z3_vars
True
>>>
>>> # From a single VarDefine
>>> single_var = VarDefine(name='x', type='int', init=Integer(0))
>>> z3_vars = create_z3_vars_from_models(single_var)
>>> 'x' in z3_vars
True
>>>
>>> # From a StateMachine
>>> root_state = State(name='System', parent=None, is_pseudo=False,
...                    display_name=None, comment=None)
>>> sm = StateMachine(variables=var_defs, root_state=root_state, global_events=[])
>>> z3_vars = create_z3_vars_from_models(sm)
>>> 'counter' in z3_vars
True