View | Details | Raw Unified | Return to bug 238376 | Differences between
and this patch

Collapse All | Expand All

(-)w/math/cvc4/Makefile (-34 / +51 lines)
Lines 1-10 Link Here
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
76
.include <bsd.port.mk>
93
.include <bsd.port.mk>
(-)w/math/cvc4/distinfo (-3 / +7 lines)
Lines 1-3 Link Here
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
(-)w/math/cvc4/files/patch-cmake_FindANTLR.cmake (+13 lines)
Added Link Here
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()
(-)w/math/cvc4/files/patch-cmake_FindReadline.cmake (+42 lines)
Added Link Here
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)
(-)c/math/cvc4/files/patch-config_cryptominisat.m4 (-31 lines)
Removed Link Here
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(
(-)c/math/cvc4/files/patch-configure.ac (-11 lines)
Removed Link Here
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])
(-)w/math/cvc4/files/patch-doc_CMakeLists.txt (+22 lines)
Added Link Here
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)
(-)w/math/cvc4/files/patch-examples_CMakeLists.txt (+12 lines)
Added Link Here
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
 #
(-)w/math/cvc4/files/patch-src_base_configuration.cpp (-2 / +2 lines)
Lines 1-6 Link Here
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() {
(-)w/math/cvc4/files/patch-test_CMakeLists.txt (+14 lines)
Added Link Here
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
(-)w/math/cvc4/files/patch-test_regress_CMakeLists.txt (+14 lines)
Added Link Here
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}
(-)w/math/cvc4/files/patch-test_system_CMakeLists.txt (+13 lines)
Added Link Here
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
 
(-)w/math/cvc4/pkg-plist (-39 / +20 lines)
Lines 1-23 Link Here
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

Return to bug 238376