Port details |
- cvc5 Automatic theorem prover for SMT (Satisfiability Modulo Theories)
- 1.2.0 math =2 1.2.0Version of this port present on the latest quarterly branch.
- Maintainer: yuri@FreeBSD.org
- Port Added: 2023-01-04 11:54:07
- Last Update: 2024-08-11 16:54:42
- Commit Hash: d41c16c
- People watching this port, also watch:: jdictionary, py311-Automat, py311-python-gdsii, py39-PyOpenGL, p5-Sane
- 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 = 1723346538
SHA256 (cvc5-cvc5-cvc5-1.2.0_GH0.tar.gz) = 7877b1f89f8b6a6bcc643d9ab1c60535911f6a30e32233eafa9db8a3eae5e34e
SIZE (cvc5-cvc5-cvc5-1.2.0_GH0.tar.gz) = 8916450
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
- symfpu.a : math/symfpu
- py311-toml>0 : textproc/py-toml@py311
- py311-tomli>0 : textproc/py-tomli@py311
- py311-pexpect>0 : misc/py-pexpect@py311
- py311-pybind11>0 : devel/py-pybind11@py311
- py311-pyparsing>0 : devel/py-pyparsing@py311
- libedit>0 : devel/libedit
- java : java/openjdk8
- cmake : devel/cmake-core
- ninja : devel/ninja
- pkgconf>=1.3.0_1 : devel/pkgconf
- python3.11 : lang/python311
- Runtime dependencies:
-
- libedit>0 : devel/libedit
- Library dependencies:
-
- libantlr3c.so : devel/libantlr3c
- libcadical.so : math/cadical
- 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.2.0:
COCOALIB=off: Use CoCoALib for further polynomial operations
EDITLINE=on: Use Editline for better interactive support
JAVA=off: 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:
|
Commit History - (may be incomplete: for full details, see links to repositories near top of page) |
Commit | Credits | Log message |
1.2.0 11 Aug 2024 16:54:42 |
Yuri Victorovich (yuri) |
math/cvc5: update 1.1.2 → 1.2.0
Reported by: portscout |
1.1.2_1 06 Jun 2024 08:48:57 |
Yuri Victorovich (yuri) |
math/cadical: Add shared library |
1.1.2 04 Mar 2024 23:19:08 |
Yuri Victorovich (yuri) |
math/cvc5: update 1.1.1 → 1.1.2
Reported by: portscout |
1.1.1_1 13 Feb 2024 14:44:22 |
Dima Panov (fluffy) |
devel/boost: bump consumers after library update |
1.1.1 27 Jan 2024 08:25:17 |
Yuri Victorovich (yuri) |
math/cvc5: update 1.1.0 → 1.1.1
Reported by: portscout |
1.1.0 07 Jan 2024 20:40:49 |
Yuri Victorovich (yuri) |
math/cvc5: update 1.0.8 → 1.1.0
Reported by: portscout |
1.0.8_1 05 Jan 2024 09:38:10 |
Yuri Victorovich (yuri) |
math/cvc5: Update the PORTSCOUT line |
1.0.8_1 27 Sep 2023 14:36:30 |
Dima Panov (fluffy) |
devel/boost*: bump all consumers after 1.83.0 |
1.0.8 17 Sep 2023 18:47:39 |
Yuri Victorovich (yuri) |
math/cvc5: update 1.0.5 → 1.0.8 |
1.0.5_2 27 Jun 2023 19:34:34 |
Rene Ladan (rene) |
all: remove explicit versions in USES=python for "3.x+"
The logic in USES=python will automatically convert this to 3.8+ by
itself.
Adjust two ports that only had Python 3.7 mentioned but build fine
on Python 3.8 too.
finance/quickfix: mark BROKEN with PYTHON
libtool: compile: c++ -DHAVE_CONFIG_H -I. -I../.. -I -I. -I.. -I../.. -I../C++
-DLIBICONV_PLUG -DPYTHON_MAJOR_VERSION=3 -Wno-unused-variable
-Wno-maybe-uninitialized -O2 -pipe -DLIBICONV_PLUG -fstack-protector-strong
-fno-strict-aliasing -DLIBICONV_PLUG -Wall -ansi
-Wno-unused-command-line-argument -Wpointer-arith -Wwrite-strings
-Wno-overloaded-virtual -Wno-deprecated-declarations -Wno-deprecated -std=c++0x
-MT _quickfix_la-QuickfixPython.lo -MD -MP -MF
.deps/_quickfix_la-QuickfixPython.Tpo -c QuickfixPython.cpp -fPIC -DPIC -o
.libs/_quickfix_la-QuickfixPython.o
warning: unknown warning option '-Wno-maybe-uninitialized'; did you mean
'-Wno-uninitialized'? [-Wunknown-warning-option]
QuickfixPython.cpp:175:11: fatal error: 'Python.h' file not found
^~~~~~~~~~
1 warning and 1 error generated.
Reviewed by: portmgr, vishwin, yuri
Differential Revision: <https://reviews.freebsd.org/D40568> |
1.0.5_2 25 Jun 2023 18:29:33 |
Yuri Victorovich (yuri) |
math/cadical: Update 1.5.3 → 1.6.0 |
1.0.5_1 27 Apr 2023 18:25:55 |
Dima Panov (fluffy) |
*/*: bump all direct Boost cunsumers |
1.0.5 27 Mar 2023 18:25:49 |
Yuri Victorovich (yuri) |
math/cvc5: Fix tests |
1.0.5 26 Mar 2023 17:35:48 |
Yuri Victorovich (yuri) |
math/cvc5: Add PORTSCOUT line |
1.0.5 15 Mar 2023 08:50:43 |
Yuri Victorovich (yuri) |
math/cvc5: Update 1.0.4 → 1.0.5 |
1.0.4_1 10 Feb 2023 09:42:14 |
Yuri Victorovich (yuri) |
math/cvc5: Correct options section |
1.0.4 07 Feb 2023 03:00:43 |
Yuri Victorovich (yuri) |
math/cvc5: Update 1.0.3 → 1.0.4 |
1.0.3_1 16 Jan 2023 19:32:07 |
Dima Panov (fluffy) |
*/*: bump libboost*.so libraries consumert after Boost upgrade |
1.0.3 04 Jan 2023 11:50:53 |
Yuri Victorovich (yuri) |
math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5
Remove the PYTHON option - it will be made into a separate port. |