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.dev444.tar.gz (311.7 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.dev444-py2.py3-none-any.whl (387.3 kB view details)

Uploaded Python 2Python 3

File details

Details for the file pysmt-0.9.7.dev444.tar.gz.

File metadata

  • Download URL: pysmt-0.9.7.dev444.tar.gz
  • Upload date:
  • Size: 311.7 kB
  • Tags: Source
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for pysmt-0.9.7.dev444.tar.gz
Algorithm Hash digest
SHA256 9ab000bfa24acedef05f7873d5a1bb1f89f6b1929cd21ec43dfe187929b375ee
MD5 7df392a0659dd38ac0f8ccd78ccef622
BLAKE2b-256 239dba30e2b7a0e909052d7125c6d41b6f6e4ac4d1223cc8148c08ae3c8ae982

See more details on using hashes here.

File details

Details for the file pysmt-0.9.7.dev444-py2.py3-none-any.whl.

File metadata

  • Download URL: pysmt-0.9.7.dev444-py2.py3-none-any.whl
  • Upload date:
  • Size: 387.3 kB
  • Tags: Python 2, Python 3
  • Uploaded using Trusted Publishing? No
  • Uploaded via: twine/7.0.0 CPython/3.13.14

File hashes

Hashes for pysmt-0.9.7.dev444-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 ce14749d90872fa5533efe140e72795a67921f353d4f8c3a0faeacdb3a208990
MD5 18d17354917b0501d8a634deb0fb9174
BLAKE2b-256 a8ad009be3a8037622999980bac1d57aa28f6171a2ad74f7fa8d5c59df28aa99

See more details on using hashes here.

Release history Release notifications | RSS feed

This release

0.9.7.dev444 This release

2 files

0.9.6

2 files

0.9.5

2 files

0.9.0

1 file

0.8.0

1 file

0.7.5

1 file

0.7.0

1 file

0.6.1

1 file

0.6.0

1 file

0.5.1

1 file

0.5.0

1 file

0.4.4

1 file

0.4.3

1 file

0.4.2

1 file

0.4.1

1 file

0.4.0

1 file

0.3.0

1 file

0.2.5.dev

0.2.4

1 file

0.2.3

1 file

0.2.2

1 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