notbugAs an Amazon Associate I earn from qualifying purchases.
Want a good read? Try FreeBSD Mastery: Jails (IT Mastery Book 15)
Want a good monitor light? See my photosAll times are UTC
Ukraine
Port details
cvc5 Automatic theorem prover for SMT (Satisfiability Modulo Theories)
1.2.0 math on this many watch lists=2 search for ports that depend on this port Find issues related to this port Report an issue related to this port View this port on Repology. pkg-fallout 1.2.0Version of this port present on the latest quarterly branch.
Maintainer: yuri@FreeBSD.org search for ports maintained by this maintainer
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.
Homepage    cgit ¦ Codeberg ¦ GitHub ¦ GitLab ¦ SVNWeb - no subversion history for this port

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.
  1. @ldconfig
  2. /usr/local/share/licenses/cvc5-1.2.0/catalog.mk
  3. /usr/local/share/licenses/cvc5-1.2.0/LICENSE
  4. /usr/local/share/licenses/cvc5-1.2.0/BSD3CLAUSE
  5. bin/cvc5
  6. include/cvc5/c/cvc5.h
  7. include/cvc5/c/cvc5_parser.h
  8. include/cvc5/cvc5.h
  9. include/cvc5/cvc5_export.h
  10. include/cvc5/cvc5_kind.h
  11. include/cvc5/cvc5_parser.h
  12. include/cvc5/cvc5_proof_rule.h
  13. include/cvc5/cvc5_skolem_id.h
  14. include/cvc5/cvc5_types.h
  15. lib/cmake/cvc5/cvc5Config.cmake
  16. lib/cmake/cvc5/cvc5ConfigVersion.cmake
  17. lib/cmake/cvc5/cvc5Targets-production.cmake
  18. lib/cmake/cvc5/cvc5Targets.cmake
  19. lib/libcvc5.so
  20. lib/libcvc5.so.1
  21. @comment lib/libcvc5jni.so
  22. lib/libcvc5parser.so
  23. lib/libcvc5parser.so.1
  24. @comment share/java/cvc5-1.2.0.jar
  25. @comment share/java/cvc5.jar
  26. @owner
  27. @group
  28. @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 = 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):
cvc5
ABIaarch64amd64armv6armv7i386powerpcpowerpc64powerpc64le
FreeBSD:13:latest1.2.01.2.0-1.2.01.2.0---
FreeBSD:13:quarterly1.2.01.2.01.0.5_21.2.01.2.0-1.0.8_11.0.8_1
FreeBSD:14:latest1.2.01.2.0-1.2.01.2.0--1.0.5_1
FreeBSD:14:quarterly1.2.01.2.0--1.2.0-1.0.8_11.0.8_1
FreeBSD:15:latest1.2.01.2.0n/a-n/a-1.1.11.1.1_1
Dependencies
NOTE: FreshPorts displays only information on required and default dependencies. Optional dependencies are not covered.
Build dependencies:
  1. bash : shells/bash
  2. symfpu.a : math/symfpu
  3. py311-toml>0 : textproc/py-toml@py311
  4. py311-tomli>0 : textproc/py-tomli@py311
  5. py311-pexpect>0 : misc/py-pexpect@py311
  6. py311-pybind11>0 : devel/py-pybind11@py311
  7. py311-pyparsing>0 : devel/py-pyparsing@py311
  8. libedit>0 : devel/libedit
  9. java : java/openjdk8
  10. cmake : devel/cmake-core
  11. ninja : devel/ninja
  12. pkgconf>=1.3.0_1 : devel/pkgconf
  13. python3.11 : lang/python311
Runtime dependencies:
  1. libedit>0 : devel/libedit
Library dependencies:
  1. libantlr3c.so : devel/libantlr3c
  2. libcadical.so : math/cadical
  3. libcryptominisat5.so : math/cryptominisat
  4. libgmp.so : math/gmp
This port is required by:
for Run
  1. 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:
Expand this list (1 items)
Collapse this list.
  1. https://codeload.github.com/cvc5/cvc5/tar.gz/cvc5-1.2.0?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: 19

Commit History - (may be incomplete: for full details, see links to repositories near top of page)
CommitCreditsLog message
1.2.0
11 Aug 2024 16:54:42
commit hash: d41c16c98e5d078415711d46cad8206d53e70199commit hash: d41c16c98e5d078415711d46cad8206d53e70199commit hash: d41c16c98e5d078415711d46cad8206d53e70199commit hash: d41c16c98e5d078415711d46cad8206d53e70199 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: update 1.1.2 → 1.2.0

Reported by:	portscout
1.1.2_1
06 Jun 2024 08:48:57
commit hash: e42f6a977895756044e2b6c93271b1c5fb69664acommit hash: e42f6a977895756044e2b6c93271b1c5fb69664acommit hash: e42f6a977895756044e2b6c93271b1c5fb69664acommit hash: e42f6a977895756044e2b6c93271b1c5fb69664a files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cadical: Add shared library
1.1.2
04 Mar 2024 23:19:08
commit hash: 0d219467b46a43a70b287202b39690a88bf17fe0commit hash: 0d219467b46a43a70b287202b39690a88bf17fe0commit hash: 0d219467b46a43a70b287202b39690a88bf17fe0commit hash: 0d219467b46a43a70b287202b39690a88bf17fe0 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: update 1.1.1 → 1.1.2

Reported by:	portscout
1.1.1_1
13 Feb 2024 14:44:22
commit hash: db616534ff99d6268997e2f30858891e20641a1ecommit hash: db616534ff99d6268997e2f30858891e20641a1ecommit hash: db616534ff99d6268997e2f30858891e20641a1ecommit hash: db616534ff99d6268997e2f30858891e20641a1e files touched by this commit
Dima Panov (fluffy) search for other commits by this committer
devel/boost: bump consumers after library update
1.1.1
27 Jan 2024 08:25:17
commit hash: ea1e702e732989cd9f3a3b1aef66cfe2a6caf4f3commit hash: ea1e702e732989cd9f3a3b1aef66cfe2a6caf4f3commit hash: ea1e702e732989cd9f3a3b1aef66cfe2a6caf4f3commit hash: ea1e702e732989cd9f3a3b1aef66cfe2a6caf4f3 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: update 1.1.0 → 1.1.1

Reported by:	portscout
1.1.0
07 Jan 2024 20:40:49
commit hash: cf32d424195e2314e3b7eb9f83584af6e697b51ccommit hash: cf32d424195e2314e3b7eb9f83584af6e697b51ccommit hash: cf32d424195e2314e3b7eb9f83584af6e697b51ccommit hash: cf32d424195e2314e3b7eb9f83584af6e697b51c files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: update 1.0.8 → 1.1.0

Reported by:	portscout
1.0.8_1
05 Jan 2024 09:38:10
commit hash: 0d52d8cbc0456348df6167a9d20f651ef276d5d3commit hash: 0d52d8cbc0456348df6167a9d20f651ef276d5d3commit hash: 0d52d8cbc0456348df6167a9d20f651ef276d5d3commit hash: 0d52d8cbc0456348df6167a9d20f651ef276d5d3 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Update the PORTSCOUT line
1.0.8_1
27 Sep 2023 14:36:30
commit hash: 21d8008e86830262f2a33a6dca9ddf2478cd6487commit hash: 21d8008e86830262f2a33a6dca9ddf2478cd6487commit hash: 21d8008e86830262f2a33a6dca9ddf2478cd6487commit hash: 21d8008e86830262f2a33a6dca9ddf2478cd6487 files touched by this commit
Dima Panov (fluffy) search for other commits by this committer
devel/boost*: bump all consumers after 1.83.0
1.0.8
17 Sep 2023 18:47:39
commit hash: a31acf08261d5c3a734dea6edbc94008688ffeabcommit hash: a31acf08261d5c3a734dea6edbc94008688ffeabcommit hash: a31acf08261d5c3a734dea6edbc94008688ffeabcommit hash: a31acf08261d5c3a734dea6edbc94008688ffeab files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: update 1.0.5 → 1.0.8
1.0.5_2
27 Jun 2023 19:34:34
commit hash: 3d9a815d9c5acbb71f4bb07738bdeab4879feacbcommit hash: 3d9a815d9c5acbb71f4bb07738bdeab4879feacbcommit hash: 3d9a815d9c5acbb71f4bb07738bdeab4879feacbcommit hash: 3d9a815d9c5acbb71f4bb07738bdeab4879feacb files touched by this commit
Rene Ladan (rene) search for other commits by this committer
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
commit hash: 584102d5e08dfbcb2af91db6fafdc492d1615186commit hash: 584102d5e08dfbcb2af91db6fafdc492d1615186commit hash: 584102d5e08dfbcb2af91db6fafdc492d1615186commit hash: 584102d5e08dfbcb2af91db6fafdc492d1615186 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cadical: Update 1.5.3 → 1.6.0
1.0.5_1
27 Apr 2023 18:25:55
commit hash: 3e45e8e24481fab02384c55a1e655d1dc1b781c6commit hash: 3e45e8e24481fab02384c55a1e655d1dc1b781c6commit hash: 3e45e8e24481fab02384c55a1e655d1dc1b781c6commit hash: 3e45e8e24481fab02384c55a1e655d1dc1b781c6 files touched by this commit
Dima Panov (fluffy) search for other commits by this committer
*/*: bump all direct Boost cunsumers
1.0.5
27 Mar 2023 18:25:49
commit hash: 359167a298721dff5bc99fc9bcae00d7819b50f6commit hash: 359167a298721dff5bc99fc9bcae00d7819b50f6commit hash: 359167a298721dff5bc99fc9bcae00d7819b50f6commit hash: 359167a298721dff5bc99fc9bcae00d7819b50f6 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Fix tests
1.0.5
26 Mar 2023 17:35:48
commit hash: f2389f083f3992c10828674544e068d754db8178commit hash: f2389f083f3992c10828674544e068d754db8178commit hash: f2389f083f3992c10828674544e068d754db8178commit hash: f2389f083f3992c10828674544e068d754db8178 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Add PORTSCOUT line
1.0.5
15 Mar 2023 08:50:43
commit hash: a732bcdc59d6acb3b275fd9ae0f3a0776c8b8335commit hash: a732bcdc59d6acb3b275fd9ae0f3a0776c8b8335commit hash: a732bcdc59d6acb3b275fd9ae0f3a0776c8b8335commit hash: a732bcdc59d6acb3b275fd9ae0f3a0776c8b8335 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Update 1.0.4 → 1.0.5
1.0.4_1
10 Feb 2023 09:42:14
commit hash: ca722003daacc9cf18b1eccb22500099e4fcf26acommit hash: ca722003daacc9cf18b1eccb22500099e4fcf26acommit hash: ca722003daacc9cf18b1eccb22500099e4fcf26acommit hash: ca722003daacc9cf18b1eccb22500099e4fcf26a files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Correct options section
1.0.4
07 Feb 2023 03:00:43
commit hash: 7c8a6b010bfac0c78c4123c4d3e8049600d95f73commit hash: 7c8a6b010bfac0c78c4123c4d3e8049600d95f73commit hash: 7c8a6b010bfac0c78c4123c4d3e8049600d95f73commit hash: 7c8a6b010bfac0c78c4123c4d3e8049600d95f73 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
math/cvc5: Update 1.0.3 → 1.0.4
1.0.3_1
16 Jan 2023 19:32:07
commit hash: e1287d0d1228d93e469256fa6c4c824b9d20426bcommit hash: e1287d0d1228d93e469256fa6c4c824b9d20426bcommit hash: e1287d0d1228d93e469256fa6c4c824b9d20426bcommit hash: e1287d0d1228d93e469256fa6c4c824b9d20426b files touched by this commit
Dima Panov (fluffy) search for other commits by this committer
*/*:	bump libboost*.so libraries consumert after Boost upgrade
1.0.3
04 Jan 2023 11:50:53
commit hash: faf8043d8972b9be04156c476417ed611a280821commit hash: faf8043d8972b9be04156c476417ed611a280821commit hash: faf8043d8972b9be04156c476417ed611a280821commit hash: faf8043d8972b9be04156c476417ed611a280821 files touched by this commit
Yuri Victorovich (yuri) search for other commits by this committer
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: 19