pyfcstm.solver

Public solver helpers for Z3-backed FCSTM analysis.

The solver package is the pure symbolic layer shared by verification algorithms and future reachability/search work. It translates model expressions and operation blocks into Z3 formulas, but it does not import pyfcstm.verify, diagnostics, registries, lifecycle rules, or inspect policy. FCSTM runtime semantics that need states, transitions, declaration order, or lifecycle phases live in pyfcstm.verify.

Module map:

Module	Public entry	Purpose
`pyfcstm.solver.expr`	`expr_to_z3()`, `create_z3_vars_from_models()`	Translate expressions and declared variables into Z3 values.
`pyfcstm.solver.domain`	`translate_expr_domain()`, `merge_definedness_constraints()`	Return expression values together with runtime-definedness constraints such as non-zero divisors.
`pyfcstm.solver.operation`	`parse_operations()`, `execute_operations()`, `execute_operations_domain`	Parse and symbolically execute operation blocks, including path-sensitive execution through `if` / `elif` / `else`.
`pyfcstm.solver.logical`	`is_sat` and related query helpers	Wrap small satisfiability, validity, and overlap checks.
`pyfcstm.solver.safety`	Optional safety classifiers	Provide advisory classification for downstream policy layers; raw verification algorithms do not use it as a default gate.
`pyfcstm.solver.solve`	`solve()`, `SolveResult`	Enumerate satisfying assignments for caller-supplied constraints.

Example:

>>> import z3
>>> from pyfcstm.model.expr import BinaryOp, Integer, Variable
>>> from pyfcstm.solver import expr_to_z3, solve
>>> # The package-level imports keep the historical simple solver API.
>>> z3_vars = {"x": z3.Int("x")}
>>> expr = BinaryOp(x=Variable("x"), op="+", y=Integer(5))
>>> z3_expr = expr_to_z3(expr, z3_vars)
>>> result = solve([z3_expr == 10], max_solutions=1)
>>> result.status
'sat'
>>> result.solutions[0]["x"]
5

>>> from pyfcstm.solver.domain import translate_expr_domain
>>> # Domain-aware translation also reports runtime preconditions.
>>> div_expr = BinaryOp(x=Variable("x"), op="/", y=Integer(2))
>>> domain = translate_expr_domain(div_expr, z3_vars)
>>> domain.failure is None
True
>>> len(domain.definedness_constraints)
1

all

pyfcstm.solver.__all__ = ['SolveResult', 'create_z3_vars_from_models', 'execute_operations', 'expr_to_z3', 'parse_operations', 'solve']

Built-in mutable sequence.

If no argument is given, the constructor creates a new empty list. The argument must be an iterable if specified.

pyfcstm.solver

__all__

all