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.dev439.tar.gz (311.1 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.dev439-py2.py3-none-any.whl (386.7 kB view details)

Uploaded Python 2Python 3

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev439.tar.gz
  • Upload date:
  • Size: 311.1 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.dev439.tar.gz
Algorithm Hash digest
SHA256 7dcad278aa78ada2cfe438db66d11f8a917e202237bcf69d9787e106586ac7d7
MD5 73f46630b03746573390538d01d03367
BLAKE2b-256 a42910e820bbced4ec745e50d8eef8eb171a07851e544ced721f7bc5d6bd1707

See more details on using hashes here.

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev439-py2.py3-none-any.whl
  • Upload date:
  • Size: 386.7 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.dev439-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 eeb4e047ac0e10e0d73773fe89299761f62ba5189fd0db79f2a547813886aaab
MD5 eb349f30bbf897335db72bd0e8175cc7
BLAKE2b-256 99e9dd80aa4c8ebabba45fde02f26db983598dd456eabf3bc5ab1e74787b88fc

See more details on using hashes here.

Release history Release notifications | RSS feed

This release

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