Skip to main content
Pre-release

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

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

Download files

Download the file for your platform. If you're not sure which to choose, learn more about installing packages.

Source Distribution

PySMT-0.9.7.dev129.tar.gz (264.6 kB view details)

Uploaded Source

Built Distribution

If you're not sure about the file name format, learn more about wheel file names.

PySMT-0.9.7.dev129-py2.py3-none-any.whl (327.9 kB view details)

Uploaded Python 2Python 3

File details

Details for the file PySMT-0.9.7.dev129.tar.gz.

File metadata

  • Download URL: PySMT-0.9.7.dev129.tar.gz
  • Upload date:
  • Size: 264.6 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.11.12

File hashes

Hashes for PySMT-0.9.7.dev129.tar.gz
Algorithm Hash digest
SHA256 1f6eda4bdab117a1b331c0d2cd6ba3d6fcfbdefb8f75e73f16b1f90d4a7c8e8f
MD5 7a1bd68e971ce71ab8ab294124ff19fc
BLAKE2b-256 05c390c9bba316f0c0bd6f1e92fcc7a7d8a2b7aa579df12e9df37d427d955a9a

See more details on using hashes here.

File details

Details for the file PySMT-0.9.7.dev129-py2.py3-none-any.whl.

File metadata

  • Download URL: PySMT-0.9.7.dev129-py2.py3-none-any.whl
  • Upload date:
  • Size: 327.9 kB
  • Tags: Python 2, Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/4.0.2 CPython/3.11.12

File hashes

Hashes for PySMT-0.9.7.dev129-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 4eb88a9af72a6f08b5a4ef72916046bc532924a34fc396c3d051f800c822ff82
MD5 3e298eb4d4c46cde09602e638cca8e6a
BLAKE2b-256 ba1a317ab1d7ff73e5397a929654a8d0d137454d6dc38ef3de2e72db8af34088

See more details on using hashes here.

Release history Release notifications | RSS feed

Supported by

AWS Cloud computing and Security Sponsor Datadog Monitoring Depot Continuous Integration Fastly CDN Google Download Analytics Sentry Error logging StatusPage Status page