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:

expr_to_z3() - Convert a pyfcstm model expression to a Z3 expression
create_z3_vars_from_models() - Create Z3 variables from model objects

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)

python_round_to_z3

pyfcstm.solver.expr.python_round_to_z3(operand: ArithRef | BoolRef) → ArithRef[source]

Return a Z3 expression matching Python single-argument round.

Python rounds half-way cases to the nearest even integer. Keeping this helper in the shared solver layer prevents raw verify algorithms from drifting away from runtime expression semantics.

Parameters:: operand (Union[z3.ArithRef, z3.BoolRef]) – Integer or real Z3 operand.
Returns:: Rounded integer expression.
Return type:: z3.ArithRef

Example:

>>> import z3
>>> x = z3.Real("x")
>>> rounded = python_round_to_z3(x)
>>> solver = z3.Solver()
>>> solver.add(x == z3.RealVal("2.5"), rounded != 2)
>>> solver.check()
unsat

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 (pyfcstm.model.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.dsl import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> from pyfcstm.model.model import VarDefine
>>> 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 parsed through the public DSL pipeline.
>>> source = '''
... def int counter = 0;
... state System;
... '''
>>> ast = parse_with_grammar_entry(source, "state_machine_dsl")
>>> machine = parse_dsl_node_to_state_machine(ast)
>>> z3_vars = create_z3_vars_from_models(machine)
>>> 'counter' in z3_vars
True