pyfcstm.verify.encoding._core

SMT-local verification encoding helpers for FCSTM models.

Raw verify algorithms are full-power by default: they do not consult pyfcstm.solver.safety or diagnostics/inspect policy gates, and smt_timeout_ms=None leaves the underlying solver timeout unset. Callers that need product-level limits can pass optional budgets or apply policy in an adapter layer.

The functions intentionally return lightweight dictionaries instead of ModelDiagnostic objects so the raw verification layer stays independent from diagnostics presentation concerns.

Example:

>>> from pyfcstm.dsl.parse import parse_with_grammar_entry
>>> from pyfcstm.model import parse_dsl_node_to_state_machine
>>> from pyfcstm.verify.encoding._core import _z3_vars
>>> code = "def int x = 0; state Root { state A; [*] -> A; }"
>>> machine = parse_dsl_node_to_state_machine(
...     parse_with_grammar_entry(code, "state_machine_dsl")
... )
>>> sorted(_z3_vars(tuple(machine.defines.values())))
['x']

is_sat

pyfcstm.verify.encoding._core.is_sat = <function is_sat>

Check whether an iterable of Z3 constraints is satisfiable.

Parameters:

• constraints (Iterable[z3.ExprRef]) – Constraints to add to a fresh Z3 solver.

• timeout_ms (Optional[int], optional) – Optional value forwarded unchanged to Z3’s timeout parameter. None means the helper does not configure a solver timeout. Values rejected by Z3 propagate as Z3 errors; callers that need a finite positive budget must validate it before calling, defaults to None.

• get_model (bool, optional) – Whether to return a model when the constraints are satisfiable, defaults to False.

Returns:

Satisfiability result.

Return type:

SatResult

Example:

>>> import z3
>>> x = z3.Int('x')
>>> is_sat([x == 1], timeout_ms=1000).kind
'sat'