diff options
Diffstat (limited to 'math')
-rw-r--r-- | math/cvc4/Makefile | 26 | ||||
-rw-r--r-- | math/cvc4/distinfo | 6 | ||||
-rw-r--r-- | math/cvc4/files/patch-config_cryptominisat.m4 | 31 | ||||
-rw-r--r-- | math/cvc4/files/patch-configure.ac | 11 | ||||
-rw-r--r-- | math/cvc4/files/patch-src_base_configuration.cpp | 4 | ||||
-rw-r--r-- | math/cvc4/pkg-plist | 32 |
6 files changed, 79 insertions, 31 deletions
diff --git a/math/cvc4/Makefile b/math/cvc4/Makefile index 426e951f4c72..1ecc3536275c 100644 --- a/math/cvc4/Makefile +++ b/math/cvc4/Makefile @@ -1,7 +1,7 @@ # $FreeBSD$ PORTNAME= cvc4 -PORTVERSION= 1.5 +DISTVERSION= 1.6 CATEGORIES= math java MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/ @@ -13,11 +13,10 @@ LICENSE_FILE= ${WRKSRC}/COPYING LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \ libboost_system.so:devel/boost-libs -BUILD_DEPENDS= gexpr:sysutils/coreutils \ - bash:shells/bash \ +BUILD_DEPENDS= bash:shells/bash \ antlr3:devel/antlr3 -USES= compiler:c++11-lang pkgconfig gmake libtool shebangfix localbase +USES= autoreconf compiler:c++11-lang gmake python:3.5+,build libtool localbase pkgconfig shebangfix USE_JAVA= yes JAVA_BUILD= yes @@ -27,17 +26,21 @@ CONFIGURE_ARGS+= --disable-dependency-tracking \ 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 +SHEBANG_FILES= src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression.py -OPTIONS_DEFINE= JAVA READLINE DEBUG +OPTIONS_DEFINE= CRYPTOMINISAT JAVA READLINE DEBUG OPTIONS_RADIO= NUMLIB OPTIONS_RADIO_NUMLIB= GMP CLN -OPTIONS_DEFAULT= READLINE GMP +OPTIONS_DEFAULT= CRYPTOMINISAT 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_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} @@ -61,9 +64,6 @@ DEBUG_CONFIGURE_ON= --with-build=debug DEBUG_CONFIGURE_OFF= --with-build=production DEBUG_INSTALL_TARGET_OFF= install-strip -post-patch: - ${REINPLACE_CMD} -e 's|expr |gexpr |g' ${WRKSRC}/src/options/mkoptions - .include <bsd.port.options.mk> .if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN} @@ -71,4 +71,10 @@ LICENSE= GPLv3 CONFIGURE_ARGS+= --enable-gpl .endif +# use the fixed compiler version from ports to prevent failures on FreeBSD_10 +LLVM_VERSION= 60 +BUILD_DEPENDS+= clang${LLVM_VERSION}:devel/llvm${LLVM_VERSION} +CC= clang${LLVM_VERSION} +CXX= clang++${LLVM_VERSION} + .include <bsd.port.mk> diff --git a/math/cvc4/distinfo b/math/cvc4/distinfo index 579934f7d6c3..a251931aa151 100644 --- a/math/cvc4/distinfo +++ b/math/cvc4/distinfo @@ -1,3 +1,3 @@ -TIMESTAMP = 1524235369 -SHA256 (cvc4-1.5.tar.gz) = 5d6b4f8ee8420f85e3f804181341cedf6ea32342c48f355a5be87754152b14e9 -SIZE (cvc4-1.5.tar.gz) = 8059968 +TIMESTAMP = 1531429558 +SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7 +SIZE (cvc4-1.6.tar.gz) = 7815893 diff --git a/math/cvc4/files/patch-config_cryptominisat.m4 b/math/cvc4/files/patch-config_cryptominisat.m4 new file mode 100644 index 000000000000..96985b4b41d7 --- /dev/null +++ b/math/cvc4/files/patch-config_cryptominisat.m4 @@ -0,0 +1,31 @@ +--- config/cryptominisat.m4.orig 2018-07-12 21:34:02 UTC ++++ config/cryptominisat.m4 +@@ -36,7 +36,7 @@ elif test -n "$with_cryptominisat"; then + AC_MSG_RESULT([no]) + fi + +- if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat5_simple" ; then ++ if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/bin/cryptominisat5_simple" ; then + AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built]) + fi + +@@ -54,7 +54,7 @@ elif test -n "$with_cryptominisat"; then + have_libcryptominisat=1 + fi + +- CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" ++ CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/lib" + + else + AC_MSG_RESULT([no, user didn't request cryptominisat]) +@@ -74,8 +74,8 @@ if test -z "$CRYPTOMINISAT_LIBS"; then + cvc4_save_LDFLAGS="$LDFLAGS" + cvc4_save_CPPFLAGS="$CPPFLAGS" + +- LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib" +- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include" ++ LDFLAGS="-L$CRYPTOMINISAT_HOME/lib" ++ CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/include" + LIBS="-lcryptominisat5 $1" + + AC_LINK_IFELSE( diff --git a/math/cvc4/files/patch-configure.ac b/math/cvc4/files/patch-configure.ac new file mode 100644 index 000000000000..b4177f36639f --- /dev/null +++ b/math/cvc4/files/patch-configure.ac @@ -0,0 +1,11 @@ +--- configure.ac.orig 2018-07-12 21:33:27 UTC ++++ configure.ac +@@ -913,7 +913,7 @@ AC_ARG_WITH([cryptominisat], + CVC4_CHECK_FOR_CRYPTOMINISAT + if test $have_libcryptominisat -eq 1; then + CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT" +- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include" ++ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include" + fi + AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1]) + AC_SUBST([CRYPTOMINISAT_LDFLAGS]) diff --git a/math/cvc4/files/patch-src_base_configuration.cpp b/math/cvc4/files/patch-src_base_configuration.cpp index 6e48c9e5c562..4206b023799e 100644 --- a/math/cvc4/files/patch-src_base_configuration.cpp +++ b/math/cvc4/files/patch-src_base_configuration.cpp @@ -1,6 +1,6 @@ ---- src/base/configuration.cpp.orig 2018-04-22 17:53:43 UTC +--- src/base/configuration.cpp.orig 2018-06-25 21:13:17 UTC +++ src/base/configuration.cpp -@@ -291,7 +291,7 @@ std::string Configuration::getCompiler() { +@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() { } std::string Configuration::getCompiledDateTime() { diff --git a/math/cvc4/pkg-plist b/math/cvc4/pkg-plist index a7758f76b670..4c8bb1c64da8 100644 --- a/math/cvc4/pkg-plist +++ b/math/cvc4/pkg-plist @@ -1,11 +1,9 @@ bin/cvc4 -bin/lfsc-checker %%GMP%%bin/pcvc4 include/cvc4/base/configuration.h include/cvc4/base/exception.h include/cvc4/base/listener.h include/cvc4/base/modal_exception.h -include/cvc4/base/ptr_closer.h include/cvc4/base/tls.h include/cvc4/bindings/compat/c/c_interface.h include/cvc4/bindings/compat/c/c_interface_defs.h @@ -36,7 +34,6 @@ 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/predicate.h include/cvc4/expr/record.h include/cvc4/expr/symbol_table.h include/cvc4/expr/type.h @@ -46,6 +43,7 @@ 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 @@ -53,11 +51,13 @@ 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/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 @@ -79,6 +79,7 @@ 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 @@ -88,27 +89,26 @@ include/cvc4/util/resource_manager.h include/cvc4/util/result.h include/cvc4/util/sexpr.h include/cvc4/util/statistics.h -include/cvc4/util/subrange_bound.h include/cvc4/util/tuple.h include/cvc4/util/unsafe_interrupt_exception.h %%JAVA%%lib/jni/libcvc4compatjni.so -%%JAVA%%lib/jni/libcvc4compatjni.so.4 -%%JAVA%%lib/jni/libcvc4compatjni.so.4.0.0 +%%JAVA%%lib/jni/libcvc4compatjni.so.5 +%%JAVA%%lib/jni/libcvc4compatjni.so.5.0.0 %%JAVA%%lib/jni/libcvc4jni.so -%%JAVA%%lib/jni/libcvc4jni.so.4 -%%JAVA%%lib/jni/libcvc4jni.so.4.0.0 +%%JAVA%%lib/jni/libcvc4jni.so.5 +%%JAVA%%lib/jni/libcvc4jni.so.5.0.0 lib/libcvc4.so -lib/libcvc4.so.4 -lib/libcvc4.so.4.0.0 +lib/libcvc4.so.5 +lib/libcvc4.so.5.0.0 lib/libcvc4bindings_c_compat.so -lib/libcvc4bindings_c_compat.so.4 -lib/libcvc4bindings_c_compat.so.4.0.0 +lib/libcvc4bindings_c_compat.so.5 +lib/libcvc4bindings_c_compat.so.5.0.0 lib/libcvc4compat.so -lib/libcvc4compat.so.4 -lib/libcvc4compat.so.4.0.0 +lib/libcvc4compat.so.5 +lib/libcvc4compat.so.5.0.0 lib/libcvc4parser.so -lib/libcvc4parser.so.4 -lib/libcvc4parser.so.4.0.0 +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 |