math/z3 5.3.1.0 FreeBSD
Z3 Theorem Prover
- System
- FreeBSD
- Repository
- FreeBSD ports
- Maintainer
- [email protected]
- Last update
- Commit
896185a6d8- License
- MIT
- Categories
- math
- Package size
- 13060.0 KiB, 46064.0 KiB installed
Description
Z3 is a high-performance theorem prover developed at Microsoft Research.
In the other systems
Install
Binary package:
pkg install z3From the ports tree:
cd /usr/ports/math/z3/ && make install cleanTo depend on this port in another port's Makefile:
RUN_DEPENDS= z3>0:math/z3
LIB_DEPENDS= libz3.so:math/z3Packages
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 | 5.1.0.0 | 5.1.0.0 | - | 4.14.1.0 | 5.3.1.0 |
| FreeBSD:14:quarterly | 5.1.0.0 | 5.1.0.0 | n/a | 4.14.1.0 | 5.1.0.0 |
| FreeBSD:15:latest | 5.1.0.0 | 5.3.1.0 | n/a | 4.14.1.0 | 4.14.1.0 |
| FreeBSD:15:quarterly | 5.1.0.0 | 5.1.0.0 | n/a | n/a | n/a |
| FreeBSD:16:latest | 5.1.0.0 | 5.3.1.0 | n/a | n/a | n/a |
| FreeBSD:16:quarterly | n/a | n/a | n/a | n/a | n/a |
Dependencies
The Makefile names none itself; they come from USES and USE_*.
The full lists below include those, and their dependencies in turn.
Build dependencies 15
Required by 21
- astro/py-pytest-astropy
- cad/PrusaSlicer
- cad/py-pymtl
- devel/cbmc
- devel/py-crosshair-tool
- devel/py-hypothesis
- devel/py-hypothesis-crosshair
- devel/py-hypothesmith
- lang/solidity
- math/py-CyLP
- math/py-claripy
- math/py-z3-solver
- math/vampire
- misc/py-pytorch
- net-mgmt/py-ciscoconfparse2
- science/py-MDAnalysisTests
- security/hs-cryptol
- security/klee
- security/py-angr
- sysutils/triton
- textproc/py-textdistance
Configuration
Options name: math_z3
| Option | Default | Description |
|---|---|---|
| GMP | off | GMP (multiple precision arithmetic) support |
- USES
- cmake:testing compiler:c++20-lang localbase:ldflags
- Service scripts
- none
Files
pkg-plist 23
- bin/z3
- include/z3++.h
- include/z3.h
- include/z3_algebraic.h
- include/z3_api.h
- include/z3_ast_containers.h
- include/z3_fixedpoint.h
- include/z3_fpa.h
- include/z3_macros.h
- include/z3_optimization.h
- include/z3_polynomial.h
- include/z3_rcf.h
- include/z3_spacer.h
- include/z3_v1.h
- include/z3_version.h
- lib/cmake/z3/Z3-shared-targets-.cmake
- lib/cmake/z3/Z3-shared-targets.cmake
- lib/cmake/z3/Z3Config.cmake
- lib/cmake/z3/Z3ConfigVersion.cmake
- lib/libz3.so
- lib/libz3.so.5.3
- lib/libz3.so.
- libdata/pkgconfig/z3.pc
distinfo 1
| File | Size | SHA256 |
|---|---|---|
| z3_solver-5.3.1.0.tar.gz | 5.870439e+06 | efa420092193e1e65f90fedb0905e230deb1673634e0c66cccf4aab14d533473 |
Master sites 1
- https://github.com/Z3Prover/z3/releases/download/z3-${DISTVERSION:R}/
Commit history 3
| Date | Commit | Credits | Log message |
|---|---|---|---|
896185a6d8 |
Älven | math/z3: Update 5.1.0.0 => 5.3.1.0 Approved by: arrowd@ (maintainer)
Differential Revision: https://reviews.freebsd.org/D60825 |
|
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) |