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