FreshPorts -- math/cvc5: Automatic theorem prover for SMT (Satisfiability Modulo Theories)

Port details

cvc5 Automatic theorem prover for SMT (Satisfiability Modulo Theories)

1.2.1 math =2 1.2.1Version of this port present on the latest quarterly branch.

Maintainer: yuri@FreeBSD.org

Port Added: 2023-01-04 11:54:07

Last Update: 2025-01-28 05:59:13

Commit Hash: 2cae0a1

People watching this port, also watch:: jdictionary, py311-Automat, py311-python-gdsii, py311-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

Expand this list (28 items)

Collapse this list.

@ldconfig
/usr/local/share/licenses/cvc5-1.2.1/catalog.mk
/usr/local/share/licenses/cvc5-1.2.1/LICENSE
/usr/local/share/licenses/cvc5-1.2.1/BSD3CLAUSE
bin/cvc5
include/cvc5/c/cvc5.h
include/cvc5/c/cvc5_parser.h
include/cvc5/cvc5.h
include/cvc5/cvc5_export.h
include/cvc5/cvc5_kind.h
include/cvc5/cvc5_parser.h
include/cvc5/cvc5_proof_rule.h
include/cvc5/cvc5_skolem_id.h
include/cvc5/cvc5_types.h
lib/cmake/cvc5/cvc5Config.cmake
lib/cmake/cvc5/cvc5ConfigVersion.cmake
lib/cmake/cvc5/cvc5Targets-production.cmake
lib/cmake/cvc5/cvc5Targets.cmake
lib/libcvc5.so
lib/libcvc5.so.1
@comment lib/libcvc5jni.so
lib/libcvc5parser.so
lib/libcvc5parser.so.1
@comment share/java/cvc5-1.2.1.jar
@comment share/java/cvc5.jar
@owner
@group
@mode

Collapse this list.

Dependency lines:

cvc5>0:math/cvc5

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 = 1738036883 SHA256 (cvc5-cvc5-cvc5-1.2.1_GH0.tar.gz) = 01197ca37a810bce418ae98a44dbb3348697554582395300a09c85d7af182d69 SIZE (cvc5-cvc5-cvc5-1.2.1_GH0.tar.gz) = 9045038

Packages (timestamps in pop-ups are UTC):

cvc5
ABI	aarch64	amd64	armv6	armv7	i386	powerpc	powerpc64	powerpc64le
FreeBSD:13:latest	1.2.1	1.2.1	-	1.2.1	1.2.1	-	-	-
FreeBSD:13:quarterly	1.2.0	1.2.0	1.0.5_2	1.2.0	1.2.1	-	1.0.8_1	1.0.8_1
FreeBSD:14:latest	1.2.1	1.2.1	-	1.2.1	1.2.1	-	-	1.0.5_1
FreeBSD:14:quarterly	1.2.0	1.2.1	-	1.2.0	1.2.1	-	1.0.8_1	1.0.8_1
FreeBSD:15:latest	1.2.1	1.2.1	n/a	1.2.1	n/a	-	1.1.1	1.1.1_1

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
cmake : devel/cmake-core
ninja : devel/ninja
java : java/openjdk8
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.1: 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 java:build localbase:ldflags pkgconfig python:build

FreshPorts was unable to extract/find any pkg message

Master Sites:

Expand this list (1 items)

Collapse this list.

https://codeload.github.com/cvc5/cvc5/tar.gz/cvc5-1.2.1?dummy=/

Collapse this list.

Port Moves

port moved here from math/cvc3 on 2023-01-04
REASON: CVC3 was succeeded by CVC4 and CVC5
port moved here from math/cvc4 on 2023-01-03
REASON: CVC4 was succeeded by CVC5

Number of commits found: 21

Commit	Credits	Log message
Commit History - (may be incomplete: for full details, see links to repositories near top of page)
1.2.1 28 Jan 2025 05:59:13	Yuri Victorovich (yuri)	math/cvc5: update 1.2.0 → 1.2.1 Reported by: portscout
1.2.0 31 Dec 2024 08:57:55	Muhammad Moinur Rahman (bofh)	Mk/**java.mk: Convert bsd.java.mk to USES The following features have been added or changed: - Instead of USE_JAVA use USES=java. This defaults to USES=java:build,run if NO_BUILD is undefined. Else it defaults to USES=java:run - Instead of USE_ANT=yes use USES=java:ant which also implies USES=java:build - Instead of JAVA_BUILD=yes use USES=java:build. Does not imply run or extract - Instead of JAVA_EXTRACT=yes use USES=java:extract does not imply build or run - Instead of JAVA_RUN=yes use USES=java:run does not imply extract or build - Instead of USE_JAVA=<version> use USES=java and JAVA_VERSION=<version> Approved by: mat (portmgr), glewis Differential Revision: https://reviews.freebsd.org/D48201
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.

Number of commits found: 21

Login
User Login Create account

Servers and bandwidth provided by
New York Internet, iXsystems, and RootBSD

This site
What is FreshPorts? About the authors Issues FAQ How big is it? Security Policy Privacy Blog Contact

Search
Enter Keywords: more...

Latest Vulnerabilities

jenkins	Apr 11
jenkins-lts	Apr 11
gitlab	Apr 10
expat2	Apr 09
firefox	Apr 07
firefox	Apr 07
firefox	Apr 07
firefox	Apr 07
firefox	Apr 07
firefox	Apr 07
firefox-esr	Apr 07
firefox-esr	Apr 07
firefox-esr	Apr 07
librewolf	Apr 07
librewolf	Apr 07

33 vulnerabilities affecting 380 ports have been reported in the past 14 days

^* - modified, not new

All vulnerabilities

Last processed:
2025-04-11 06:28:22 UTC

Ports
Home Categories Deleted ports Sanity Test Failures Newsfeeds

Statistics

Graphs
NEW Graphs (Javascript)

Calculated hourly:

Port count	33265
Broken	128
Deprecated	282
Ignore	244
Forbidden	1
Restricted	2
No CDROM	1
Vulnerable	27
Expired	33
Set to expire	239
Interactive	0
new 24 hours	1
new 48 hours	1
new 7 days	17
new fortnight	29
new month	91

Newsfeed changes