Port details on branch 2022Q2 |
- cvc5 Automatic theorem prover for SMT (Satisfiability Modulo Theories)
- 1.1.2 math =0 1.0.8_1Version of this port present on the latest quarterly branch.
- Maintainer: yuri@FreeBSD.org
- Port Added: 2023-01-04 11:54:07
- Last Update: 2024-03-04 23:19:08
- Commit Hash: 0d21946
- Also Listed In: java
- License: BSD3CLAUSE
- WWW:
- https://cvc5.github.io/
- Description:
- An efficient open-source automatic theorem prover for satisfiability modulo
theories (SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in logical
theories and their combination.
- ¦ ¦ ¦ ¦
- Manual pages:
- FreshPorts has no man page information for this port.
- pkg-plist: as obtained via:
make generate-plist - Dependency lines:
-
- To install the port:
- cd /usr/ports/math/cvc5/ && make install clean
- To add the package, run one of these commands:
- pkg install math/cvc5
- pkg install cvc5
NOTE: If this package has multiple flavors (see below), then use one of them instead of the name specified above.- PKGNAME: cvc5
- Flavors: there is no flavor information for this port.
- distinfo:
- TIMESTAMP = 1709575825
SHA256 (cvc5-cvc5-cvc5-1.1.2_GH0.tar.gz) = f2eba3f957f5e064e6a87f0dce88fd647932d02014061c8f6a79bf188203993a
SIZE (cvc5-cvc5-cvc5-1.1.2_GH0.tar.gz) = 8581968
Packages (timestamps in pop-ups are UTC):
- Dependencies
- NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
- Build dependencies:
-
- bash : shells/bash
- libcadical.a : math/cadical
- symfpu.a : math/symfpu
- py39-toml>0 : textproc/py-toml@py39
- py39-tomli>0 : textproc/py-tomli@py39
- py39-pyparsing>0 : devel/py-pyparsing@py39
- libedit>0 : devel/libedit
- swig : devel/swig
- java : java/openjdk8
- cmake : devel/cmake-core
- ninja : devel/ninja
- pkgconf>=1.3.0_1 : devel/pkgconf
- python3.9 : lang/python39
- Runtime dependencies:
-
- libedit>0 : devel/libedit
- Library dependencies:
-
- libantlr3c.so : devel/libantlr3c
- libcryptominisat5.so : math/cryptominisat
- libgmp.so : math/gmp
- This port is required by:
- for Run
-
- devel/cbmc
Configuration Options:
- ===> The following configuration options are available for cvc5-1.1.2:
COCOALIB=off: Use CoCoALib for further polynomial operations
EDITLINE=on: Use Editline for better interactive support
JAVA=on: Java platform support
====> Options available for the group SOLVERS
CRYPTOMINISAT=on: Use CryptoMiniSat as the SAT solver
KISSAT=off: Use Kissat solver
====> Options available for the radio NUMLIB: you can only select none or one of them
GMP=on: Use GMP numeric library
CLN=off: Use CLN numeric library
===> Use 'make config' to modify these settings
- Options name:
- math_cvc5
- USES:
- cmake:testing ncurses compiler:c++17-lang localbase:ldflags pkgconfig python:build
- FreshPorts was unable to extract/find any pkg message
- Master Sites:
|