Attachment #204867 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
PYTHON_BUILD_DEPENDS=	swig3.0:devel/swig30

READLINE_CMAKE_BOOL=	USE_READLINE
READLINE_USES=		readline

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

.include <bsd.port.mk>

Lines 1-3 Link Here

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




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

Lines 1-6 Link Here

(-)w/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() {




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

(-)w/math/cvc4/Makefile (-34 / +47 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
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
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
76	.include <bsd.port.mk>	89	.include <bsd.port.mk>

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(

Lines 1-23 Link Here

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