pyfcstm.solver.solve

Constraint solving utilities for Z3 expressions.

This module provides high-level functions for solving Z3 constraint expressions with flexible solution enumeration. It supports single solutions, multiple solutions, and exhaustive solution enumeration with optimized solving strategies.

The module contains the following main components:

  • SolveResult - Dataclass containing solve results with status and solutions

  • solve() - Main solving function with flexible solution enumeration

Example:

>>> import z3
>>> from pyfcstm.solver.solve import solve
>>>
>>> # Create variables and constraints
>>> x = z3.Int('x')
>>> y = z3.Int('y')
>>> constraints = [x + y == 10, x > 0, y > 0]
>>>
>>> # Get 5 solutions
>>> result = solve(constraints, max_solutions=5)
>>> result.status
'sat'
>>> len(result.solutions)
5
>>>
>>> # Get all solutions (WARNING: use with caution!)
>>> result = solve(constraints, max_solutions=None)
>>>
>>> # Get single solution (fastest)
>>> result = solve(constraints, max_solutions=1)

SolveResult

class pyfcstm.solver.solve.SolveResult(status: Literal['sat', 'unsat', 'unknown'], solutions: List[Dict[str, int | float]], variables: List[str])[source]

Result of a constraint solving operation.

Contains the solving status, list of solutions, and the list of variables that were solved for. Each solution is a dictionary mapping variable names to their concrete values (int or float).

This dataclass is immutable (frozen) to ensure result integrity.

Parameters:

  • status (Literal['sat', 'unsat', 'unknown']) – Solving status - ‘sat’ (satisfiable), ‘unsat’ (unsatisfiable), or ‘unknown’ (solver could not determine)

  • solutions (List[Dict[str, Union[int, float]]]) – List of solution dictionaries, each mapping variable names to their values. Empty if status is ‘unsat’ or ‘unknown’.

  • variables (List[str]) – List of variable names that were solved for

Example:

>>> result = SolveResult(
...     status='sat',
...     solutions=[{'x': 1, 'y': 9}, {'x': 2, 'y': 8}],
...     variables=['x', 'y']
... )
>>> result.status
'sat'
>>> len(result.solutions)
2
>>> print(result)
SolveResult(sat, 2 solutions, variables=['x', 'y'])
__repr__() → str[source]

Return a comprehensive string representation of the solve result.

The representation adapts based on the number of solutions: - For small solution counts (≤3): shows all solutions - For medium counts (4-10): shows first 2 and last 1 with ellipsis - For large counts (>10): shows summary with count only

Returns:

String representation of the result

Return type:

str

Example:

>>> # Unsatisfiable
>>> result = SolveResult('unsat', [], ['x', 'y'])
>>> repr(result)
"SolveResult(unsat, 0 solutions, variables=['x', 'y'])"
>>>
>>> # Few solutions
>>> result = SolveResult('sat', [{'x': 1}, {'x': 2}], ['x'])
>>> repr(result)
"SolveResult(sat, 2 solutions, variables=['x'], solutions=[{'x': 1}, {'x': 2}])"
>>>
>>> # Many solutions
>>> result = SolveResult('sat', [{'x': i} for i in range(100)], ['x'])
>>> repr(result)
"SolveResult(sat, 100 solutions, variables=['x'])"

solve

pyfcstm.solver.solve.solve(constraints: ExprRef | List[ExprRef], max_solutions: int | None = 10, timeout: int | None = None, warn_threshold: int = 1000) → SolveResult[source]

Solve Z3 constraint expressions and return solutions.

This function solves constraint expressions using Z3 and returns a specified number of solutions. It supports three solving modes:

  • max_solutions=1: Returns a single solution (fastest, uses simple check)

  • max_solutions=N: Returns up to N solutions (uses iterative blocking)

  • max_solutions=None: Returns all solutions (WARNING: may be very slow or infinite)

The function automatically extracts all variables from the constraints and handles cases where some variables are unconstrained (don’t care values). For unconstrained variables, the solver picks arbitrary valid values.

WARNING: Using max_solutions=None can be dangerous for underconstrained systems. The solver will attempt to enumerate all solutions, which may:

  • Take an extremely long time for systems with many solutions

  • Consume excessive memory

  • Never terminate for infinite solution spaces

When max_solutions=None and the number of solutions exceeds warn_threshold, a warning will be issued to alert you of potential performance issues.

Parameters:

  • constraints (Union[z3.ExprRef, List[z3.ExprRef]]) – Single Z3 expression or list of Z3 expressions to solve

  • max_solutions (Optional[int], optional) – Maximum number of solutions to find. Use 1 for single solution, positive integer for specific count, or None for all solutions (use with caution). Defaults to 10.

  • timeout (Optional[int], optional) – Solver timeout in milliseconds. None means no timeout. Defaults to None.

  • warn_threshold (int, optional) – When max_solutions=None, issue a warning if the number of solutions exceeds this threshold. Defaults to 1000.

Returns:

Solve result containing status, solutions, and variable list

Return type:

SolveResult

Raises:

  • ValueError – If max_solutions is less than 1 (when not None)

  • ValueError – If warn_threshold is less than 1

Example:

>>> import z3
>>> x = z3.Int('x')
>>> y = z3.Int('y')
>>>
>>> # Single solution (fastest)
>>> result = solve([x + y == 10, x > 0], max_solutions=1)
>>> result.status
'sat'
>>> len(result.solutions)
1
>>>
>>> # Multiple solutions
>>> result = solve([x + y == 10, x > 0, x < 5], max_solutions=5)
>>> len(result.solutions)
4
>>>
>>> # All solutions (WARNING: use with caution!)
>>> result = solve([x + y == 10, x > 0, x < 3], max_solutions=None)
>>>
>>> # Unconstrained variable handling
>>> z = z3.Int('z')
>>> result = solve([x == 5], max_solutions=1)
>>> 'x' in result.solutions[0]
True