pyfcstm.solver.logical

Small logical predicates around Z3 solver checks.

This module provides thin wrappers for satisfiability, validity, and overlap queries needed by the verify algorithms. The wrappers keep the result shape small so callers can handle unknown and timeout without parsing Z3-specific status objects.

The helpers treat timeout_ms=None as the no-timeout path and do not configure Z3’s timeout parameter in that case. Any non-None value is forwarded to Z3 unchanged. Callers that need a bounded resource policy must validate their own budget before calling these infrastructure helpers.

Example:

>>> import z3
>>> x = z3.Int("x")
>>> is_sat([x == 1]).kind
'sat'
>>> is_valid(x == x).kind
'sat'

SatResult

class pyfcstm.solver.logical.SatResult(kind: Literal['sat', 'unsat', 'unknown', 'timeout'], model: ModelRef | None = None)[source]

Result returned by solver logical helpers.

Parameters:

kind (Literal['sat', 'unsat', 'unknown', 'timeout']) – Solver outcome. 'sat' and 'unsat' keep their normal satisfiability meaning for is_sat() and is_overlap(); for is_valid(), 'sat' means the input formula is valid and 'unsat' means it is not valid.
model (Optional[z3.ModelRef], optional) – Z3 model for satisfiable is_sat() calls when explicitly requested, defaults to None.

Example:

>>> result = SatResult(kind="unsat")
>>> result.kind
'unsat'
>>> result.model is None
True

is_sat

pyfcstm.solver.logical.is_sat(constraints: Iterable[ExprRef], *, timeout_ms: int | None = None, get_model: bool = False) → SatResult[source]

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'

is_valid

pyfcstm.solver.logical.is_valid(formula: ExprRef, *, timeout_ms: int | None = None) → SatResult[source]

Check whether a Z3 formula is valid.

The helper checks the satisfiability of Not(formula). The result kind is flipped for definite outcomes: 'sat' means the original formula is valid, and 'unsat' means the original formula is not valid. unknown and timeout are propagated unchanged.

Parameters:

formula (z3.ExprRef) – Formula to prove valid.
timeout_ms (Optional[int], optional) – Optional value forwarded through is_sat(). None means no solver timeout is configured, defaults to None.

Returns:

Validity result.

Return type:

SatResult

Example:

>>> import z3
>>> x = z3.Int("x")
>>> is_valid(x == x).kind
'sat'
>>> is_valid(x > 0).kind
'unsat'

is_overlap

pyfcstm.solver.logical.is_overlap(formula_a: ExprRef, formula_b: ExprRef, *, timeout_ms: int | None = None) → SatResult[source]

Check whether two formulas can hold at the same time.

Parameters:

formula_a (z3.ExprRef) – First formula.
formula_b (z3.ExprRef) – Second formula.
timeout_ms (Optional[int], optional) – Optional value forwarded through is_sat(). None means no solver timeout is configured, defaults to None.

Returns:

'sat' if the formulas overlap, 'unsat' if they are disjoint, or an indeterminate solver result.

Return type:

SatResult

Example:

>>> import z3
>>> x = z3.Int("x")
>>> is_overlap(x > 0, x < 2).kind
'sat'
>>> is_overlap(x > 0, x < 0).kind
'unsat'