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.dev436.tar.gz (309.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.dev436-py2.py3-none-any.whl (385.0 kB view details)

Uploaded Python 2Python 3

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev436.tar.gz
  • Upload date:
  • Size: 309.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.dev436.tar.gz
Algorithm Hash digest
SHA256 605f74b6f1764225a3003531284f50a9e3641a0c2c5d1be5c2f2257d4241ebf8
MD5 5f3b6f4edf6144bb59e1ae073167d71b
BLAKE2b-256 0d38648b61fae0306252dfd9742c67a998c1ac3afef73fe6431de21279188f54

See more details on using hashes here.

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev436-py2.py3-none-any.whl
  • Upload date:
  • Size: 385.0 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.dev436-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 ef4c3e4d71860220f3889e2333657489cade9aff3bc3fd1a41542ca0cd79943c
MD5 1fae48a21e37aa9dced6998c27019794
BLAKE2b-256 fe3a30fa5f0b231bcbb181ee53095364e1b56c5ef3819bd00839ce8a7ba03153

See more details on using hashes here.

Release history Release notifications | RSS feed

This release

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