BSD Portsmath/py-pysmt 0.9.6_3 FreeBSD
Solver-agnostic library for SMT formulae manipulation and solving
- System
- FreeBSD
- Repository
- FreeBSD ports
- Maintainer
- [email protected]
- Last update
- Commit
c3ee0d25f0- License
- APACHE20
- Categories
- math, python
- Package size
- 603.9 KiB, 4750.9 KiB installed
Description
pySMT is a library for SMT formulae manipulation and solving, which makes working with Satisfiability Modulo Theory simple.
Among others, the user 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.
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: MathSAT, Z3, CVC4, Yices, CUDD, PicoSAT, and Boolector. 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.
In the other systems
| System | Port | Version |
|---|---|---|
| FreeBSD | math/py-pysmt | 0.9.6_3 |
| OpenBSD | math/py-pysmt | 0.9.6p0 |
| DragonFly | math/py-pysmt | 0.9.6_1 |
| HardenedBSD | math/py-pysmt | 0.9.6_3 |
| GhostBSD | math/py-pysmt | 0.9.6_3 |
Install
Binary package:
pkg install py312-pysmtFrom the ports tree:
cd /usr/ports/math/py-pysmt/ && make install cleanTo depend on this port in another port's Makefile:
RUN_DEPENDS= py312-pysmt>0:math/py-pysmtPackages
The version each package repository carries. “-” means the repository builds no package of it, “n/a” that there is no such repository.
| Repository | aarch64 | amd64 | armv6 | armv7 | i386 |
|---|---|---|---|---|---|
| FreeBSD:14:latest | 0.9.6_3 | 0.9.6_3 | 0.9.0 | 0.9.6_1 | 0.9.6_3 |
| FreeBSD:14:quarterly | 0.9.6_3 | 0.9.6_3 | n/a | 0.9.6_1 | 0.9.6_3 |
| FreeBSD:15:latest | 0.9.6_3 | 0.9.6_3 | n/a | 0.9.6_1 | 0.9.6_1 |
| FreeBSD:15:quarterly | 0.9.6_3 | 0.9.6_3 | n/a | n/a | n/a |
| FreeBSD:16:latest | 0.9.6_3 | 0.9.6_3 | n/a | n/a | n/a |
| FreeBSD:16:quarterly | n/a | n/a | n/a | n/a | n/a |
Dependencies
As this port's Makefile names them.
Runtime 1
${PYTHON_PKGNAMEPREFIX}six>=0: devel/py-six
Test 3
${PYTHON_PKGNAMEPREFIX}z3-solver>0: math/py-z3-solverz3>0: math/z3cvc5>0: math/cvc5
The full lists below include those, and their dependencies in turn.
Build dependencies 11
Run dependencies 8
No port depends on this one.
Configuration
No options to configure.
- USES
- python
- Service scripts
- none
Files
distinfo 1
| File | Size | SHA256 |
|---|---|---|
| pysmt-pysmt-v0.9.6_GH0.tar.gz | 1.141496e+06 | d69561abccd089c23352a6862b3939574d47d37ed82a5d7dce75127437c06032 |
Commit history 2
| Date | Commit | Credits | Log message |
|---|---|---|---|
c3ee0d25f0 |
Älven | math/z3: Update 5.0.0.0 => 5.1.0.0 Approved by: arrowd@ (maintainer)
Approved by: db@, yuri@ (Mentors, implicit)
Differential Revision: https://reviews.freebsd.org/D58886 |
|
dfa5362257 |
Yuri Victorovich | math/z3: update 4.16.0.0 → 5.0.0.0 PR: 297106
Approved by: Gleb Popov <[email protected]> (maintainer) |