cvc5Automatic theorem prover for SMT (Satisfiability Modulo Theories)
1.4.2mathΣ=0 1.4.1Version of this port present on the latest quarterly branch.upstream: cvc5-1.4.2A newer version was found upstream by portscout, first on 2026-11-13.
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.
===> The following configuration options are available for cvc5-1.4.2:
COCOALIB=off: Use CoCoALib for further polynomial operations
EDITLINE=on: Use Editline for better interactive support
GLPK=off: Use GLPK simplex solver
JAVA=on: Java platform support
POLY=on: Use LibPoly for polynomial arithmetic
====> Options available for the group SOLVERS
CRYPTOMINISAT=on: Use CryptoMiniSat as the SAT solver
KISSAT=on: 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
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
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>
