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.dev135

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.dev135
File Size Uploaded
PySMT-0.9.7.dev135.tar.gz 264.6 kB Details

Built distribution (wheel)

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

Total release size: 592.5 kB

Release files / PySMT-0.9.7.dev135.tar.gz

Download URL PySMT-0.9.7.dev135.tar.gz
Size 264.6 kB
Tags Source
SHA-256 checksum
How to use checksums
f044c85ee3c8f9f56f60968fcc24267fe1793a43123de30ab3aa54f8ea820746
BLAKE2b-256 checksum
How to use checksums
b5b5b50fcf6540506df96c1f611fa311b90ca3a7accd66910e5926a77503a185
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/4.0.2 CPython/3.11.12

Release files / PySMT-0.9.7.dev135-py2.py3-none-any.whl

Download URL PySMT-0.9.7.dev135-py2.py3-none-any.whl
Size 327.9 kB
Tags Python 2 Python 3
SHA-256 checksum
How to use checksums
faf7d496199e0c4f20cdf40f0896ea159583e3893f60ea21f76f34d8f6e4b0e5
BLAKE2b-256 checksum
How to use checksums
d95960a721c3eb3d89dbed1a7cccebbcce0d5ae50e436dbce2730e9605c6af93
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/4.0.2 CPython/3.11.12

Release history Release notifications | RSS feed

This release

0.9.7.dev135 This release

2 release files

0.9.6

2 release files

0.9.5

2 release files

0.9.0

1 release file

0.8.0

1 release file

0.7.5

1 release file

0.7.0

1 release file

0.6.1

1 release file

0.6.0

1 release file

0.5.1

1 release file

0.5.0

1 release file

0.4.4

1 release file

0.4.3

1 release file

0.4.2

1 release file

0.4.1

1 release file

0.4.0

1 release file

0.3.0

1 release file

0.2.5.dev

0.2.4

1 release file

0.2.3

1 release file

0.2.2

1 release file

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