{"id":8520,"library":"pysmt","title":"PySMT: A Solver-Agnostic Library for SMT Formulae Manipulation and Solving","description":"PySMT is a Python library designed for solver-agnostic manipulation and solving of Satisfiability Modulo Theories (SMT) formulae. It provides a unified API to define, manipulate, and solve SMT problems using various SMT-LIB compliant solvers. The library is actively maintained, with regular releases, and its current stable version is 0.9.6.","status":"active","version":"0.9.6","language":"en","source_language":"en","source_url":"https://github.com/pysmt/pysmt","tags":["SMT","solver","logic","formal verification","satisfiability modulo theories","math"],"install":[{"cmd":"pip install pysmt","lang":"bash","label":"Basic installation"},{"cmd":"python -m pysmt install --z3","lang":"bash","label":"Install with Z3 solver (recommended for functionality)"}],"dependencies":[{"reason":"Optional, for efficient multi-precision number handling. Defaults to Python's fractions module if not installed.","package":"gmpy2","optional":true},{"reason":"Optional, used to improve performance of some internal components, e.g., SMT-LIB parser.","package":"Cython","optional":true}],"imports":[{"note":"The `pysmt.shortcuts` module provides the most commonly used functions and operators for formula construction and solving.","symbol":"Symbol, And, Not, is_sat","correct":"from pysmt.shortcuts import Symbol, And, Not, is_sat"},{"note":"Data types for SMT variables (symbols) are defined in `pysmt.typing`.","symbol":"INT, BOOL","correct":"from pysmt.typing import INT, BOOL"},{"note":"For incremental solving or explicit solver control, use the `Solver` class from `shortcuts`.","symbol":"Solver","correct":"from pysmt.shortcuts import Solver"}],"quickstart":{"code":"from pysmt.shortcuts import Symbol, And, Not, is_sat, Solver\nfrom pysmt.typing import BOOL\n\n# Define Boolean symbols\nvarA = Symbol(\"A\", BOOL)\nvarB = Symbol(\"B\", BOOL)\n\n# Construct a formula: (A AND (NOT B))\nf = And([varA, Not(varB)])\n\n# Check satisfiability using a shortcut\nres_f = is_sat(f)\nprint(f\"Formula '{f}' is SAT? {res_f}\")\n\n# Perform a substitution: replace B with A in f, resulting in (A AND (NOT A))\ng = f.substitute({varB: varA})\nres_g = is_sat(g)\nprint(f\"Formula '{g}' is SAT? {res_g}\")\n\n# Example with explicit solver and model extraction\nwith Solver(name=\"z3\", suppress_warnings=True) as solver:\n    solver.add_assertion(f)\n    if solver.solve():\n        print(f\"Model for '{f}':\")\n        for s in [varA, varB]:\n            print(f\"  {s} = {solver.get_value(s)}\")\n    else:\n        print(f\"'{f}' is UNSAT\")\n","lang":"python","description":"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."},"warnings":[{"fix":"Upgrade to Python 3.5+ (recommended) or higher. For Python 2.7, use PySMT <0.9.0.","message":"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.","severity":"breaking","affected_versions":">=0.9.0"},{"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.","message":"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)`).","severity":"gotcha","affected_versions":"All versions"},{"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.","message":"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.","severity":"gotcha","affected_versions":"All versions"},{"fix":"Update imports and references to use `pysmt.constants.Fraction` (or `Integer`, `Numerals`) instead of previous locations like `pysmt.numeral` or `pysmt.utils`.","message":"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.","severity":"breaking","affected_versions":">=0.6.0"},{"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.","message":"The methods `Solver.declare_variable` and `Solver.set_options` were removed in PySMT version 0.9.5.","severity":"deprecated","affected_versions":">=0.9.5"}],"env_vars":null,"last_verified":"2026-04-16T00:00:00.000Z","next_check":"2026-07-15T00:00:00.000Z","problems":[{"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`.","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.","error":"pysmt.exceptions.NoSolverAvailableError: No Solver is available"},{"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.","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.","error":"TypeError: unsupported operand type(s) for &: 'FNode' and 'bool'"},{"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`.","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.","error":"Solver installed, but `pysmt-install --check` or `is_sat()` still reports it as unavailable."}]}