Attachment #206129 for bug #238376




# $FreeBSD$

PORTNAME=	cvc4
DISTVERSION=	1.7
PORTREVISION=	4
CATEGORIES=	math java
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)


LIB_DEPENDS=	libantlr3c.so:devel/libantlr3c \
		libboost_system.so:devel/boost-libs
BUILD_DEPENDS=	bash:shells/bash \
		antlr3:devel/antlr3

USES=		cmake ncurses compiler:c++17-lang \
		pkgconfig python:3.5+,build shebangfix

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

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 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_CMAKE_BOOL=	USE_CRYPTOMINISAT
CRYPTOMINISAT_LIB_DEPENDS=	libcryptominisat5.so:math/cryptominisat

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

PYTHON_CMAKE_BOOL=	BUILD_BINDINGS_PYTHON USE_PYTHON3
PYTHON_BUILD_DEPENDS=	swig3.0:devel/swig30

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_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
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

post-patch:
	@${REINPLACE_CMD} -e 's|^#!/bin/bash|#!/bin/sh|g' \
		${WRKSRC}/doc/*.sh ${WRKSRC}/src/base/mk* ${WRKSRC}/src/options/*.sh
	@${REINPLACE_CMD} -e "s|sed -i 's|sed -ibak 's|g" \
		${WRKSRC}/src/fix-install-headers.sh

.include <bsd.port.mk>

Lines 1-3 Link Here

(-)i/math/cvc4/distinfo (-3 / +7 lines)
1	TIMESTAMP = 1531429558	1	TIMESTAMP = 1559856275
2	SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7	2	SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7
3	SIZE (cvc4-1.6.tar.gz) = 7815893	3	SIZE (antlr-3.4-complete.jar) = 2388361
		4	SHA256 (CVC4-CVC4-1.7_GH0.tar.gz) = 9864a364a0076ef7ff63a46cdbc69cbe6568604149626338598d4df7788f8c2e
		5	SIZE (CVC4-CVC4-1.7_GH0.tar.gz) = 6969953
		6	SHA256 (fc8907afc08d.patch) = b14fe811a91152d9311a48e1c198c82fc55febf0c76c6c8fab6c9d6f0addeb3f
		7	SIZE (fc8907afc08d.patch) = 1154




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()




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)




--- 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(

Removed Link Here

(-)c/math/cvc4/files/patch-configure.ac (-11 lines)
1	--- configure.ac.orig 2018-07-12 21:33:27 UTC
2	+++ configure.ac
3	@@ -913,7 +913,7 @@ AC_ARG_WITH([cryptominisat],
4	CVC4_CHECK_FOR_CRYPTOMINISAT
5	if test $have_libcryptominisat -eq 1; then
6	CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-DCVC4_USE_CRYPTOMINISAT"
7	- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/install/include"
8	+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$CRYPTOMINISAT_HOME/include"
9	fi
10	AM_CONDITIONAL([CVC4_USE_CRYPTOMINISAT], [test $have_libcryptominisat -eq 1])
11	AC_SUBST([CRYPTOMINISAT_LDFLAGS])




--- 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)




--- 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 Link Here

(-)i/math/cvc4/files/patch-src_CMakeLists.txt (+11 lines)
1	--- src/CMakeLists.txt.orig 2019-07-28 18:28:58 UTC
2	+++ src/CMakeLists.txt
3	@@ -913,6 +913,6 @@ install(FILES
4
5	# Fix include paths for all public headers.
6	# Note: This is a temporary fix until the new C++ API is in place.
7	-install(CODE "execute_process(COMMAND
8	+install(CODE "execute_process(COMMAND sh
9	${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
10	- ${CMAKE_INSTALL_PREFIX})")
11	+ \"\$ENV{DESTDIR}\${CMAKE_INSTALL_PREFIX}\")")

Lines 1-6 Link Here

(-)i/math/cvc4/files/patch-src_base_configuration.cpp (-2 / +2 lines)
1	--- src/base/configuration.cpp.orig 2018-06-25 21:13:17 UTC	1	--- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC
2	+++ src/base/configuration.cpp	2	+++ src/base/configuration.cpp
3	@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() {	3	@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() {
4	}	4	}
5		5
6	std::string Configuration::getCompiledDateTime() {	6	std::string Configuration::getCompiledDateTime() {




--- 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




--- 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}




--- 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)
 




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

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

include/cvc4/options/printer_modes.h
include/cvc4/options/quantifiers_modes.h
include/cvc4/options/set_language.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

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/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.6
%%JAVA%%lib/libcvc4jni.so
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/libcvc4parser.so
lib/libcvc4parser.so.6
%%PYTHON%%%%PYTHON_SITELIBDIR%%/CVC4.py
%%PYTHON%%%%PYTHON_SITELIBDIR%%/_CVC4.so
%%DATADIR%%/drat.plf
%%DATADIR%%/er.plf
%%DATADIR%%/lrat.plf
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_bv_rewrites.plf
%%DATADIR%%/th_int.plf
%%DATADIR%%/th_real.plf
%%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

Return to bug 238376

Lines 1-10 Link Here

(-)i/math/cvc4/Makefile (-34 / +53 lines)
1	# $FreeBSD$	1	# $FreeBSD$
2		2
3	PORTNAME= cvc4	3	PORTNAME= cvc4
4	DISTVERSION= 1.6	4	DISTVERSION= 1.7
5	PORTREVISION= 4
6	CATEGORIES= math java	5	CATEGORIES= math java
7	MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/	6	MASTER_SITES+= http://www.antlr3.org/download/:antlr3
		7	DISTFILES+= antlr-3.4-complete.jar:antlr3
		8	EXTRACT_ONLY= ${DISTNAME}${EXTRACT_SUFX}
		9
		10	PATCH_SITES= https://github.com/${GH_ACCOUNT}/${GH_PROJECT}/commit/
		11	PATCHFILES+= fc8907afc08d.patch:-p1 # Install Java bindings
8		12
9	MAINTAINER= greg@unrelenting.technology	13	MAINTAINER= greg@unrelenting.technology
10	COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)	14	COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)
Lines 14-76 LICENSE_FILE= ${WRKSRC}/COPYING Link Here
14		18
15	LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \	19	LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \
16	libboost_system.so:devel/boost-libs	20	libboost_system.so:devel/boost-libs
17	BUILD_DEPENDS= bash:shells/bash \
18	antlr3:devel/antlr3
19		21
20	USES= autoreconf compiler:c++17-lang gmake libtool localbase \	22	USES= cmake ncurses compiler:c++17-lang \
21	pkgconfig python:3.5+,build shebangfix	23	pkgconfig python:3.5+,build shebangfix
		24
		25	USE_GITHUB= yes
		26	GH_ACCOUNT= CVC4
		27	GH_PROJECT= CVC4
		28
22	USE_JAVA= yes	29	USE_JAVA= yes
23	JAVA_BUILD= yes	30	JAVA_BUILD= yes
24		31
25	GNU_CONFIGURE= yes
26	CONFIGURE_ARGS+= --disable-dependency-tracking \
27	--with-swig=${LOCALBASE}/bin/swig3.0 \
28	ANTLR=${LOCALBASE}/bin/antlr3
29	CONFIGURE_SHELL= ${LOCALBASE}/bin/bash
30	USE_LDCONFIG= yes	32	USE_LDCONFIG= yes
31	SHEBANG_FILES= src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression.py
32		33
33	OPTIONS_DEFINE= CRYPTOMINISAT JAVA READLINE DEBUG	34	CMAKE_BUILD_TYPE= Production
		35	CMAKE_ARGS+= -DANTLR_BINARY=${WRKDIR}/antlr3
		36
		37	OPTIONS_DEFINE= CRYPTOMINISAT JAVA PYTHON READLINE
34	OPTIONS_RADIO= NUMLIB	38	OPTIONS_RADIO= NUMLIB
35	OPTIONS_RADIO_NUMLIB= GMP CLN	39	OPTIONS_RADIO_NUMLIB= GMP CLN
36	OPTIONS_DEFAULT= CRYPTOMINISAT READLINE GMP	40	OPTIONS_DEFAULT= CRYPTOMINISAT JAVA PYTHON READLINE GMP
37	OPTIONS_SUB= yes	41	OPTIONS_SUB= yes
38		42
39	CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver	43	CRYPTOMINISAT_DESC= Use CryptoMiniSat as the SAT solver
40	GMP_DESC= Use GMP numeric library	44	GMP_DESC= Use GMP numeric library
41	CLN_DESC= Use CLN numeric library (disables portfolio mode)	45	CLN_DESC= Use CLN numeric library (disables portfolio mode)
42		46
43	CRYPTOMINISAT_CONFIGURE_ON= --with-cryptominisat --with-cryptominisat-dir=${LOCALBASE}	47	CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT
44	CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat	48	CRYPTOMINISAT_LIB_DEPENDS= libcryptominisat5.so:math/cryptominisat
45		49
46	JAVA_CONFIGURE_ON= --enable-language-bindings=c,c++,java \	50	JAVA_CMAKE_BOOL= BUILD_BINDINGS_JAVA
47	JAVA_CPPFLAGS="-I${JAVA_HOME}/include -I${JAVA_HOME}/include/freebsd" \	51	JAVA_CMAKE_ON= -DJAVA_INCLUDE_PATH:PATH=${JAVA_HOME}/include \
48	JAVAC=${JAVAC} JAVAH=${JAVAH} JAR=${JAR}	52	-DJAVA_AWT_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ARCH}/libjawt.so \
49	JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++	53	-DJAVA_JVM_LIBRARY:PATH=${JAVA_HOME}/jre/lib/${ATCH}/libjava.so
50	JAVA_BUILD_DEPENDS= swig3.0:devel/swig30	54	JAVA_BUILD_DEPENDS= swig3.0:devel/swig30
51		55
52	READLINE_CONFIGURE_WITH= readline	56	PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3
53	READLINE_USES= readline	57	PYTHON_BUILD_DEPENDS= swig3.0:devel/swig30
54		58
55	GMP_CONFIGURE_WITH= gmp	59	READLINE_CMAKE_BOOL= USE_READLINE
56	GMP_CONFIGURE_ON= --with-portfolio	60	READLINE_USES= readline:port
57	GMP_LIB_DEPENDS= libgmp.so:math/gmp \	61
58	libboost_thread.so:devel/boost-libs	62	GMP_CMAKE_BOOL= ENABLE_PORTFOLIO
		63	GMP_CMAKE_ON= -DENABLE_DUMPING=OFF
		64	GMP_LIB_DEPENDS= libgmp.so:math/gmp \
		65	libboost_thread.so:devel/boost-libs
59	# note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies	66	# note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies
60		67
61	CLN_CONFIGURE_WITH= cln	68	CLN_CMAKE_BOOL= USE_CLN
62	CLN_LIB_DEPENDS= libcln.so:math/cln \	69	CLN_LIB_DEPENDS= libcln.so:math/cln \
63	libgmp.so:math/gmp	70	libgmp.so:math/gmp
64
65	DEBUG_CONFIGURE_ON= --with-build=debug
66	DEBUG_CONFIGURE_OFF= --with-build=production
67	DEBUG_INSTALL_TARGET_OFF= install-strip
68		71
69	.include <bsd.port.options.mk>	72	.include <bsd.port.options.mk>
70		73
71	.if ${PORT_OPTIONS:MREADLINE} \|\| ${PORT_OPTIONS:MCLN}	74	.if ${PORT_OPTIONS:MREADLINE} \|\| ${PORT_OPTIONS:MCLN}
72	LICENSE= GPLv3	75	LICENSE= GPLv3
73	CONFIGURE_ARGS+= --enable-gpl	76	CMAKE_ARGS+= -DENABLE_GPL:BOOL=ON
74	.endif	77	.endif
75		78
		79	post-extract:
		80	@${CP} ${DISTDIR}/antlr-3.4-complete.jar ${WRKDIR}/antlr3.jar
		81	@${ECHO_CMD} "#!/bin/sh" > ${WRKDIR}/antlr3
		82	@${ECHO_CMD} "JAVA_VERSION=1.7+ exec \"${LOCALBASE}/bin/java\" -classpath \"${WRKDIR}/antlr3.jar\" org.antlr.Tool \"\$$@\"" >> ${WRKDIR}/antlr3
		83	@${CHMOD} +x ${WRKDIR}/antlr3
		84
		85	# make a relative symlink instead of absolute to build dir
		86	post-install-JAVA-on:
		87	@${LN} -sf CVC4-1.7.0.jar ${STAGEDIR}${PREFIX}/share/java/cvc4/CVC4.jar
		88
		89	post-patch:
		90	@${REINPLACE_CMD} -e 's\|^#!/bin/bash\|#!/bin/sh\|g' \
		91	${WRKSRC}/doc/.sh ${WRKSRC}/src/base/mk ${WRKSRC}/src/options/*.sh
		92	@${REINPLACE_CMD} -e "s\|sed -i 's\|sed -ibak 's\|g" \
		93	${WRKSRC}/src/fix-install-headers.sh
		94
76	.include <bsd.port.mk>	95	.include <bsd.port.mk>

Added Link Here

(-)i/math/cvc4/files/patch-cmake_FindANTLR.cmake (+13 lines)
1	We fetch 3.4 (since 3.5 breaks it), we don't want it to find
2	system antlr3 (3.5) and overwrite our fetched one
3
4	--- cmake/FindANTLR.cmake.orig 2019-04-09 16:14:31 UTC
5	+++ cmake/FindANTLR.cmake
6	@@ -27,7 +27,6 @@ find_library(ANTLR_LIBRARIES
7	NO_DEFAULT_PATH)
8
9	if(CHECK_SYSTEM_VERSION)
10	- find_program(ANTLR_BINARY NAMES antlr3)
11	find_path(ANTLR_INCLUDE_DIR NAMES antlr3.h)
12	find_library(ANTLR_LIBRARIES NAMES antlr3c)
13	endif()

Added Link Here

(-)i/math/cvc4/files/patch-cmake_FindReadline.cmake (+42 lines)
1	CMAKE_REQUIRED_INCLUDES does not work for some reason,
2	the check is compiled without the include path
3
4	--- cmake/FindReadline.cmake.orig 2019-04-09 16:14:31 UTC
5	+++ cmake/FindReadline.cmake
6	@@ -13,15 +13,7 @@ find_library(Readline_LIBRARIES NAMES readline)
7	function(try_compile_readline libs _result)
8	set(CMAKE_REQUIRED_QUIET TRUE)
9	set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES} ${libs})
10	- check_cxx_source_compiles(
11	- "
12	- #include <stdio.h>
13	- #include <readline/readline.h>
14	- int main() { readline(\"\"); return 0; }
15	- "
16	- ${_result}
17	- )
18	- set(${_result} ${${_result}} PARENT_SCOPE)
19	+ set(${_result} OK PARENT_SCOPE)
20	endfunction()
21
22	if(Readline_INCLUDE_DIR)
23	@@ -42,18 +34,7 @@ if(Readline_INCLUDE_DIR)
24
25	# Check which standard of readline is installed on the system.
26	# https://github.com/CVC4/CVC4/issues/702
27	- include(CheckCXXSourceCompiles)
28	- set(CMAKE_REQUIRED_QUIET TRUE)
29	- set(CMAKE_REQUIRED_LIBRARIES ${Readline_LIBRARIES})
30	- check_cxx_source_compiles(
31	- "#include <stdio.h>
32	- #include <readline/readline.h>
33	- char* foo(const char, int) { return (char)0; }
34	- int main() { rl_completion_entry_function = foo; return 0; }"
35	- Readline_COMPENTRY_FUNC_RETURNS_CHARPTR
36	- )
37	- unset(CMAKE_REQUIRED_QUIET)
38	- unset(CMAKE_REQUIRED_LIBRARIES)
39	+ set(Readline_COMPENTRY_FUNC_RETURNS_CHARPTR TRUE)
40	endif()
41
42	include(FindPackageHandleStandardArgs)

Removed Link Here

(-)c/math/cvc4/files/patch-config_cryptominisat.m4 (-31 lines)
1	--- config/cryptominisat.m4.orig 2018-07-12 21:34:02 UTC
2	+++ config/cryptominisat.m4
3	@@ -36,7 +36,7 @@ elif test -n "$with_cryptominisat"; then
4	AC_MSG_RESULT([no])
5	fi
6
7	- if ! test -d "$CRYPTOMINISAT_HOME" \|\| ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat5_simple" ; then
8	+ if ! test -d "$CRYPTOMINISAT_HOME" \|\| ! test -x "$CRYPTOMINISAT_HOME/bin/cryptominisat5_simple" ; then
9	AC_MSG_FAILURE([either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built])
10	fi
11
12	@@ -54,7 +54,7 @@ elif test -n "$with_cryptominisat"; then
13	have_libcryptominisat=1
14	fi
15
16	- CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
17	+ CRYPTOMINISAT_LDFLAGS="-L$CRYPTOMINISAT_HOME/lib"
18
19	else
20	AC_MSG_RESULT([no, user didn't request cryptominisat])
21	@@ -74,8 +74,8 @@ if test -z "$CRYPTOMINISAT_LIBS"; then
22	cvc4_save_LDFLAGS="$LDFLAGS"
23	cvc4_save_CPPFLAGS="$CPPFLAGS"
24
25	- LDFLAGS="-L$CRYPTOMINISAT_HOME/install/lib"
26	- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include"
27	+ LDFLAGS="-L$CRYPTOMINISAT_HOME/lib"
28	+ CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/include"
29	LIBS="-lcryptominisat5 $1"
30
31	AC_LINK_IFELSE(

Added Link Here

(-)i/math/cvc4/files/patch-doc_CMakeLists.txt (+22 lines)
1	--- doc/CMakeLists.txt.orig 2019-06-06 21:29:05 UTC
2	+++ doc/CMakeLists.txt
3	@@ -34,10 +34,10 @@ configure_file(
4	#-----------------------------------------------------------------------------#
5	# Install man pages
6
7	-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1)
8	-install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5)
9	+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1)
10	+install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION man/man5)
11	if(ENABLE_PORTFOLIO)
12	- install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1
13	+ install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION man/man1
14	RENAME pcvc4.1)
15	endif()
16	install(FILES
17	@@ -45,4 +45,4 @@ install(FILES
18	${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3
19	${CMAKE_CURRENT_BINARY_DIR}/options.3cvc
20	${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc
21	- DESTINATION share/man/man3)
22	+ DESTINATION man/man3)

Added Link Here

(-)i/math/cvc4/files/patch-examples_CMakeLists.txt (+12 lines)
1	--- examples/CMakeLists.txt.orig 2019-06-06 19:10:39 UTC
2	+++ examples/CMakeLists.txt
3	@@ -17,9 +17,6 @@ add_custom_target(examples)
4
5	# Create target runexamples.
6	# Builds and runs all examples.
7	-add_custom_target(runexamples
8	- COMMAND ctest --output-on-failure -L "example" -j${NTHREADS} $(ARGS)
9	- DEPENDS examples)
10
11	# Add example target and create test to run example with ctest.
12	#

Added Link Here

(-)i/math/cvc4/files/patch-test_CMakeLists.txt (+14 lines)
1	--- test/CMakeLists.txt.orig 2019-06-06 19:12:46 UTC
2	+++ test/CMakeLists.txt
3	@@ -15,11 +15,6 @@ add_dependencies(build-tests examples)
4	# first run the command of the regress target (i.e., run all regression tests)
5	# and afterwards run the command specified for the check target.
6	# Dependencies of check are added in the corresponding subdirectories.
7	-add_custom_target(check
8	- COMMAND
9	- ctest --output-on-failure -LE "regress[3-4]" -j${CTEST_NTHREADS} $(ARGS)
10	- DEPENDS
11	- build-tests)
12
13	#-----------------------------------------------------------------------------#
14	# Add subdirectories

Added Link Here

(-)i/math/cvc4/files/patch-test_regress_CMakeLists.txt (+14 lines)
1	--- test/regress/CMakeLists.txt.orig 2019-06-06 19:13:41 UTC
2	+++ test/regress/CMakeLists.txt
3	@@ -2138,11 +2138,6 @@ set(run_regress_script ${CMAKE_CURRENT_LIST_DIR}/run_r
4	add_custom_target(build-regress DEPENDS cvc4-bin)
5	add_dependencies(build-tests build-regress)
6
7	-add_custom_target(regress
8	- COMMAND
9	- ctest --output-on-failure -L "regress[0-2]" -j${CTEST_NTHREADS} $(ARGS)
10	- DEPENDS build-regress)
11	-
12	macro(cvc4_add_regression_test level file)
13	add_test(${file}
14	${run_regress_script}

Added Link Here

(-)i/math/cvc4/files/patch-test_system_CMakeLists.txt (+13 lines)
1	--- test/system/CMakeLists.txt.orig 2019-06-06 19:13:50 UTC
2	+++ test/system/CMakeLists.txt
3	@@ -10,10 +10,6 @@ include_directories(${CMAKE_BINARY_DIR}/src)
4	add_custom_target(build-systemtests)
5	add_dependencies(build-tests build-systemtests)
6
7	-add_custom_target(systemtests
8	- COMMAND ctest --output-on-failure -L "system" -j${CTEST_NTHREADS} $(ARGS)
9	- DEPENDS build-systemtests)
10	-
11	set(CVC4_SYSTEM_TEST_FLAGS
12	-D__BUILDING_CVC4_SYSTEM_TEST -D__STDC_LIMIT_MACROS -D__STDC_FORMAT_MACROS)
13

Lines 1-23 Link Here

(-)i/math/cvc4/pkg-plist (-39 / +20 lines)
1	bin/cvc4	1	bin/cvc4
2	%%GMP%%bin/pcvc4	2	%%GMP%%bin/pcvc4
		3	include/cvc4/api/cvc4cpp.h
		4	include/cvc4/api/cvc4cppkind.h
3	include/cvc4/base/configuration.h	5	include/cvc4/base/configuration.h
4	include/cvc4/base/exception.h	6	include/cvc4/base/exception.h
5	include/cvc4/base/listener.h	7	include/cvc4/base/listener.h
6	include/cvc4/base/modal_exception.h	8	include/cvc4/base/modal_exception.h
7	include/cvc4/base/tls.h
8	include/cvc4/bindings/compat/c/c_interface.h
9	include/cvc4/bindings/compat/c/c_interface_defs.h
10	include/cvc4/compat/cvc3_compat.h
11	include/cvc4/context/cdhashmap_forward.h	9	include/cvc4/context/cdhashmap_forward.h
12	include/cvc4/context/cdhashset_forward.h	10	include/cvc4/context/cdhashset_forward.h
13	include/cvc4/context/cdinsert_hashmap_forward.h	11	include/cvc4/context/cdinsert_hashmap_forward.h
14	include/cvc4/context/cdlist_forward.h	12	include/cvc4/context/cdlist_forward.h
15	include/cvc4/context/cdtrail_hashmap_forward.h
16	include/cvc4/cvc4.h	13	include/cvc4/cvc4.h
17	include/cvc4/cvc4_private.h
18	include/cvc4/cvc4_private_library.h
19	include/cvc4/cvc4_public.h	14	include/cvc4/cvc4_public.h
20	include/cvc4/cvc4parser_private.h
21	include/cvc4/cvc4parser_public.h	15	include/cvc4/cvc4parser_public.h
22	include/cvc4/expr/array.h	16	include/cvc4/expr/array.h
23	include/cvc4/expr/array_store_all.h	17	include/cvc4/expr/array_store_all.h
Lines 28-38 include/cvc4/expr/emptyset.h Link Here
28	include/cvc4/expr/expr.h	22	include/cvc4/expr/expr.h
29	include/cvc4/expr/expr_iomanip.h	23	include/cvc4/expr/expr_iomanip.h
30	include/cvc4/expr/expr_manager.h	24	include/cvc4/expr/expr_manager.h
31	include/cvc4/expr/expr_manager_template.h
32	include/cvc4/expr/expr_stream.h	25	include/cvc4/expr/expr_stream.h
33	include/cvc4/expr/expr_template.h
34	include/cvc4/expr/kind.h	26	include/cvc4/expr/kind.h
35	include/cvc4/expr/kind_template.h
36	include/cvc4/expr/pickler.h	27	include/cvc4/expr/pickler.h
37	include/cvc4/expr/record.h	28	include/cvc4/expr/record.h
38	include/cvc4/expr/symbol_table.h	29	include/cvc4/expr/symbol_table.h
Lines 50-56 include/cvc4/options/options.h Link Here
50	include/cvc4/options/printer_modes.h	41	include/cvc4/options/printer_modes.h
51	include/cvc4/options/quantifiers_modes.h	42	include/cvc4/options/quantifiers_modes.h
52	include/cvc4/options/set_language.h	43	include/cvc4/options/set_language.h
53	include/cvc4/options/simplification_mode.h	44	include/cvc4/options/smt_modes.h
54	include/cvc4/options/sygus_out_mode.h	45	include/cvc4/options/sygus_out_mode.h
55	include/cvc4/options/theoryof_mode.h	46	include/cvc4/options/theoryof_mode.h
56	include/cvc4/parser/input.h	47	include/cvc4/parser/input.h
Lines 66-72 include/cvc4/smt_util/lemma_channels.h Link Here
66	include/cvc4/smt_util/lemma_input_channel.h	57	include/cvc4/smt_util/lemma_input_channel.h
67	include/cvc4/smt_util/lemma_output_channel.h	58	include/cvc4/smt_util/lemma_output_channel.h
68	include/cvc4/theory/logic_info.h	59	include/cvc4/theory/logic_info.h
69	include/cvc4/theory/theory_test_utils.h
70	include/cvc4/util/abstract_value.h	60	include/cvc4/util/abstract_value.h
71	include/cvc4/util/bitvector.h	61	include/cvc4/util/bitvector.h
72	include/cvc4/util/bool.h	62	include/cvc4/util/bool.h
Lines 91-122 include/cvc4/util/sexpr.h Link Here
91	include/cvc4/util/statistics.h	81	include/cvc4/util/statistics.h
92	include/cvc4/util/tuple.h	82	include/cvc4/util/tuple.h
93	include/cvc4/util/unsafe_interrupt_exception.h	83	include/cvc4/util/unsafe_interrupt_exception.h
94	%%JAVA%%lib/jni/libcvc4compatjni.so
95	%%JAVA%%lib/jni/libcvc4compatjni.so.5
96	%%JAVA%%lib/jni/libcvc4compatjni.so.5.0.0
97	%%JAVA%%lib/jni/libcvc4jni.so
98	%%JAVA%%lib/jni/libcvc4jni.so.5
99	%%JAVA%%lib/jni/libcvc4jni.so.5.0.0
100	lib/libcvc4.so	84	lib/libcvc4.so
101	lib/libcvc4.so.5	85	lib/libcvc4.so.6
102	lib/libcvc4.so.5.0.0	86	%%JAVA%%lib/libcvc4jni.so
103	lib/libcvc4bindings_c_compat.so
104	lib/libcvc4bindings_c_compat.so.5
105	lib/libcvc4bindings_c_compat.so.5.0.0
106	lib/libcvc4compat.so
107	lib/libcvc4compat.so.5
108	lib/libcvc4compat.so.5.0.0
109	lib/libcvc4parser.so	87	lib/libcvc4parser.so
110	lib/libcvc4parser.so.5	88	lib/libcvc4parser.so.6
111	lib/libcvc4parser.so.5.0.0	89	%%PYTHON%%%%PYTHON_SITELIBDIR%%/CVC4.py
112	man/man1/cvc4.1.gz	90	%%PYTHON%%%%PYTHON_SITELIBDIR%%/_CVC4.so
113	%%GMP%%man/man1/pcvc4.1.gz	91	%%DATADIR%%/drat.plf
114	man/man3/SmtEngine.3cvc.gz	92	%%DATADIR%%/er.plf
115	man/man3/libcvc4.3.gz	93	%%DATADIR%%/lrat.plf
116	man/man3/libcvc4compat.3.gz
117	man/man3/libcvc4parser.3.gz
118	man/man3/options.3cvc.gz
119	man/man5/cvc4.5.gz
120	%%DATADIR%%/sat.plf	94	%%DATADIR%%/sat.plf
121	%%DATADIR%%/smt.plf	95	%%DATADIR%%/smt.plf
122	%%DATADIR%%/th_arrays.plf	96	%%DATADIR%%/th_arrays.plf
Lines 126-130 man/man5/cvc4.5.gz Link Here
126	%%DATADIR%%/th_bv_rewrites.plf	100	%%DATADIR%%/th_bv_rewrites.plf
127	%%DATADIR%%/th_int.plf	101	%%DATADIR%%/th_int.plf
128	%%DATADIR%%/th_real.plf	102	%%DATADIR%%/th_real.plf
129	%%JAVA%%share/java/CVC4.jar	103	%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4-1.7.0.jar
130	%%JAVA%%share/java/CVC4compat.jar	104	%%JAVA%%%%JAVASHAREDIR%%/cvc4/CVC4.jar
		105	man/man1/cvc4.1.gz
		106	%%GMP%%man/man1/pcvc4.1.gz
		107	man/man3/SmtEngine.3cvc.gz
		108	man/man3/libcvc4.3.gz
		109	man/man3/libcvc4parser.3.gz
		110	man/man3/options.3cvc.gz
		111	man/man5/cvc4.5.gz