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.

pySMT works on both Python 3 and Python 2.

Wanna know more?

Visit http://www.pysmt.org

Metadata

Release files for PySMT 0.8.1.dev101

For a detailed explanation of source distributions (sdists) and built distributions (wheels), please see the package formats documentation.

Built distribution (wheel)

Table of built distributions (wheels) for PySMT 0.8.1.dev101
File Interpreter ABI Platform
PySMT-0.8.1.dev101-py2.py3-none-any.whl Python 3, Python 2 none any Details

Release files / PySMT-0.8.1.dev101-py2.py3-none-any.whl

Download URL PySMT-0.8.1.dev101-py2.py3-none-any.whl
Size 316.6 kB
Tags Python 2 Python 3
SHA-256 checksum
How to use checksums
93c8ee7e5d0afc83a2c5593a0cf1440fe0c74dad5bb0567e710af764618cfd68
BLAKE2b-256 checksum
How to use checksums
2e9ae3062b1259f564d96f6fc18afeced26d85b02e33890fd7d05b9d749f481c
Upload date
Uploaded using Trusted Publishing?
What is trusted publishing?
No
Uploaded via twine/3.1.1 pkginfo/1.5.0.1 requests/2.23.0 setuptools/41.2.0 requests-toolbelt/0.9.1 tqdm/4.45.0 CPython/3.7.6

Release history Release notifications | RSS feed

0.9.6

2 release files

0.9.5

2 release files

0.9.0

1 release file

This release

0.8.1.dev101 This release

1 release file

0.8.0

1 release file

0.7.5

1 release file

0.7.0

1 release file

0.6.1

1 release file

0.6.0

1 release file

0.5.1

1 release file

0.5.0

1 release file

0.4.4

1 release file

0.4.3

1 release file

0.4.2

1 release file

0.4.1

1 release file

0.4.0

1 release file

0.3.0

1 release file

0.2.5.dev

0.2.4

1 release file

0.2.3

1 release file

0.2.2

1 release 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