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

Uploaded Python 2Python 3

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev441.tar.gz
  • Upload date:
  • Size: 311.2 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.dev441.tar.gz
Algorithm Hash digest
SHA256 96e086bad2595c9f5e83f45892074607774eaa042b2f1fe1c1cce36ceb818f8f
MD5 10a0d2810fec1ba0a6c7ae5c774f76c0
BLAKE2b-256 42983bc956322304f0c3c4b280aa5a97a0c5db896b6153edaabb68ae30c0832a

See more details on using hashes here.

File details

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

File metadata

  • Download URL: pysmt-0.9.7.dev441-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.dev441-py2.py3-none-any.whl
Algorithm Hash digest
SHA256 ebaaa3f6d63eb1a3ca6f058bc4cc2f9ebc0d9ed46dcaaa0034a7abb9cdfe6565
MD5 9a6d29291ff24772d944c06390b122a3
BLAKE2b-256 992e852eb6ee0c6cc5f692387a8d776cc81361e81125ec33ad10ea1f74cd7bb8

See more details on using hashes here.

Release history Release notifications | RSS feed

This release

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