git: faf8043d8972 - main - math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5
- Go to: [ bottom of page ] [ top of archives ] [ this month ]
Date: Wed, 04 Jan 2023 11:50:57 UTC
The branch main has been updated by yuri:
URL: https://cgit.FreeBSD.org/ports/commit/?id=faf8043d8972b9be04156c476417ed611a280821
commit faf8043d8972b9be04156c476417ed611a280821
Author: Yuri Victorovich <yuri@FreeBSD.org>
AuthorDate: 2023-01-04 11:27:14 +0000
Commit: Yuri Victorovich <yuri@FreeBSD.org>
CommitDate: 2023-01-04 11:50:53 +0000
math/cvc4: Move to math/cvc5 - CVC4 was succeeded by CVC5
Remove the PYTHON option - it will be made into a separate port.
---
MOVED | 1 +
math/Makefile | 2 +-
math/cvc4/distinfo | 7 --
math/cvc4/files/patch-cmake_FindANTLR.cmake | 13 ---
math/cvc4/files/patch-cmake_FindReadline.cmake | 42 --------
math/cvc4/files/patch-doc_CMakeLists.txt | 22 -----
math/cvc4/files/patch-examples_CMakeLists.txt | 12 ---
math/cvc4/files/patch-src_CMakeLists.txt | 11 ---
math/cvc4/files/patch-src_base_configuration.cpp | 11 ---
math/cvc4/files/patch-src_main_portfolio.cpp | 24 -----
math/cvc4/files/patch-swig4 | 40 --------
math/cvc4/files/patch-test_CMakeLists.txt | 14 ---
math/cvc4/files/patch-test_regress_CMakeLists.txt | 14 ---
math/cvc4/files/patch-test_system_CMakeLists.txt | 13 ---
math/cvc4/pkg-plist | 111 ----------------------
math/{cvc4 => cvc5}/Makefile | 69 ++++++--------
math/cvc5/distinfo | 7 ++
math/cvc5/files/patch-cmake_FindANTLR3.cmake | 11 +++
math/cvc5/files/patch-cmake_FindEditline.cmake | 11 +++
math/{cvc4 => cvc5}/pkg-descr | 0
math/cvc5/pkg-plist | 16 ++++
21 files changed, 74 insertions(+), 377 deletions(-)
diff --git a/MOVED b/MOVED
index c6ff383b5959..95671d3e34fd 100644
--- a/MOVED
+++ b/MOVED
@@ -17747,3 +17747,4 @@ sysutils/beats6||2023-01-01|Has expired: No longer maintained and supported
sysutils/logstash6||2023-01-01|Has expired: No longer maintained and supported
textproc/elasticsearch6||2023-01-01|Has expired: No longer maintained and supported
japanese/ja-tex-xdvik|print/tex-xdvik|2023-01-02|pTeX support has been integrated
+math/cvc4|math/cvc5|2023-01-03|CVC4 was succeeded by CVC5
diff --git a/math/Makefile b/math/Makefile
index c5b0cf9072d9..cbe924b35d07 100644
--- a/math/Makefile
+++ b/math/Makefile
@@ -264,7 +264,7 @@
SUBDIR += cudd
SUBDIR += curv
SUBDIR += cvc3
- SUBDIR += cvc4
+ SUBDIR += cvc5
SUBDIR += dbcsr
SUBDIR += deal.ii
SUBDIR += dieharder
diff --git a/math/cvc4/distinfo b/math/cvc4/distinfo
deleted file mode 100644
index a16df890b9e7..000000000000
--- a/math/cvc4/distinfo
+++ /dev/null
@@ -1,7 +0,0 @@
-TIMESTAMP = 1559856275
-SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7
-SIZE (antlr-3.4-complete.jar) = 2388361
-SHA256 (CVC4-CVC4-1.7_GH0.tar.gz) = 9864a364a0076ef7ff63a46cdbc69cbe6568604149626338598d4df7788f8c2e
-SIZE (CVC4-CVC4-1.7_GH0.tar.gz) = 6969953
-SHA256 (fc8907afc08d.patch) = b14fe811a91152d9311a48e1c198c82fc55febf0c76c6c8fab6c9d6f0addeb3f
-SIZE (fc8907afc08d.patch) = 1154
diff --git a/math/cvc4/files/patch-cmake_FindANTLR.cmake b/math/cvc4/files/patch-cmake_FindANTLR.cmake
deleted file mode 100644
index ae6462f57e37..000000000000
--- a/math/cvc4/files/patch-cmake_FindANTLR.cmake
+++ /dev/null
@@ -1,13 +0,0 @@
-We fetch 3.4 (since 3.5 breaks it), we don't want it to find
-system antlr3 (3.5) and overwrite our fetched one
-
---- cmake/FindANTLR.cmake.orig 2019-04-09 16:14:31 UTC
-+++ cmake/FindANTLR.cmake
-@@ -27,7 +27,6 @@ find_library(ANTLR_LIBRARIES
- NO_DEFAULT_PATH)
-
- if(CHECK_SYSTEM_VERSION)
-- find_program(ANTLR_BINARY NAMES antlr3)
- find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h)
- find_library(ANTLR_LIBRARIES NAMES antlr3c)
- endif()
diff --git a/math/cvc4/files/patch-cmake_FindReadline.cmake b/math/cvc4/files/patch-cmake_FindReadline.cmake
deleted file mode 100644
index 50c691763f06..000000000000
--- a/math/cvc4/files/patch-cmake_FindReadline.cmake
+++ /dev/null
@@ -1,42 +0,0 @@
-CMAKE_REQUIRED_INCLUDES does not work for some reason,
-the check is compiled without the include path
-
---- cmake/FindReadline.cmake.orig 2019-04-09 16:14:31 UTC
-+++ cmake/FindReadline.cmake
-@@ -13,15 +13,7 @@ find_library(Readline_LIBRARIES NAMES readline)
- function(try_compile_readline libs _result)
- set(CMAKE_REQUIRED_QUIET TRUE)
- set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs})
-- check_cxx_source_compiles(
-- "
-- #include <stdio.h>
-- #include <readline/readline.h>
-- int main() { readline(\"\"); return 0; }
-- "
-- ${_result}
-- )
-- set(${_result} ${${_result}} PARENT_SCOPE)
-+ set(${_result} OK PARENT_SCOPE)
- endfunction()
-
- if(Readline_INCLUDE_DIR)
-@@ -42,18 +34,7 @@ if(Readline_INCLUDE_DIR)
-
- # Check which standard of readline is installed on the system.
- # https://github.com/CVC4/CVC4/issues/702
-- include(CheckCXXSourceCompiles)
-- set(CMAKE_REQUIRED_QUIET TRUE)
-- set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES})
-- check_cxx_source_compiles(
-- "#include <stdio.h>
-- #include <readline/readline.h>
-- char* foo(const char*, int) { return (char*)0; }
-- int main() { rl_completion_entry_function = foo; return 0; }"
-- Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
-- )
-- unset(CMAKE_REQUIRED_QUIET)
-- unset(CMAKE_REQUIRED_LIBRARIES)
-+ set(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR TRUE)
- endif()
-
- include(FindPackageHandleStandardArgs)
diff --git a/math/cvc4/files/patch-doc_CMakeLists.txt b/math/cvc4/files/patch-doc_CMakeLists.txt
deleted file mode 100644
index 764bb44e1d12..000000000000
--- a/math/cvc4/files/patch-doc_CMakeLists.txt
+++ /dev/null
@@ -1,22 +0,0 @@
---- doc/CMakeLists.txt.orig 2019-06-06 21:29:05 UTC
-+++ doc/CMakeLists.txt
-@@ -34,10 +34,10 @@ configure_file(
- #-----------------------------------------------------------------------------#
- # Install man pages
-
--install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1)
--install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5)
-+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1)
-+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION man/man5)
- if(ENABLE_PORTFOLIO)
-- install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1
-+ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1
- RENAME pcvc4.1)
- endif()
- install(FILES
-@@ -45,4 +45,4 @@ install(FILES
- ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3
- ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc
- ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc
-- DESTINATION share/man/man3)
-+ DESTINATION man/man3)
diff --git a/math/cvc4/files/patch-examples_CMakeLists.txt b/math/cvc4/files/patch-examples_CMakeLists.txt
deleted file mode 100644
index 60ccd1f7adbf..000000000000
--- a/math/cvc4/files/patch-examples_CMakeLists.txt
+++ /dev/null
@@ -1,12 +0,0 @@
---- examples/CMakeLists.txt.orig 2019-06-06 19:10:39 UTC
-+++ examples/CMakeLists.txt
-@@ -17,9 +17,6 @@ add_custom_target(examples)
-
- # Create target runexamples.
- # Builds and runs all examples.
--add_custom_target(runexamples
-- COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $(ARGS)
-- DEPENDS examples)
-
- # Add example target and create test to run example with ctest.
- #
diff --git a/math/cvc4/files/patch-src_CMakeLists.txt b/math/cvc4/files/patch-src_CMakeLists.txt
deleted file mode 100644
index a516e618fe82..000000000000
--- a/math/cvc4/files/patch-src_CMakeLists.txt
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/CMakeLists.txt.orig 2019-07-28 18:28:58 UTC
-+++ src/CMakeLists.txt
-@@ -913,6 +913,6 @@ install(FILES
-
- # Fix include paths for all public headers.
- # Note: This is a temporary fix until the new C++ API is in place.
--install(CODE "execute_process(COMMAND
-+install(CODE "execute_process(COMMAND sh
- ${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
-- ${CMAKE_INSTALL_PREFIX})")
-+ \"\$ENV{DESTDIR}\${CMAKE_INSTALL_PREFIX}\")")
diff --git a/math/cvc4/files/patch-src_base_configuration.cpp b/math/cvc4/files/patch-src_base_configuration.cpp
deleted file mode 100644
index 43541f78a272..000000000000
--- a/math/cvc4/files/patch-src_base_configuration.cpp
+++ /dev/null
@@ -1,11 +0,0 @@
---- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC
-+++ src/base/configuration.cpp
-@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() {
- }
-
- std::string Configuration::getCompiledDateTime() {
-- return __DATE__ " " __TIME__;
-+ return "(timestamp removed for reproducible builds)";
- }
-
- }/* CVC4 namespace */
diff --git a/math/cvc4/files/patch-src_main_portfolio.cpp b/math/cvc4/files/patch-src_main_portfolio.cpp
deleted file mode 100644
index 454c9693112c..000000000000
--- a/math/cvc4/files/patch-src_main_portfolio.cpp
+++ /dev/null
@@ -1,24 +0,0 @@
---- src/main/portfolio.cpp.orig 2018-04-22 17:42:48 UTC
-+++ src/main/portfolio.cpp
-@@ -18,6 +18,9 @@
- #include <boost/bind.hpp>
- #include <boost/thread/condition.hpp>
- #include <boost/exception_ptr.hpp>
-+#ifdef __FreeBSD__
-+#include <pthread_np.h>
-+#endif
-
- #include "base/output.h"
- #include "options/options.h"
-@@ -100,7 +103,11 @@ std::pair<int, S> runPortfolio(int numThreads,
- void *stackaddr;
- size_t stacksize;
- pthread_attr_t attr;
-+#ifdef __linux__
- pthread_getattr_np(threads[t].native_handle(), &attr);
-+#elif __FreeBSD__
-+ pthread_attr_get_np(threads[t].native_handle(), &attr);
-+#endif
- pthread_attr_getstack(&attr, &stackaddr, &stacksize);
- Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl;
- }
diff --git a/math/cvc4/files/patch-swig4 b/math/cvc4/files/patch-swig4
deleted file mode 100644
index ca9a8faea594..000000000000
--- a/math/cvc4/files/patch-swig4
+++ /dev/null
@@ -1,40 +0,0 @@
-Obtained from: https://github.com/CVC4/CVC4/commit/c587235d29d2e3e1cd52a9f76dde8f58c89ae37e
-
---- src/bindings/java/CMakeLists.txt.orig 2019-04-09 16:14:31 UTC
-+++ src/bindings/java/CMakeLists.txt
-@@ -131,6 +131,7 @@ set(gen_java_files
- ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java
- ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java
- ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java
-+ ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java
- ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java
- ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java
- ${CMAKE_CURRENT_BINARY_DIR}/Options.java
-@@ -177,7 +178,6 @@ set(gen_java_files
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java
-- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java
- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java
-@@ -210,6 +210,7 @@ set(gen_java_files
- ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java
- ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java
- ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java
-+ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java
- ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java
- ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java
- ${CMAKE_CURRENT_BINARY_DIR}/Timer.java
---- src/smt/smt_engine.i.orig 2019-04-09 16:14:31 UTC
-+++ src/smt/smt_engine.i
-@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acsys_CVC4_SmtEng
- swigCPtr = 0;
- }
- }
-+
-+%template(Map_ExprExpr) std::map<CVC4::Expr, CVC4::Expr>;
-+
- #endif // SWIGJAVA
-
- %ignore CVC4::SmtEngine::setLogic(const char*);
diff --git a/math/cvc4/files/patch-test_CMakeLists.txt b/math/cvc4/files/patch-test_CMakeLists.txt
deleted file mode 100644
index 43d5da2a3df0..000000000000
--- a/math/cvc4/files/patch-test_CMakeLists.txt
+++ /dev/null
@@ -1,14 +0,0 @@
---- test/CMakeLists.txt.orig 2019-06-06 19:12:46 UTC
-+++ test/CMakeLists.txt
-@@ -15,11 +15,6 @@ add_dependencies(build-tests examples)
- # first run the command of the regress target (i.e., run all regression tests)
- # and afterwards run the command specified for the check target.
- # Dependencies of check are added in the corresponding subdirectories.
--add_custom_target(check
-- COMMAND
-- ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $(ARGS)
-- DEPENDS
-- build-tests)
-
- #-----------------------------------------------------------------------------#
- # Add subdirectories
diff --git a/math/cvc4/files/patch-test_regress_CMakeLists.txt b/math/cvc4/files/patch-test_regress_CMakeLists.txt
deleted file mode 100644
index a52d05061534..000000000000
--- a/math/cvc4/files/patch-test_regress_CMakeLists.txt
+++ /dev/null
@@ -1,14 +0,0 @@
---- test/regress/CMakeLists.txt.orig 2019-06-06 19:13:41 UTC
-+++ test/regress/CMakeLists.txt
-@@ -2138,11 +2138,6 @@ set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_r
- add_custom_target(build-regress DEPENDS cvc4-bin)
- add_dependencies(build-tests build-regress)
-
--add_custom_target(regress
-- COMMAND
-- ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $(ARGS)
-- DEPENDS build-regress)
--
- macro(cvc4_add_regression_test level file)
- add_test(${file}
- ${run_regress_script}
diff --git a/math/cvc4/files/patch-test_system_CMakeLists.txt b/math/cvc4/files/patch-test_system_CMakeLists.txt
deleted file mode 100644
index d05dbdc083df..000000000000
--- a/math/cvc4/files/patch-test_system_CMakeLists.txt
+++ /dev/null
@@ -1,13 +0,0 @@
---- test/system/CMakeLists.txt.orig 2019-06-06 19:13:50 UTC
-+++ test/system/CMakeLists.txt
-@@ -10,10 +10,6 @@ include_directories(${CMAKE_BINARY_DIR}/src)
- add_custom_target(build-systemtests)
- add_dependencies(build-tests build-systemtests)
-
--add_custom_target(systemtests
-- COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $(ARGS)
-- DEPENDS build-systemtests)
--
- set(CVC4_SYSTEM_TEST_FLAGS
- -D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
-
diff --git a/math/cvc4/pkg-plist b/math/cvc4/pkg-plist
deleted file mode 100644
index 9a057af977ee..000000000000
--- a/math/cvc4/pkg-plist
+++ /dev/null
@@ -1,111 +0,0 @@
-bin/cvc4
-%%GMP%%bin/pcvc4
-include/cvc4/api/cvc4cpp.h
-include/cvc4/api/cvc4cppkind.h
-include/cvc4/base/configuration.h
-include/cvc4/base/exception.h
-include/cvc4/base/listener.h
-include/cvc4/base/modal_exception.h
-include/cvc4/context/cdhashmap_forward.h
-include/cvc4/context/cdhashset_forward.h
-include/cvc4/context/cdinsert_hashmap_forward.h
-include/cvc4/context/cdlist_forward.h
-include/cvc4/cvc4.h
-include/cvc4/cvc4_public.h
-include/cvc4/cvc4parser_public.h
-include/cvc4/expr/array.h
-include/cvc4/expr/array_store_all.h
-include/cvc4/expr/ascription_type.h
-include/cvc4/expr/chain.h
-include/cvc4/expr/datatype.h
-include/cvc4/expr/emptyset.h
-include/cvc4/expr/expr.h
-include/cvc4/expr/expr_iomanip.h
-include/cvc4/expr/expr_manager.h
-include/cvc4/expr/expr_stream.h
-include/cvc4/expr/kind.h
-include/cvc4/expr/pickler.h
-include/cvc4/expr/record.h
-include/cvc4/expr/symbol_table.h
-include/cvc4/expr/type.h
-include/cvc4/expr/uninterpreted_constant.h
-include/cvc4/expr/variable_type_map.h
-include/cvc4/options/argument_extender.h
-include/cvc4/options/arith_heuristic_pivot_rule.h
-include/cvc4/options/arith_propagation_mode.h
-include/cvc4/options/arith_unate_lemma_mode.h
-include/cvc4/options/datatypes_modes.h
-include/cvc4/options/language.h
-include/cvc4/options/option_exception.h
-include/cvc4/options/options.h
-include/cvc4/options/printer_modes.h
-include/cvc4/options/quantifiers_modes.h
-include/cvc4/options/set_language.h
-include/cvc4/options/smt_modes.h
-include/cvc4/options/sygus_out_mode.h
-include/cvc4/options/theoryof_mode.h
-include/cvc4/parser/input.h
-include/cvc4/parser/parser.h
-include/cvc4/parser/parser_builder.h
-include/cvc4/parser/parser_exception.h
-include/cvc4/printer/sygus_print_callback.h
-include/cvc4/proof/unsat_core.h
-include/cvc4/smt/command.h
-include/cvc4/smt/logic_exception.h
-include/cvc4/smt/smt_engine.h
-include/cvc4/smt_util/lemma_channels.h
-include/cvc4/smt_util/lemma_input_channel.h
-include/cvc4/smt_util/lemma_output_channel.h
-include/cvc4/theory/logic_info.h
-include/cvc4/util/abstract_value.h
-include/cvc4/util/bitvector.h
-include/cvc4/util/bool.h
-include/cvc4/util/cardinality.h
-include/cvc4/util/channel.h
-include/cvc4/util/divisible.h
-include/cvc4/util/floatingpoint.h
-include/cvc4/util/gmp_util.h
-include/cvc4/util/hash.h
-include/cvc4/util/integer.h
-include/cvc4/util/integer_cln_imp.h
-include/cvc4/util/integer_gmp_imp.h
-include/cvc4/util/maybe.h
-include/cvc4/util/proof.h
-include/cvc4/util/rational.h
-include/cvc4/util/rational_cln_imp.h
-include/cvc4/util/rational_gmp_imp.h
-include/cvc4/util/regexp.h
-include/cvc4/util/resource_manager.h
-include/cvc4/util/result.h
-include/cvc4/util/sexpr.h
-include/cvc4/util/statistics.h
-include/cvc4/util/tuple.h
-include/cvc4/util/unsafe_interrupt_exception.h
-lib/libcvc4.so
-lib/libcvc4.so.6
-%%JAVA%%lib/libcvc4jni.so
-lib/libcvc4parser.so
-lib/libcvc4parser.so.6
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/CVC4.py
-%%PYTHON%%%%PYTHON_SITELIBDIR%%/_CVC4.so
-%%DATADIR%%/drat.plf
-%%DATADIR%%/er.plf
-%%DATADIR%%/lrat.plf
-%%DATADIR%%/sat.plf
-%%DATADIR%%/smt.plf
-%%DATADIR%%/th_arrays.plf
-%%DATADIR%%/th_base.plf
-%%DATADIR%%/th_bv.plf
-%%DATADIR%%/th_bv_bitblast.plf
-%%DATADIR%%/th_bv_rewrites.plf
-%%DATADIR%%/th_int.plf
-%%DATADIR%%/th_real.plf
-%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4-1.7.0.jar
-%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4.jar
-man/man1/cvc4.1.gz
-%%GMP%%man/man1/pcvc4.1.gz
-man/man3/SmtEngine.3cvc.gz
-man/man3/libcvc4.3.gz
-man/man3/libcvc4parser.3.gz
-man/man3/options.3cvc.gz
-man/man5/cvc4.5.gz
diff --git a/math/cvc4/Makefile b/math/cvc5/Makefile
similarity index 51%
rename from math/cvc4/Makefile
rename to math/cvc5/Makefile
index cf288551b284..8820265fccca 100644
--- a/math/cvc4/Makefile
+++ b/math/cvc5/Makefile
@@ -1,54 +1,46 @@
-PORTNAME= cvc4
-DISTVERSION= 1.7
-PORTREVISION= 6
+PORTNAME= cvc5
+DISTVERSIONPREFIX= cvc5-
+DISTVERSION= 1.0.3
CATEGORIES= math java
MASTER_SITES+= http://www.antlr3.org/download/:antlr3
DISTFILES+= antlr-3.4-complete.jar:antlr3
EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
-PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/
-PATCHFILES+= fc8907afc08d.patch:-p1 # Install Java bindings
-
-MAINTAINER= ports@FreeBSD.org
+MAINTAINER= yuri@FreeBSD.org
COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)
-WWW= https://cvc4.cs.stanford.edu/web/
+WWW= https://cvc5.github.io/
LICENSE= BSD3CLAUSE
LICENSE_FILE= ${WRKSRC}/COPYING
-BROKEN= Doesn't build, src/expr/expr_template.h:0: error: undefined replacement ${getConst_instantiations}
-
-BUILD_DEPENDS= bash:shells/bash
+BUILD_DEPENDS= bash:shells/bash \
+ ${LOCALBASE}/lib/libcadical.a:math/cadical \
+ ${LOCALBASE}/lib/symfpu.a:math/symfpu \
+ ${PYTHON_PKGNAMEPREFIX}toml>0:textproc/py-toml@${PY_FLAVOR}
LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \
libboost_system.so:devel/boost-libs
USES= cmake ncurses compiler:c++17-lang \
- pkgconfig python:3.5+,build shebangfix
-
-SHEBANG_FILES= src/base/mktagheaders \
- src/base/mktags
-
+ localbase:ldflags pkgconfig python:3.5+,build
+USE_LDCONFIG= yes
USE_GITHUB= yes
-GH_ACCOUNT= CVC4
-GH_PROJECT= CVC4
USE_JAVA= yes
JAVA_BUILD= yes
-USE_LDCONFIG= yes
-
CMAKE_BUILD_TYPE= Production
-CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3
+CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 \
+ -DFREEBSD_DISTDIR=${DISTDIR}
+CMAKE_ON= BUILD_SHARED_LIBS
+CMAKE_OFF= BUILD_BINDINGS_PYTHON USE_PYTHON3 # Python binding should be a separate port
-OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE
+OPTIONS_DEFINE= CRYPTOMINISAT JAVA EDITLINE
OPTIONS_RADIO= NUMLIB
OPTIONS_RADIO_NUMLIB= GMP CLN
-OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE GMP
+OPTIONS_DEFAULT= CRYPTOMINISAT JAVA EDITLINE GMP
OPTIONS_SUB= yes
CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver
-GMP_DESC= Use GMP numeric library
-CLN_DESC= Use CLN numeric library (disables portfolio mode)
CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT
CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat
@@ -59,25 +51,22 @@ JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \
-DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so
JAVA_BUILD_DEPENDS= swig:devel/swig
-PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3
-PYTHON_BUILD_DEPENDS= swig:devel/swig
-
-READLINE_CMAKE_BOOL= USE_READLINE
-READLINE_USES= readline
+EDITLINE_DESC= Use Editline for better interactive support
+EDITLINE_CMAKE_BOOL= USE_EDITLINE
+EDITLINE_BUILD_DEPENDS= libedit>0:devel/libedit
+EDITLINE_RUN_DEPENDS= libedit>0:devel/libedit
-GMP_CMAKE_BOOL= ENABLE_PORTFOLIO
-GMP_CMAKE_ON= -DENABLE_DUMPING=OFF
-GMP_LIB_DEPENDS= libgmp.so:math/gmp \
- libboost_thread.so:devel/boost-libs
-# note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies
+GMP_DESC= Use GMP numeric library
+GMP_LIB_DEPENDS= libgmp.so:math/gmp
+CLN_DESC= Use CLN numeric library
CLN_CMAKE_BOOL= USE_CLN
CLN_LIB_DEPENDS= libcln.so:math/cln \
libgmp.so:math/gmp
.include <bsd.port.options.mk>
-.if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN}
+.if ${PORT_OPTIONS:MCLN}
LICENSE= GPLv3
CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON
.endif
@@ -89,11 +78,7 @@ post-extract:
@${CHMOD} +x ${WRKDIR}/antlr3
post-patch:
- @${REINPLACE_CMD} -e "s|sed -i 's|sed -i '' 's|g" \
- ${WRKSRC}/src/fix-install-headers.sh
-
-# make a relative symlink instead of absolute to build dir
-post-install-JAVA-on:
- @${LN} -sf CVC4-1.7.0.jar ${STAGEDIR}${PREFIX}/share/java/cvc4/CVC4.jar
+ @${REINPLACE_CMD} -e "s|sed -i'' -e 's|sed -i '' -e 's|g" \
+ ${WRKSRC}/src/fix-install-headers.sh
.include <bsd.port.mk>
diff --git a/math/cvc5/distinfo b/math/cvc5/distinfo
new file mode 100644
index 000000000000..76743a798912
--- /dev/null
+++ b/math/cvc5/distinfo
@@ -0,0 +1,7 @@
+TIMESTAMP = 1672779263
+SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7
+SIZE (antlr-3.4-complete.jar) = 2388361
+SHA256 (cvc5-cvc5-cvc5-1.0.3_GH0.tar.gz) = bf787b74c35ef61958865902e21dcb8f98f79d910b00a9e762a00ff8fcd2c462
+SIZE (cvc5-cvc5-cvc5-1.0.3_GH0.tar.gz) = 8335175
+SHA256 (fc8907afc08d.patch) = dfb42f7c9fbc4091d21ce4804f11c72945ccc9131f3d79dbc275fd9238ff55d4
+SIZE (fc8907afc08d.patch) = 1156
diff --git a/math/cvc5/files/patch-cmake_FindANTLR3.cmake b/math/cvc5/files/patch-cmake_FindANTLR3.cmake
new file mode 100644
index 000000000000..4af6273f9f53
--- /dev/null
+++ b/math/cvc5/files/patch-cmake_FindANTLR3.cmake
@@ -0,0 +1,11 @@
+--- cmake/FindANTLR3.cmake.orig 2022-12-12 22:42:47 UTC
++++ cmake/FindANTLR3.cmake
+@@ -18,7 +18,7 @@
+
+ include(deps-helper)
+
+-find_file(ANTLR3_JAR NAMES antlr-3.4-complete.jar PATH_SUFFIXES share/java/)
++set(ANTLR3_JAR ${FREEBSD_DISTDIR}/antlr-3.4-complete.jar)
+ find_path(ANTLR3_INCLUDE_DIR NAMES antlr3.h)
+ find_library(ANTLR3_LIBRARIES NAMES antlr3c)
+
diff --git a/math/cvc5/files/patch-cmake_FindEditline.cmake b/math/cvc5/files/patch-cmake_FindEditline.cmake
new file mode 100644
index 000000000000..a8d897cd7b95
--- /dev/null
+++ b/math/cvc5/files/patch-cmake_FindEditline.cmake
@@ -0,0 +1,11 @@
+--- cmake/FindEditline.cmake.orig 2023-01-04 10:29:29 UTC
++++ cmake/FindEditline.cmake
+@@ -41,7 +41,7 @@ if(Editline_INCLUDE_DIRS)
+ unset(CMAKE_REQUIRED_LIBRARIES)
+ unset(CMAKE_REQUIRED_INCLUDES)
+
+- if(NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
++ if(FALSE AND NOT CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+ set(Editline_LIBRARIES ${Editline_LIBRARIES} bsd tinfo)
+ endif()
+ endif()
diff --git a/math/cvc4/pkg-descr b/math/cvc5/pkg-descr
similarity index 100%
rename from math/cvc4/pkg-descr
rename to math/cvc5/pkg-descr
diff --git a/math/cvc5/pkg-plist b/math/cvc5/pkg-plist
new file mode 100644
index 000000000000..75d440acfa8e
--- /dev/null
+++ b/math/cvc5/pkg-plist
@@ -0,0 +1,16 @@
+bin/cvc5
+include/cvc5/cvc5.h
+include/cvc5/cvc5_export.h
+include/cvc5/cvc5_kind.h
+include/cvc5/cvc5_types.h
+lib/cmake/cvc5/cvc5Config.cmake
+lib/cmake/cvc5/cvc5ConfigVersion.cmake
+lib/cmake/cvc5/cvc5JavaTargets.cmake
+lib/cmake/cvc5/cvc5Targets-%%CMAKE_BUILD_TYPE%%.cmake
+lib/cmake/cvc5/cvc5Targets.cmake
+lib/libcvc5.so
+%%JAVA%%lib/libcvc5jni.so
+lib/libcvc5parser.so
+lib/libcvc5parser.so.1
+%%JAVA%%%%JAVASHAREDIR%%/cvc5-1.0.3.jar
+%%JAVA%%%%JAVASHAREDIR%%/cvc5.jar