{"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.","language":"python","status":"active","last_verified":"Mon May 18","install":{"commands":["pip install pysmt"],"cli":{"name":"pysmt","version":"sh: 1: pysmt: not found"}},"imports":["from pysmt.shortcuts import Symbol, And, Not, is_sat","from pysmt.typing import INT, BOOL","from pysmt.shortcuts import Solver"],"auth":{"required":false,"env_vars":[]},"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.","tag":null,"tag_description":null,"last_tested":null,"results":[]},"compatibility":{"tag":null,"tag_description":null,"last_tested":"2026-05-18","installed_version":"0.9.6","pypi_latest":"0.9.6","is_stale":false,"summary":{"python_range":"3.10–3.9","success_rate":100,"avg_install_s":1.8,"avg_import_s":0.11,"wheel_type":"wheel"},"results":[{"runtime":"python:3.10-alpine","python_version":"3.10","os_libc":"alpine (musl)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":null,"import_time_s":0.1,"mem_mb":3.2,"disk_size":"20.6M"},{"runtime":"python:3.10-slim","python_version":"3.10","os_libc":"slim (glibc)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":1.8,"import_time_s":0.07,"mem_mb":3.2,"disk_size":"21M"},{"runtime":"python:3.11-alpine","python_version":"3.11","os_libc":"alpine (musl)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":null,"import_time_s":0.13,"mem_mb":3.8,"disk_size":"23.4M"},{"runtime":"python:3.11-slim","python_version":"3.11","os_libc":"slim (glibc)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":2,"import_time_s":0.11,"mem_mb":3.8,"disk_size":"24M"},{"runtime":"python:3.12-alpine","python_version":"3.12","os_libc":"alpine (musl)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":null,"import_time_s":0.11,"mem_mb":3.7,"disk_size":"15.0M"},{"runtime":"python:3.12-slim","python_version":"3.12","os_libc":"slim (glibc)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":1.7,"import_time_s":0.12,"mem_mb":3.7,"disk_size":"16M"},{"runtime":"python:3.13-alpine","python_version":"3.13","os_libc":"alpine (musl)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":null,"import_time_s":0.14,"mem_mb":4.2,"disk_size":"14.8M"},{"runtime":"python:3.13-slim","python_version":"3.13","os_libc":"slim (glibc)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":1.7,"import_time_s":0.12,"mem_mb":4,"disk_size":"15M"},{"runtime":"python:3.9-alpine","python_version":"3.9","os_libc":"alpine (musl)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":null,"import_time_s":0.08,"mem_mb":3.2,"disk_size":"20.1M"},{"runtime":"python:3.9-slim","python_version":"3.9","os_libc":"slim (glibc)","variant":"pysmt","exit_code":0,"wheel_type":"wheel","failure_reason":null,"import_side_effects":"clean","install_time_s":2,"import_time_s":0.07,"mem_mb":3.2,"disk_size":"21M"}]}}