aboutsummaryrefslogtreecommitdiffstats
path: root/math
diff options
context:
space:
mode:
Diffstat (limited to 'math')
-rw-r--r--math/cvc4/Makefile26
-rw-r--r--math/cvc4/distinfo6
-rw-r--r--math/cvc4/files/patch-config_cryptominisat.m431
-rw-r--r--math/cvc4/files/patch-configure.ac11
-rw-r--r--math/cvc4/files/patch-src_base_configuration.cpp4
-rw-r--r--math/cvc4/pkg-plist32
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