Attachment #192897 for bug #227702




# $FreeBSD$

PORTNAME=	cvc4
PORTVERSION=	1.5
CATEGORIES=	math
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 \
		antlr3:devel/antlr3

USES=		compiler:c++11-lang pkgconfig gmake libtool shebangfix localbase
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

OPTIONS_DEFINE=		JAVA READLINE DEBUG
OPTIONS_RADIO=		NUMLIB
OPTIONS_RADIO_NUMLIB=	GMP CLN
OPTIONS_DEFAULT=	READLINE CLN
OPTIONS_SUB=		yes

GMP_DESC=		Use GMP numeric library
CLN_DESC=		Use CLN numeric library (disables portfolio mode)

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 <bsd.port.options.mk>

.if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN}
LICENSE=		GPLv3
CONFIGURE_ARGS+=	--enable-gpl
.endif

.include <bsd.port.mk>

Added Link Here

(-)w/math/cvc4/distinfo (+3 lines)
1	TIMESTAMP = 1524235369
2	SHA256 (cvc4-1.5.tar.gz) = 5d6b4f8ee8420f85e3f804181341cedf6ea32342c48f355a5be87754152b14e9
3	SIZE (cvc4-1.5.tar.gz) = 8059968

Added Link Here

(-)w/math/cvc4/files/patch-src_base_configuration.cpp (+11 lines)
1	--- src/base/configuration.cpp.orig 2018-04-22 17:53:43 UTC
2	+++ src/base/configuration.cpp
3	@@ -291,7 +291,7 @@ std::string Configuration::getCompiler() {
4	}
5
6	std::string Configuration::getCompiledDateTime() {
7	- return __DATE__ " " __TIME__;
8	+ return "(timestamp removed for reproducible builds)";
9	}
10
11	}/* CVC4 namespace */




--- src/main/portfolio.cpp.orig	2018-04-22 17:42:48 UTC
+++ src/main/portfolio.cpp
@@ -18,6 +18,9 @@
 #include <boost/bind.hpp>
 #include <boost/thread/condition.hpp>
 #include <boost/exception_ptr.hpp>
+#ifdef __FreeBSD__
+#include <pthread_np.h>
+#endif
 
 #include "base/output.h"
 #include "options/options.h"
@@ -100,7 +103,11 @@ std::pair<int, S> runPortfolio(int numThreads,
       void *stackaddr;
       size_t stacksize;
       pthread_attr_t attr;
+#ifdef __linux__
       pthread_getattr_np(threads[t].native_handle(), &attr);
+#elif __FreeBSD__
+      pthread_attr_get_np(threads[t].native_handle(), &attr);
+#endif
       pthread_attr_getstack(&attr, &stackaddr, &stacksize);
       Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl;
     }

Added Link Here

(-)w/math/cvc4/pkg-descr (+6 lines)
1	An efficient open-source automatic theorem prover for satisfiability modulo
2	theories (SMT) problems. It can be used to prove the validity (or, dually, the
3	satisfiability) of first-order formulas in a large number of built-in logical
4	theories and their combination.
5
6	WWW: https://cvc4.cs.stanford.edu/web/




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/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/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/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/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/libcvc4jni.so
%%JAVA%%lib/jni/libcvc4jni.so.4
%%JAVA%%lib/jni/libcvc4jni.so.4.0.0
lib/libcvc4.so
lib/libcvc4.so.4
lib/libcvc4.so.4.0.0
lib/libcvc4bindings_c_compat.so
lib/libcvc4bindings_c_compat.so.4
lib/libcvc4bindings_c_compat.so.4.0.0
lib/libcvc4compat.so
lib/libcvc4compat.so.4
lib/libcvc4compat.so.4.0.0
lib/libcvc4parser.so
lib/libcvc4parser.so.4
lib/libcvc4parser.so.4.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

Return to bug 227702

Added Link Here

(-)w/math/cvc4/Makefile (+74 lines)
1	# $FreeBSD$
2
3	PORTNAME= cvc4
4	PORTVERSION= 1.5
5	CATEGORIES= math
6	MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/
7
8	MAINTAINER= greg@unrelenting.technology
9	COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)
10
11	LICENSE= BSD3CLAUSE
12	LICENSE_FILE= ${WRKSRC}/COPYING
13
14	LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \
15	libboost_system.so:devel/boost-libs
16	BUILD_DEPENDS= gexpr:sysutils/coreutils \
17	bash:shells/bash \
18	antlr3:devel/antlr3
19
20	USES= compiler:c++11-lang pkgconfig gmake libtool shebangfix localbase
21	USE_JAVA= yes
22	JAVA_BUILD= yes
23
24	GNU_CONFIGURE= yes
25	CONFIGURE_ARGS+= --disable-dependency-tracking \
26	--with-swig=${LOCALBASE}/bin/swig3.0 \
27	ANTLR=${LOCALBASE}/bin/antlr3
28	CONFIGURE_SHELL= ${LOCALBASE}/bin/bash
29	USE_LDCONFIG= yes
30	SHEBANG_FILES= src/mk* src/theory/mk* src/base/mk* src/expr/mk* src/options/mk* test/regress/run_regression
31
32	OPTIONS_DEFINE= JAVA READLINE DEBUG
33	OPTIONS_RADIO= NUMLIB
34	OPTIONS_RADIO_NUMLIB= GMP CLN
35	OPTIONS_DEFAULT= READLINE CLN
36	OPTIONS_SUB= yes
37
38	GMP_DESC= Use GMP numeric library
39	CLN_DESC= Use CLN numeric library (disables portfolio mode)
40
41	JAVA_CONFIGURE_ON= --enable-language-bindings=c,c++,java \
42	JAVA_CPPFLAGS="-I${JAVA_HOME}/include -I${JAVA_HOME}/include/freebsd" \
43	JAVAC=${JAVAC} JAVAH=${JAVAH} JAR=${JAR}
44	JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++
45	JAVA_BUILD_DEPENDS= swig3.0:devel/swig30
46
47	READLINE_CONFIGURE_WITH= readline
48	READLINE_USES= readline
49
50	GMP_CONFIGURE_WITH= gmp
51	GMP_CONFIGURE_ON= --with-portfolio
52	GMP_LIB_DEPENDS= libgmp.so:math/gmp \
53	libboost_thread.so:devel/boost-libs
54	# note: CVC4 already depends on boost-libs, so portfolio mode is "free" in terms of pkg dependencies
55
56	CLN_CONFIGURE_WITH= cln
57	CLN_LIB_DEPENDS= libcln.so:math/cln \
58	libgmp.so:math/gmp
59
60	DEBUG_CONFIGURE_ON= --with-build=debug
61	DEBUG_CONFIGURE_OFF= --with-build=production
62	DEBUG_INSTALL_TARGET_OFF= install-strip
63
64	post-patch:
65	${REINPLACE_CMD} -e 's\|expr \|gexpr \|g' ${WRKSRC}/src/options/mkoptions
66
67	.include <bsd.port.options.mk>
68
69	.if ${PORT_OPTIONS:MREADLINE} \|\| ${PORT_OPTIONS:MCLN}
70	LICENSE= GPLv3
71	CONFIGURE_ARGS+= --enable-gpl
72	.endif
73
74	.include <bsd.port.mk>

Added Link Here

(-)w/math/cvc4/files/patch-src_main_portfolio.cpp (+24 lines)
1	--- src/main/portfolio.cpp.orig 2018-04-22 17:42:48 UTC
2	+++ src/main/portfolio.cpp
3	@@ -18,6 +18,9 @@
4	#include <boost/bind.hpp>
5	#include <boost/thread/condition.hpp>
6	#include <boost/exception_ptr.hpp>
7	+#ifdef __FreeBSD__
8	+#include <pthread_np.h>
9	+#endif
10
11	#include "base/output.h"
12	#include "options/options.h"
13	@@ -100,7 +103,11 @@ std::pair<int, S> runPortfolio(int numThreads,
14	void *stackaddr;
15	size_t stacksize;
16	pthread_attr_t attr;
17	+#ifdef __linux__
18	pthread_getattr_np(threads[t].native_handle(), &attr);
19	+#elif __FreeBSD__
20	+ pthread_attr_get_np(threads[t].native_handle(), &attr);
21	+#endif
22	pthread_attr_getstack(&attr, &stackaddr, &stacksize);
23	Chat() << "Created worker thread " << t << " with stack size " << stacksize << std::endl;
24	}

Added Link Here

(-)w/math/cvc4/pkg-plist (+130 lines)
1	bin/cvc4
2	bin/lfsc-checker
3	%%GMP%%bin/pcvc4
4	include/cvc4/base/configuration.h
5	include/cvc4/base/exception.h
6	include/cvc4/base/listener.h
7	include/cvc4/base/modal_exception.h
8	include/cvc4/base/ptr_closer.h
9	include/cvc4/base/tls.h
10	include/cvc4/bindings/compat/c/c_interface.h
11	include/cvc4/bindings/compat/c/c_interface_defs.h
12	include/cvc4/compat/cvc3_compat.h
13	include/cvc4/context/cdhashmap_forward.h
14	include/cvc4/context/cdhashset_forward.h
15	include/cvc4/context/cdinsert_hashmap_forward.h
16	include/cvc4/context/cdlist_forward.h
17	include/cvc4/context/cdtrail_hashmap_forward.h
18	include/cvc4/cvc4.h
19	include/cvc4/cvc4_private.h
20	include/cvc4/cvc4_private_library.h
21	include/cvc4/cvc4_public.h
22	include/cvc4/cvc4parser_private.h
23	include/cvc4/cvc4parser_public.h
24	include/cvc4/expr/array.h
25	include/cvc4/expr/array_store_all.h
26	include/cvc4/expr/ascription_type.h
27	include/cvc4/expr/chain.h
28	include/cvc4/expr/datatype.h
29	include/cvc4/expr/emptyset.h
30	include/cvc4/expr/expr.h
31	include/cvc4/expr/expr_iomanip.h
32	include/cvc4/expr/expr_manager.h
33	include/cvc4/expr/expr_manager_template.h
34	include/cvc4/expr/expr_stream.h
35	include/cvc4/expr/expr_template.h
36	include/cvc4/expr/kind.h
37	include/cvc4/expr/kind_template.h
38	include/cvc4/expr/pickler.h
39	include/cvc4/expr/predicate.h
40	include/cvc4/expr/record.h
41	include/cvc4/expr/symbol_table.h
42	include/cvc4/expr/type.h
43	include/cvc4/expr/uninterpreted_constant.h
44	include/cvc4/expr/variable_type_map.h
45	include/cvc4/options/argument_extender.h
46	include/cvc4/options/arith_heuristic_pivot_rule.h
47	include/cvc4/options/arith_propagation_mode.h
48	include/cvc4/options/arith_unate_lemma_mode.h
49	include/cvc4/options/language.h
50	include/cvc4/options/option_exception.h
51	include/cvc4/options/options.h
52	include/cvc4/options/printer_modes.h
53	include/cvc4/options/quantifiers_modes.h
54	include/cvc4/options/set_language.h
55	include/cvc4/options/simplification_mode.h
56	include/cvc4/options/theoryof_mode.h
57	include/cvc4/parser/input.h
58	include/cvc4/parser/parser.h
59	include/cvc4/parser/parser_builder.h
60	include/cvc4/parser/parser_exception.h
61	include/cvc4/proof/unsat_core.h
62	include/cvc4/smt/command.h
63	include/cvc4/smt/logic_exception.h
64	include/cvc4/smt/smt_engine.h
65	include/cvc4/smt_util/lemma_channels.h
66	include/cvc4/smt_util/lemma_input_channel.h
67	include/cvc4/smt_util/lemma_output_channel.h
68	include/cvc4/theory/logic_info.h
69	include/cvc4/theory/theory_test_utils.h
70	include/cvc4/util/abstract_value.h
71	include/cvc4/util/bitvector.h
72	include/cvc4/util/bool.h
73	include/cvc4/util/cardinality.h
74	include/cvc4/util/channel.h
75	include/cvc4/util/divisible.h
76	include/cvc4/util/floatingpoint.h
77	include/cvc4/util/gmp_util.h
78	include/cvc4/util/hash.h
79	include/cvc4/util/integer.h
80	include/cvc4/util/integer_cln_imp.h
81	include/cvc4/util/integer_gmp_imp.h
82	include/cvc4/util/proof.h
83	include/cvc4/util/rational.h
84	include/cvc4/util/rational_cln_imp.h
85	include/cvc4/util/rational_gmp_imp.h
86	include/cvc4/util/regexp.h
87	include/cvc4/util/resource_manager.h
88	include/cvc4/util/result.h
89	include/cvc4/util/sexpr.h
90	include/cvc4/util/statistics.h
91	include/cvc4/util/subrange_bound.h
92	include/cvc4/util/tuple.h
93	include/cvc4/util/unsafe_interrupt_exception.h
94	%%JAVA%%lib/jni/libcvc4compatjni.so
95	%%JAVA%%lib/jni/libcvc4compatjni.so.4
96	%%JAVA%%lib/jni/libcvc4compatjni.so.4.0.0
97	%%JAVA%%lib/jni/libcvc4jni.so
98	%%JAVA%%lib/jni/libcvc4jni.so.4
99	%%JAVA%%lib/jni/libcvc4jni.so.4.0.0
100	lib/libcvc4.so
101	lib/libcvc4.so.4
102	lib/libcvc4.so.4.0.0
103	lib/libcvc4bindings_c_compat.so
104	lib/libcvc4bindings_c_compat.so.4
105	lib/libcvc4bindings_c_compat.so.4.0.0
106	lib/libcvc4compat.so
107	lib/libcvc4compat.so.4
108	lib/libcvc4compat.so.4.0.0
109	lib/libcvc4parser.so
110	lib/libcvc4parser.so.4
111	lib/libcvc4parser.so.4.0.0
112	man/man1/cvc4.1.gz
113	%%GMP%%man/man1/pcvc4.1.gz
114	man/man3/SmtEngine.3cvc.gz
115	man/man3/libcvc4.3.gz
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
121	%%DATADIR%%/smt.plf
122	%%DATADIR%%/th_arrays.plf
123	%%DATADIR%%/th_base.plf
124	%%DATADIR%%/th_bv.plf
125	%%DATADIR%%/th_bv_bitblast.plf
126	%%DATADIR%%/th_bv_rewrites.plf
127	%%DATADIR%%/th_int.plf
128	%%DATADIR%%/th_real.plf
129	%%JAVA%%share/java/CVC4.jar
130	%%JAVA%%share/java/CVC4compat.jar