Index: head/math/cvc4/Makefile =================================================================== --- head/math/cvc4/Makefile (revision 475114) +++ head/math/cvc4/Makefile (revision 475115) @@ -1,74 +1,80 @@ # $FreeBSD$ PORTNAME= cvc4 -PORTVERSION= 1.5 +DISTVERSION= 1.6 CATEGORIES= math java MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/ MAINTAINER= greg@unrelenting.technology COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories) LICENSE= BSD3CLAUSE 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 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 +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} JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++ JAVA_BUILD_DEPENDS= swig3.0:devel/swig30 READLINE_CONFIGURE_WITH= readline READLINE_USES= readline GMP_CONFIGURE_WITH= gmp GMP_CONFIGURE_ON= --with-portfolio 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 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 .if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN} 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 Index: head/math/cvc4/distinfo =================================================================== --- head/math/cvc4/distinfo (revision 475114) +++ head/math/cvc4/distinfo (revision 475115) @@ -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 Index: head/math/cvc4/files/patch-config_cryptominisat.m4 =================================================================== --- head/math/cvc4/files/patch-config_cryptominisat.m4 (nonexistent) +++ head/math/cvc4/files/patch-config_cryptominisat.m4 (revision 475115) @@ -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( Property changes on: head/math/cvc4/files/patch-config_cryptominisat.m4 ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/math/cvc4/files/patch-configure.ac =================================================================== --- head/math/cvc4/files/patch-configure.ac (nonexistent) +++ head/math/cvc4/files/patch-configure.ac (revision 475115) @@ -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]) Property changes on: head/math/cvc4/files/patch-configure.ac ___________________________________________________________________ Added: fbsd:nokeywords ## -0,0 +1 ## +yes \ No newline at end of property Added: svn:eol-style ## -0,0 +1 ## +native \ No newline at end of property Added: svn:mime-type ## -0,0 +1 ## +text/plain \ No newline at end of property Index: head/math/cvc4/files/patch-src_base_configuration.cpp =================================================================== --- head/math/cvc4/files/patch-src_base_configuration.cpp (revision 475114) +++ head/math/cvc4/files/patch-src_base_configuration.cpp (revision 475115) @@ -1,11 +1,11 @@ ---- 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() { - return __DATE__ " " __TIME__; + return "(timestamp removed for reproducible builds)"; } }/* CVC4 namespace */ Index: head/math/cvc4/pkg-plist =================================================================== --- head/math/cvc4/pkg-plist (revision 475114) +++ head/math/cvc4/pkg-plist (revision 475115) @@ -1,130 +1,130 @@ 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 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 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_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/predicate.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/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 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/theory/theory_test_utils.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/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 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 %%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%%share/java/CVC4.jar %%JAVA%%share/java/CVC4compat.jar