mirror/freebsd-ports
1
0
Fork 0
mirror of https://git.FreeBSD.org/ports.git synced 2024-12-22 04:17:44 +00:00
Code Issues Releases Activity

math/cvc4: update to 1.7

Browse Source 
ChangeLog:

https://github.com/CVC4/CVC4/releases/tag/1.7

* New Features:
    Proofs:
        Support for bit-vector proofs with eager bitblasting
    Strings:
        Support for str.replaceall operator.
        New option --re-elim
    SyGuS:
        Support for abduction (--sygus-abduct)

* Improvements:
    Strings:
        Significantly better performance

* Changes:
    API change: Expr::iffExpr() is renamed to Expr::eqExpr()
    Compiling the language bindings now requires SWIG 3 instead of SWIG 2.
    The CVC3 compatibility layer has been removed.
    The build system now uses CMake instead of Autotools
This commit is contained in:
Fernando Apesteguía 2019-08-01 15:20:28 +00:00
parent ce401dadce
commit 549b27dafd
Notes: svn2git 2021-03-31 03:12:20 +00:00 
svn path=/head/; revision=507774
14 changed files with 221 additions and 120 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

85
math/cvc4/Makefile
View File

@ -1,10 +1,14 @@
# $FreeBSD$
PORTNAME= cvc4
DISTVERSION= 1.6
PORTREVISION= 5
DISTVERSION= 1.7
CATEGORIES= math java
MASTER_SITES= https://cvc4.cs.stanford.edu/downloads/builds/src/
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)
@ -12,65 +16,78 @@ COMMENT= Automatic theorem prover for SMT (Satisfiability Modulo Theories)
LICENSE= BSD3CLAUSE
LICENSE_FILE= ${WRKSRC}/COPYING
BUILD_DEPENDS= bash:shells/bash
LIB_DEPENDS= libantlr3c.so:devel/libantlr3c \
libboost_system.so:devel/boost-libs
BUILD_DEPENDS= bash:shells/bash \
antlr3:devel/antlr3
USES= autoreconf compiler:c++17-lang gmake libtool localbase \
USES= cmake ncurses compiler:c++17-lang \
pkgconfig python:3.5+,build shebangfix
SHEBANG_FILES= src/base/mktagheaders \
src/base/mktags
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
OPTIONS_DEFINE= CRYPTOMINISAT JAVA READLINE DEBUG
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 READLINE GMP
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_CONFIGURE_ON= --with-cryptominisat --with-cryptominisat-dir=${LOCALBASE}
CRYPTOMINISAT_CMAKE_BOOL= USE_CRYPTOMINISAT
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}
JAVA_CONFIGURE_OFF= --enable-language-bindings=c,c++
JAVA_BUILD_DEPENDS= swig3.0:devel/swig30
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
READLINE_CONFIGURE_WITH= readline
READLINE_USES= readline
PYTHON_CMAKE_BOOL= BUILD_BINDINGS_PYTHON USE_PYTHON3
PYTHON_BUILD_DEPENDS= swig3.0:devel/swig30
GMP_CONFIGURE_WITH= gmp
GMP_CONFIGURE_ON= --with-portfolio
GMP_LIB_DEPENDS= libgmp.so:math/gmp \
libboost_thread.so:devel/boost-libs
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_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
CLN_CMAKE_BOOL= USE_CLN
CLN_LIB_DEPENDS= libcln.so:math/cln \
libgmp.so:math/gmp
.include <bsd.port.options.mk>
.if ${PORT_OPTIONS:MREADLINE} || ${PORT_OPTIONS:MCLN}
LICENSE= GPLv3
CONFIGURE_ARGS+= --enable-gpl
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>

10
math/cvc4/distinfo
View File

@ -1,3 +1,7 @@
TIMESTAMP = 1531429558
SHA256 (cvc4-1.6.tar.gz) = 5c18bd5ea893fba9723a4d35c889d412ec6d29a21db9db69481891a8ff4887c7
SIZE (cvc4-1.6.tar.gz) = 7815893
TIMESTAMP = 1559856275
SHA256 (antlr-3.4-complete.jar) = 9d3e866b610460664522520f73b81777b5626fb0a282a5952b9800b751550bf7
SIZE (antlr-3.4-complete.jar) = 2388361
SHA256 (CVC4-CVC4-1.7_GH0.tar.gz) = 9864a364a0076ef7ff63a46cdbc69cbe6568604149626338598d4df7788f8c2e
SIZE (CVC4-CVC4-1.7_GH0.tar.gz) = 6969953
SHA256 (fc8907afc08d.patch) = b14fe811a91152d9311a48e1c198c82fc55febf0c76c6c8fab6c9d6f0addeb3f
SIZE (fc8907afc08d.patch) = 1154

13
math/cvc4/files/patch-cmake_FindANTLR.cmake Normal file
View File

@ -0,0 +1,13 @@
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()

42
math/cvc4/files/patch-cmake_FindReadline.cmake Normal file
View File

@ -0,0 +1,42 @@
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)

31
math/cvc4/files/patch-config_cryptominisat.m4
View File

@ -1,31 +0,0 @@
--- 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(

11
math/cvc4/files/patch-configure.ac
View File

@ -1,11 +0,0 @@
--- 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])

22
math/cvc4/files/patch-doc_CMakeLists.txt Normal file
View File

@ -0,0 +1,22 @@
--- 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)

12
math/cvc4/files/patch-examples_CMakeLists.txt Normal file
View File

@ -0,0 +1,12 @@
--- 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.
#

11
math/cvc4/files/patch-src_CMakeLists.txt Normal file
View File

@ -0,0 +1,11 @@
--- src/CMakeLists.txt.orig 2019-07-28 18:28:58 UTC
+++ src/CMakeLists.txt
@@ -913,6 +913,6 @@ install(FILES
# Fix include paths for all public headers.
# Note: This is a temporary fix until the new C++ API is in place.
-install(CODE "execute_process(COMMAND
+install(CODE "execute_process(COMMAND sh
${CMAKE_CURRENT_LIST_DIR}/fix-install-headers.sh
- ${CMAKE_INSTALL_PREFIX})")
+ \"\$ENV{DESTDIR}\${CMAKE_INSTALL_PREFIX}\")")

4
math/cvc4/files/patch-src_base_configuration.cpp
View File

@ -1,6 +1,6 @@
--- src/base/configuration.cpp.orig 2018-06-25 21:13:17 UTC
--- src/base/configuration.cpp.orig 2019-04-09 16:14:31 UTC
+++ src/base/configuration.cpp
@@ -405,7 +405,7 @@ std::string Configuration::getCompiler() {
@@ -376,7 +376,7 @@ std::string Configuration::getCompiler() {
}
std::string Configuration::getCompiledDateTime() {

14
math/cvc4/files/patch-test_CMakeLists.txt Normal file
View File

@ -0,0 +1,14 @@
--- 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

14
math/cvc4/files/patch-test_regress_CMakeLists.txt Normal file
View File

@ -0,0 +1,14 @@
--- 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}

13
math/cvc4/files/patch-test_system_CMakeLists.txt Normal file
View File

@ -0,0 +1,13 @@
--- 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)

59
math/cvc4/pkg-plist
View File

@ -1,23 +1,17 @@
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
@ -28,11 +22,8 @@ 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/record.h
include/cvc4/expr/symbol_table.h
@ -50,7 +41,7 @@ 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/smt_modes.h
include/cvc4/options/sygus_out_mode.h
include/cvc4/options/theoryof_mode.h
include/cvc4/parser/input.h
@ -66,7 +57,6 @@ 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
@ -91,32 +81,16 @@ include/cvc4/util/sexpr.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.5
lib/libcvc4.so.5.0.0
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/libcvc4.so.6
%%JAVA%%lib/libcvc4jni.so
lib/libcvc4parser.so
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
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
lib/libcvc4parser.so.6
%%PYTHON%%%%PYTHON_SITELIBDIR%%/CVC4.py
%%PYTHON%%%%PYTHON_SITELIBDIR%%/_CVC4.so
%%DATADIR%%/drat.plf
%%DATADIR%%/er.plf
%%DATADIR%%/lrat.plf
%%DATADIR%%/sat.plf
%%DATADIR%%/smt.plf
%%DATADIR%%/th_arrays.plf
@ -126,5 +100,12 @@ man/man5/cvc4.5.gz
%%DATADIR%%/th_bv_rewrites.plf
%%DATADIR%%/th_int.plf
%%DATADIR%%/th_real.plf
%%JAVA%%share/java/CVC4.jar
%%JAVA%%share/java/CVC4compat.jar
%%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