Date: Thu, 1 Aug 2019 15:20:28 +0000 (UTC) From: =?UTF-8?Q?Fernando_Apestegu=c3=ada?= <fernape@FreeBSD.org> To: ports-committers@freebsd.org, svn-ports-all@freebsd.org, svn-ports-head@freebsd.org Subject: svn commit: r507774 - in head/math/cvc4: . files Message-ID: <201908011520.x71FKSXe065377@repo.freebsd.org>
next in thread | raw e-mail | index | archive | help
Author: fernape Date: Thu Aug 1 15:20:28 2019 New Revision: 507774 URL: https://svnweb.freebsd.org/changeset/ports/507774 Log: math/cvc4: update to 1.7 ChangeLog: https://github.com/CVC4/CVC4/releases/tag/1.7 * New Features: Proofs: Support for bit-vector proofs with eager bitblasting Strings: Support for str.replaceall operator. New option --re-elim SyGuS: Support for abduction (--sygus-abduct) * Improvements: Strings: Significantly better performance * Changes: API change: Expr::iffExpr() is renamed to Expr::eqExpr() Compiling the language bindings now requires SWIG 3 instead of SWIG 2. The CVC3 compatibility layer has been removed. The build system now uses CMake instead of Autotools Added: head/math/cvc4/files/patch-cmake_FindANTLR.cmake (contents, props changed) head/math/cvc4/files/patch-cmake_FindReadline.cmake (contents, props changed) head/math/cvc4/files/patch-doc_CMakeLists.txt (contents, props changed) head/math/cvc4/files/patch-examples_CMakeLists.txt (contents, props changed) head/math/cvc4/files/patch-src_CMakeLists.txt (contents, props changed) head/math/cvc4/files/patch-test_CMakeLists.txt (contents, props changed) head/math/cvc4/files/patch-test_regress_CMakeLists.txt (contents, props changed) head/math/cvc4/files/patch-test_system_CMakeLists.txt (contents, props changed) Deleted: head/math/cvc4/files/patch-config_cryptominisat.m4 head/math/cvc4/files/patch-configure.ac Modified: head/math/cvc4/Makefile head/math/cvc4/distinfo head/math/cvc4/files/patch-src_base_configuration.cpp head/math/cvc4/pkg-plist Modified: head/math/cvc4/Makefile ============================================================================== --- head/math/cvc4/Makefile Thu Aug 1 14:32:41 2019 (r507773) +++ head/math/cvc4/Makefile Thu Aug 1 15:20:28 2019 (r507774) @@ -1,76 +1,93 @@ # $FreeBSD$ PORTNAME= cvc4 -DISTVERSION= 1.6 -PORTREVISION= 5 +DISTVERSION= 1.7 CATEGORIES= math java -MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/ +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= greg@unrelenting.technology COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) LICENSE= BSD3CLAUSE LICENSE_FILE= ${WRKSRC}/COPYING +BUILD_DEPENDS= bash:shells/bash LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ libboost_system.so:devel/boost-libs -BUILD_DEPENDS= bash:shells/bash \ - antlr3:devel/antlr3 -USES= autoreconf compiler:c++17-lang gmake libtool localbase \ +USES= cmake ncurses compiler:c++17-lang \ pkgconfig python:3.5+,build shebangfix + +SHEBANG_FILES= src/base/mktagheaders \ + src/base/mktags + +USE_GITHUB= yes +GH_ACCOUNT= CVC4 +GH_PROJECT= CVC4 + USE_JAVA= yes JAVA_BUILD= yes -GNU_CONFIGURE= yes -CONFIGURE_ARGS+= --disable-dependency-tracking \ - --with-swig=${LOCALBASE}/bin/swig3.0 \ - ANTLR=${LOCALBASE}/bin/antlr3 -CONFIGURE_SHELL= ${LOCALBASE}/bin/bash USE_LDCONFIG= yes -SHEBANG_FILES= src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression.py -OPTIONS_DEFINE= CRYPTOMINISAT JAVA READLINE DEBUG +CMAKE_BUILD_TYPE= Production +CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3 + +OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE OPTIONS_RADIO= NUMLIB OPTIONS_RADIO_NUMLIB= GMP CLN -OPTIONS_DEFAULT= CRYPTOMINISAT READLINE GMP +OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE 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_CONFIGURE_ON= --with-cryptominisat --with-cryptominisat-dir=${LOCALBASE} +CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat -JAVA_CONFIGURE_ON= --enable-language-bindings=c,c++,java \ - JAVA_CPPFLAGS="-I${JAVA_HOME}/include -I${JAVA_HOME}/include/freebsd" \ - JAVAC=${JAVAC} JAVAH=${JAVAH} JAR=${JAR} -JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++ -JAVA_BUILD_DEPENDS= swig3.0:devel/swig30 +JAVA_CMAKE_BOOL= BUILD_BINDINGS_JAVA +JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \ + -DJAVA_AWT_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ARCH}/libjawt.so \ + -DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so +JAVA_BUILD_DEPENDS= swig3.0:devel/swig30 -READLINE_CONFIGURE_WITH= readline -READLINE_USES= readline +PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3 +PYTHON_BUILD_DEPENDS= swig3.0:devel/swig30 -GMP_CONFIGURE_WITH= gmp -GMP_CONFIGURE_ON= --with-portfolio -GMP_LIB_DEPENDS= libgmp.so:math/gmp \ - libboost_thread.so:devel/boost-libs +READLINE_CMAKE_BOOL= USE_READLINE +READLINE_USES= readline:port + +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 -CLN_CONFIGURE_WITH= cln -CLN_LIB_DEPENDS= libcln.so:math/cln \ - libgmp.so:math/gmp +CLN_CMAKE_BOOL= USE_CLN +CLN_LIB_DEPENDS= libcln.so:math/cln \ + libgmp.so:math/gmp -DEBUG_CONFIGURE_ON= --with-build=debug -DEBUG_CONFIGURE_OFF= --with-build=production -DEBUG_INSTALL_TARGET_OFF= install-strip - .include <bsd.port.options.mk> .if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN} LICENSE= GPLv3 -CONFIGURE_ARGS+= --enable-gpl +CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON .endif + +post-extract: + @${CP} ${DISTDIR}/antlr-3.4-complete.jar ${WRKDIR}/antlr3.jar + @${ECHO_CMD} "#!/bin/sh" > ${WRKDIR}/antlr3 + @${ECHO_CMD} "JAVA_VERSION=1.7+ exec \"${LOCALBASE}/bin/java\" -classpath \"${WRKDIR}/antlr3.jar\" org.antlr.Tool \"\$$@\"" >> ${WRKDIR}/antlr3 + @${CHMOD} +x ${WRKDIR}/antlr3 + +# 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 .include <bsd.port.mk> Modified: head/math/cvc4/distinfo ============================================================================== --- head/math/cvc4/distinfo Thu Aug 1 14:32:41 2019 (r507773) +++ head/math/cvc4/distinfo Thu Aug 1 15:20:28 2019 (r507774) @@ -1,3 +1,7 @@ -TIMESTAMP = 1531429558 -SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7 -SIZE (cvc4-1.6.tar.gz) = 7815893 +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 Added: head/math/cvc4/files/patch-cmake_FindANTLR.cmake ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-cmake_FindANTLR.cmake Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,13 @@ +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() Added: head/math/cvc4/files/patch-cmake_FindReadline.cmake ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-cmake_FindReadline.cmake Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,42 @@ +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) Added: head/math/cvc4/files/patch-doc_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-doc_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,22 @@ +--- 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) Added: head/math/cvc4/files/patch-examples_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-examples_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,12 @@ +--- 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. + # Added: head/math/cvc4/files/patch-src_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-src_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,11 @@ +--- 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}\")") Modified: head/math/cvc4/files/patch-src_base_configuration.cpp ============================================================================== --- head/math/cvc4/files/patch-src_base_configuration.cpp Thu Aug 1 14:32:41 2019 (r507773) +++ head/math/cvc4/files/patch-src_base_configuration.cpp Thu Aug 1 15:20:28 2019 (r507774) @@ -1,6 +1,6 @@ ---- src/base/configuration.cpp.orig 2018-06-25 21:13:17 UTC +--- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC +++ src/base/configuration.cpp -@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() { +@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() { } std::string Configuration::getCompiledDateTime() { Added: head/math/cvc4/files/patch-test_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-test_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,14 @@ +--- 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 Added: head/math/cvc4/files/patch-test_regress_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-test_regress_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,14 @@ +--- 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} Added: head/math/cvc4/files/patch-test_system_CMakeLists.txt ============================================================================== --- /dev/null 00:00:00 1970 (empty, because file is newly added) +++ head/math/cvc4/files/patch-test_system_CMakeLists.txt Thu Aug 1 15:20:28 2019 (r507774) @@ -0,0 +1,13 @@ +--- 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) + Modified: head/math/cvc4/pkg-plist ============================================================================== --- head/math/cvc4/pkg-plist Thu Aug 1 14:32:41 2019 (r507773) +++ head/math/cvc4/pkg-plist Thu Aug 1 15:20:28 2019 (r507774) @@ -1,23 +1,17 @@ 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/base/tls.h -include/cvc4/bindings/compat/c/c_interface.h -include/cvc4/bindings/compat/c/c_interface_defs.h -include/cvc4/compat/cvc3_compat.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/context/cdtrail_hashmap_forward.h include/cvc4/cvc4.h -include/cvc4/cvc4_private.h -include/cvc4/cvc4_private_library.h include/cvc4/cvc4_public.h -include/cvc4/cvc4parser_private.h include/cvc4/cvc4parser_public.h include/cvc4/expr/array.h include/cvc4/expr/array_store_all.h @@ -28,11 +22,8 @@ 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_manager_template.h include/cvc4/expr/expr_stream.h -include/cvc4/expr/expr_template.h include/cvc4/expr/kind.h -include/cvc4/expr/kind_template.h include/cvc4/expr/pickler.h include/cvc4/expr/record.h include/cvc4/expr/symbol_table.h @@ -50,7 +41,7 @@ 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/simplification_mode.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 @@ -66,7 +57,6 @@ 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/theory/theory_test_utils.h include/cvc4/util/abstract_value.h include/cvc4/util/bitvector.h include/cvc4/util/bool.h @@ -91,32 +81,16 @@ include/cvc4/util/sexpr.h include/cvc4/util/statistics.h include/cvc4/util/tuple.h include/cvc4/util/unsafe_interrupt_exception.h -%%JAVA%%lib/jni/libcvc4compatjni.so -%%JAVA%%lib/jni/libcvc4compatjni.so.5 -%%JAVA%%lib/jni/libcvc4compatjni.so.5.0.0 -%%JAVA%%lib/jni/libcvc4jni.so -%%JAVA%%lib/jni/libcvc4jni.so.5 -%%JAVA%%lib/jni/libcvc4jni.so.5.0.0 lib/libcvc4.so -lib/libcvc4.so.5 -lib/libcvc4.so.5.0.0 -lib/libcvc4bindings_c_compat.so -lib/libcvc4bindings_c_compat.so.5 -lib/libcvc4bindings_c_compat.so.5.0.0 -lib/libcvc4compat.so -lib/libcvc4compat.so.5 -lib/libcvc4compat.so.5.0.0 +lib/libcvc4.so.6 +%%JAVA%%lib/libcvc4jni.so lib/libcvc4parser.so -lib/libcvc4parser.so.5 -lib/libcvc4parser.so.5.0.0 -man/man1/cvc4.1.gz -%%GMP%%man/man1/pcvc4.1.gz -man/man3/SmtEngine.3cvc.gz -man/man3/libcvc4.3.gz -man/man3/libcvc4compat.3.gz -man/man3/libcvc4parser.3.gz -man/man3/options.3cvc.gz -man/man5/cvc4.5.gz +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 @@ -126,5 +100,12 @@ man/man5/cvc4.5.gz %%DATADIR%%/th_bv_rewrites.plf %%DATADIR%%/th_int.plf %%DATADIR%%/th_real.plf -%%JAVA%%share/java/CVC4.jar -%%JAVA%%share/java/CVC4compat.jar +%%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
Want to link to this message? Use this URL: <https://mail-archive.FreeBSD.org/cgi/mid.cgi?201908011520.x71FKSXe065377>