Skip to main content
Pre-release

This release is a pre-release and may not be stable for production use.

pySMT: A library for SMT formulae manipulation and solving

pySMT makes working with Satisfiability Modulo Theory simple.

Among others, you can:

  • Define formulae in a solver independent way in a simple and inutitive way,

  • Write ad-hoc simplifiers and operators,

  • Dump your problems in the SMT-Lib format,

  • Solve them using one of the native solvers, or by wrapping any SMT-Lib complaint solver.

Supported Theories and Solvers

pySMT provides methods to define a formula in Linear Real Arithmetic (LRA), Real Difference Logic (RDL), their combination (LIRA), Equalities and Uninterpreted Functions (EUF), Bit-Vectors (BV), and Arrays (A). The following solvers are supported through native APIs:

Additionally, you can use any SMT-LIB 2 compliant solver.

PySMT assumes that the python bindings for the SMT Solver are installed and accessible from your PYTHONPATH.

Wanna know more?

Visit http://www.pysmt.org

Metadata

Release files for PySMT 0.9.7.dev444

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Source distribution (sdist)

Source distribution for PySMT 0.9.7.dev444
File Size Uploaded Provenance
pysmt-0.9.7.dev444.tar.gz 311.7 kB Without provenance Details

Built distribution (wheel)

Table of built distributions (wheels) for PySMT 0.9.7.dev444
File Interpreter ABI Platform
pysmt-0.9.7.dev444-py2.py3-none-any.whl Python 3, Python 2 none any Details

Total release size: 699.1 kB

Release files / pysmt-0.9.7.dev444.tar.gz

Download URL pysmt-0.9.7.dev444.tar.gz
Size 311.7 kB
Tags Source
SHA-256 checksum
How to use checksums
9ab000bfa24acedef05f7873d5a1bb1f89f6b1929cd21ec43dfe187929b375ee
BLAKE2b-256 checksum
How to use checksums
239dba30e2b7a0e909052d7125c6d41b6f6e4ac4d1223cc8148c08ae3c8ae982
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/7.0.0 CPython/3.13.14

Release files / pysmt-0.9.7.dev444-py2.py3-none-any.whl

Download URL pysmt-0.9.7.dev444-py2.py3-none-any.whl
Size 387.3 kB
Tags Python 2 Python 3
SHA-256 checksum
How to use checksums
ce14749d90872fa5533efe140e72795a67921f353d4f8c3a0faeacdb3a208990
BLAKE2b-256 checksum
How to use checksums
a8ad009be3a8037622999980bac1d57aa28f6171a2ad74f7fa8d5c59df28aa99
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/7.0.0 CPython/3.13.14

Security for PySMT 0.9.7.dev444

Provenance

Provenance describes where a file came from. On PyPI, provenance is shared via attestations, which provide a verifiable record of the build or publishing details. View details, limitations and caveats.

No provenance found

None of the files in this release were uploaded with provenance metadata.

A note on package security

PyPI is a repository for distributing packages, not a service for auditing them. While third-party security researchers and our staff do their best to detect and remove malicious packages, PyPI cannot guarantee the quality, security or suitability of any given package.

To learn more about protecting yourself from malicious actors, visit our package security documentation.

Release history Release notifications | RSS feed

This release

0.2.5.dev

Anthropic, PBC Visionary sponsor Bloomberg Visionary sponsor Hudson River Trading Visionary sponsor Meta Visionary sponsor NVIDIA Visionary sponsor Microsoft Sustainability sponsor Depot Continuous Integration AWS Cloud computing and Security Sponsor Datadog Monitoring Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page