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.dev446.tar.gz (311.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.dev446-py2.py3-none-any.whl (387.2 kB view details)

Uploaded Python 2Python 3

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev446.tar.gz
  • Upload date:
  • Size: 311.6 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.dev446.tar.gz
Algorithm Hash digest
SHA256 f3665c0ffc2a391397f1f8e64574b188c8ba95d0e48c9110e65af3a9b8452bc0
MD5 627986f8fcbba5c7176fdb1f278173f0
BLAKE2b-256 d369134c09bd895c020b9f04d55e50070348893f46096f550867662ed0bba1f4

See more details on using hashes here.

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev446-py2.py3-none-any.whl
  • Upload date:
  • Size: 387.2 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.dev446-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 7888d89c92c46f20f8453b94ff28eb17e5fb07ab8ea468b1592ccaca0dfd24b2
MD5 771ade754b93781749e37deb235351cd
BLAKE2b-256 2addd1e6a5a549e2f445ac5c03ccfdb618d84a20f8562a819c37961a6c15a33b

See more details on using hashes here.

Release history Release notifications | RSS feed

This release

0.9.7.dev446 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