PySMT: A Solver-Agnostic Library for SMT Formulae Manipulation and Solving

Common errors

• pysmt.exceptions.NoSolverAvailableError: No Solver is available

  cause This error occurs when PySMT attempts to perform a solving operation (e.g., `is_sat()`, `Solver().solve()`) but cannot find an installed and accessible SMT solver. This could be because no solver was installed, or its Python bindings are not correctly configured.
  fix Install a solver using `python -m pysmt install --<solver-name>` (e.g., `python -m pysmt install --z3`). Verify installation with `pysmt-install --check`. If the solver was installed manually or in a non-standard location, ensure its Python bindings directory is added to your `PYTHONPATH`.

• TypeError: unsupported operand type(s) for &: 'FNode' and 'bool'

  cause This typically happens when mixing PySMT's infix operators (which expect `FNode` objects on both sides) with standard Python boolean literals or expressions without explicit conversion. For example, `f & True` might raise this if `True` isn't wrapped as a PySMT Boolean constant.
  fix Ensure all operands in SMT expressions are `FNode` objects. For Python boolean literals, use `Bool(True)` or `Bool(False)` from `pysmt.shortcuts`. Better yet, use explicit logical operators like `And()`, `Or()`, `Not()` to avoid ambiguity and improve clarity.

• Solver installed, but `pysmt-install --check` or `is_sat()` still reports it as unavailable.

  cause Even if `pysmt-install --<solver-name>` completes without errors, the Python bindings for the solver might not be correctly located by PySMT, particularly if they are installed in a non-default location or if the `PYTHONPATH` environment variable is not properly configured.
  fix After running `python -m pysmt install`, check the output for the location of the installed bindings. If they are not in a standard `site-packages` directory, you might need to manually add the path to your `PYTHONPATH` environment variable. For example, `export PYTHONPATH=$HOME/.smt_solvers/python_bindings:$PYTHONPATH`.

Warnings

• breaking Python 2.7 support was officially dropped in PySMT version 0.9.0. Versions 0.9.0 and later only support Python 3+. The last release to support Python 2.7 was 0.8.0.
  Fix: Upgrade to Python 3.5+ (recommended) or higher. For Python 2.7, use PySMT <0.9.0.
• gotcha When `pysmt.shortcuts` is imported, infix notation (e.g., `a & b`) is enabled by default. While convenient for quick experimentation, it can make complex code less clear by blurring the line between Python and SMT operators. For clarity, prefer explicit textual operators (e.g., `And(a, b)`).
  Fix: Import specific textual operators from `pysmt.shortcuts` (e.g., `from pysmt.shortcuts import And, Or, Not`) and use them directly for better code readability and to avoid unexpected operator precedence issues.
• gotcha SMT solvers are not direct Python dependencies of PySMT. While `pip install pysmt` installs the library, you need to explicitly install at least one solver (e.g., Z3, MathSAT) using `python -m pysmt install --<solver-name>` to perform actual solving. Solvers need to have their Python bindings accessible, potentially requiring `PYTHONPATH` adjustments for custom installations.
  Fix: Run `python -m pysmt install --<solver-name>` (e.g., `python -m pysmt install --z3`) to install a solver. If issues persist, check `pysmt-install --check` and ensure your `PYTHONPATH` includes the solver bindings directory, especially for non-standard installations.
• breaking The classes `Integer`, `Fraction`, and `Numerals` were moved to `pysmt.constants` in version 0.6.0. Methods from `pysmt.utils` also moved to `pysmt.constants`. The `pysmt.numeral` module was removed.
  Fix: Update imports and references to use `pysmt.constants.Fraction` (or `Integer`, `Numerals`) instead of previous locations like `pysmt.numeral` or `pysmt.utils`.
• deprecated The methods `Solver.declare_variable` and `Solver.set_options` were removed in PySMT version 0.9.5.
  Fix: Remove calls to `Solver.declare_variable` as variables are typically declared via `Symbol()` and added to the solver with `add_assertion()`. For solver options, consult the documentation for solver-specific configuration or use the `Solver` constructor's `options` argument if available.

Install

• pip install pysmt Basic installation
• python -m pysmt install --z3 Install with Z3 solver (recommended for functionality)

Imports

• Symbol, And, Not, is_sat

  from pysmt.shortcuts import Symbol, And, Not, is_sat

  The `pysmt.shortcuts` module provides the most commonly used functions and operators for formula construction and solving.
• INT, BOOL

  from pysmt.typing import INT, BOOL

  Data types for SMT variables (symbols) are defined in `pysmt.typing`.
• Solver

  from pysmt.shortcuts import Solver

  For incremental solving or explicit solver control, use the `Solver` class from `shortcuts`.

Quickstart

This quickstart demonstrates defining Boolean SMT variables, constructing a logical formula, checking its satisfiability using a shortcut, performing variable substitution, and using an explicit solver to extract a model.

from pysmt.shortcuts import Symbol, And, Not, is_sat, Solver
from pysmt.typing import BOOL

# Define Boolean symbols
varA = Symbol("A", BOOL)
varB = Symbol("B", BOOL)

# Construct a formula: (A AND (NOT B))
f = And([varA, Not(varB)])

# Check satisfiability using a shortcut
res_f = is_sat(f)
print(f"Formula '{f}' is SAT? {res_f}")

# Perform a substitution: replace B with A in f, resulting in (A AND (NOT A))
g = f.substitute({varB: varA})
res_g = is_sat(g)
print(f"Formula '{g}' is SAT? {res_g}")

# Example with explicit solver and model extraction
with Solver(name="z3", suppress_warnings=True) as solver:
    solver.add_assertion(f)
    if solver.solve():
        print(f"Model for '{f}':")
        for s in [varA, varB]:
            print(f"  {s} = {solver.get_value(s)}")
    else:
        print(f"'{f}' is UNSAT")