From ded5ca8205cec6e326542c50c6b1f4417a5d113f Mon Sep 17 00:00:00 2001 From: Jerry James Date: Thu, 13 Jun 2019 06:32:44 -0600 Subject: [PATCH] New upstream release. Also: - Drop -autoconf, -cadical, -doxygen, -symfpu, and -vec patches. - Drop -doc subpackage; upstream no longer supports doxygen. - Build with python 3 instead of python 2. - Build with drat2er support. - Add -abc and -flags patches. - Add -swig4 patch (bz 1707353). --- cvc4-abc.patch | 54 ++++++++++ cvc4-autoconf.patch | 123 ----------------------- cvc4-cadical.patch | 50 ---------- cvc4-doxygen.patch | 72 -------------- cvc4-flags.patch | 46 +++++++++ cvc4-swig4.patch | 44 ++++++++ cvc4-symfpu.patch | 14 --- cvc4-vec.patch | 24 ----- cvc4.spec | 237 +++++++++++++++++++------------------------- sources | 2 +- 10 files changed, 246 insertions(+), 420 deletions(-) create mode 100644 cvc4-abc.patch delete mode 100644 cvc4-autoconf.patch delete mode 100644 cvc4-cadical.patch delete mode 100644 cvc4-doxygen.patch create mode 100644 cvc4-flags.patch create mode 100644 cvc4-swig4.patch delete mode 100644 cvc4-symfpu.patch delete mode 100644 cvc4-vec.patch diff --git a/cvc4-abc.patch b/cvc4-abc.patch new file mode 100644 index 0000000..f80c5f8 --- /dev/null +++ b/cvc4-abc.patch @@ -0,0 +1,54 @@ +--- cmake/FindABC.cmake.orig 2019-04-09 10:14:31.000000000 -0600 ++++ cmake/FindABC.cmake 2019-04-16 16:01:44.519958231 -0600 +@@ -2,7 +2,6 @@ + # ABC_FOUND - system has ABC lib + # ABC_INCLUDE_DIR - the ABC include directory + # ABC_LIBRARIES - Libraries needed to use ABC +-# ABC_ARCH_FLAGS - Platform specific compile flags + + + # Check default location of ABC built with contrib/get-abc. +@@ -14,28 +13,19 @@ endif() + # install rule. + find_path(ABC_INCLUDE_DIR + NAMES base/abc/abc.h +- PATHS ${ABC_HOME}/src ++ PATHS /usr/include/abc + NO_DEFAULT_PATH) + find_library(ABC_LIBRARIES + NAMES abc +- PATHS ${ABC_HOME} +- NO_DEFAULT_PATH) +-find_program(ABC_ARCH_FLAGS_PROG +- NAMES arch_flags +- PATHS ${ABC_HOME} ++ PATHS /usr/lib64 + NO_DEFAULT_PATH) + +-if(ABC_ARCH_FLAGS_PROG) +- execute_process(COMMAND ${ABC_ARCH_FLAGS_PROG} +- OUTPUT_VARIABLE ABC_ARCH_FLAGS) +-endif() +- + include(FindPackageHandleStandardArgs) + find_package_handle_standard_args(ABC + DEFAULT_MSG +- ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) ++ ABC_INCLUDE_DIR ABC_LIBRARIES) + +-mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES ABC_ARCH_FLAGS) ++mark_as_advanced(ABC_INCLUDE_DIR ABC_LIBRARIES) + if(ABC_LIBRARIES) + message(STATUS "Found ABC libs: ${ABC_LIBRARIES}") + endif() +--- CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 ++++ CMakeLists.txt 2019-04-16 15:54:30.334111544 -0600 +@@ -379,7 +379,7 @@ endif() + if(USE_ABC) + set(ABC_HOME "${ABC_DIR}") + find_package(ABC REQUIRED) +- add_definitions(-DCVC4_USE_ABC ${ABC_ARCH_FLAGS}) ++ add_definitions(-DCVC4_USE_ABC) + endif() + + if(USE_CADICAL) diff --git a/cvc4-autoconf.patch b/cvc4-autoconf.patch deleted file mode 100644 index 373b81a..0000000 --- a/cvc4-autoconf.patch +++ /dev/null @@ -1,123 +0,0 @@ ---- config/abc.m4.orig 2018-06-25 15:13:17.531906649 -0600 -+++ config/abc.m4 2018-07-05 14:55:03.244625126 -0600 -@@ -35,21 +35,17 @@ elif test -n "$with_abc"; then - AC_MSG_RESULT([no]) - fi - -- if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then -+ if ! test -d "$ABC_HOME"; then - AC_MSG_FAILURE([either $ABC_HOME is not an abc source tree or it's not yet built]) - fi - -- AC_MSG_CHECKING([for arch_flags to use with libabc]) -- libabc_arch_flags="$("$ABC_HOME/arch_flags")" -- AC_MSG_RESULT([$libabc_arch_flags]) -- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags" -- ABC_LDFLAGS="-L$ABC_HOME" -+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I/usr/include/abc" -+ ABC_LDFLAGS="" - - dnl Try a bunch of combinations until something works :-/ - cvc4_save_LDFLAGS="$LDFLAGS" - ABC_LIBS= -- CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags" -- LDFLAGS="$LDFLAGS $ABC_LDFLAGS" -+ CPPFLAGS="$CPPFLAGS -I/usr/include/abc" - AC_CHECK_HEADER([base/abc/abc.h], [], [AC_MSG_FAILURE([cannot find abc.h, the ABC header!])]) - AC_MSG_CHECKING([how to link abc]) - CVC4_TRY_ABC_WITH([]) ---- config/antlr.m4.orig 2018-06-25 15:13:17.532906666 -0600 -+++ config/antlr.m4 2018-07-05 14:56:06.052723809 -0600 -@@ -35,6 +35,7 @@ been generated already. To obtain ANTLR - case "$ANTLR_VERSION" in - 3.2|3.2.*) ANTLR_VERSION=3.2 ;; - 3.4|3.4.*) ANTLR_VERSION=3.4 ;; -+ 3.5|3.5.*) ANTLR_VERSION=3.5 ;; - *) AC_MSG_WARN([unknown version of antlr: $ANTLR_VERSION]);; - esac - fi -@@ -130,8 +131,8 @@ AC_DEFUN([AC_LIB_ANTLR],[ - } - ])], - [ -- AC_MSG_RESULT([found it (must be antlr3 3.4 or similar)]) -- if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.4; then -+ AC_MSG_RESULT([found it (must be antlr3 3.5 or similar)]) -+ if test -n "$ANTLR_VERSION" -a "$ANTLR_VERSION" != 3.5; then - AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!]) - fi - ], ---- config/boost.m4.orig 2018-06-25 15:13:17.539906789 -0600 -+++ config/boost.m4 2018-07-05 14:56:32.388765183 -0600 -@@ -71,7 +71,7 @@ dnl strip `\n' with backquotes, not the - dnl boost_cv_lib_version='1_37\r' for instance, which breaks - dnl everything else. - dnl Cannot use 'dnl' after [$4] because a trailing dnl may break AC_CACHE_CHECK --(eval "$ac_cpp conftest.$ac_ext") 2>&AS_MESSAGE_LOG_FD | -+(eval "$ac_cpp -P conftest.$ac_ext") 2>&AS_MESSAGE_LOG_FD | - grep -v "^#" | - tr -d '\r\n ' | - $SED -n -e "$1" >conftest.i 2>&1], ---- config/cryptominisat.m4.orig 2018-06-25 15:13:17.542906841 -0600 -+++ config/cryptominisat.m4 2018-07-05 14:57:42.402740101 -0600 -@@ -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" ; 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="" - - 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="" -+ CPPFLAGS="$CPPFLAGS -I/usr/include/cryptominisat5" - LIBS="-lcryptominisat5 $1" - - AC_LINK_IFELSE( ---- configure.ac.orig 2018-06-25 15:33:12.372543152 -0600 -+++ configure.ac 2018-07-05 14:58:49.284601972 -0600 -@@ -294,7 +294,7 @@ if test $cross_compiling = "no"; then - AC_MSG_CHECKING([whether C++ exceptions work]) - AC_LANG_PUSH([C++]) - AC_RUN_IFELSE( -- AC_LANG_PROGRAM([#include ], [[ -+ [AC_LANG_PROGRAM([#include ], [[ - int result = 1; - try { - throw std::exception(); -@@ -302,7 +302,7 @@ if test $cross_compiling = "no"; then - result = 0; - } - return result; -- ]]), -+ ]])], - [AC_MSG_RESULT([yes])], - [AC_MSG_ERROR([C++ exceptions do not work.])] - ) -@@ -657,11 +657,6 @@ fi - - AC_MSG_RESULT([$enable_debug_symbols]) - --if test "$enable_debug_symbols" = yes; then -- CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3" -- CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" --fi -- - AC_MSG_CHECKING([whether to enable Valgrind instrumentation]) - - AC_ARG_ENABLE([valgrind], diff --git a/cvc4-cadical.patch b/cvc4-cadical.patch deleted file mode 100644 index bdd21b5..0000000 --- a/cvc4-cadical.patch +++ /dev/null @@ -1,50 +0,0 @@ ---- config/cadical.m4.orig 2018-06-25 15:13:17.541906824 -0600 -+++ config/cadical.m4 2018-07-06 16:08:10.850078221 -0600 -@@ -21,7 +21,7 @@ elif test -n "$with_cadical"; then - [path to top level of CaDiCaL source tree] - ), - CADICAL_HOME="$withval", -- [ if test -z "$CADICAL_HOME" && ! test -e "$ac_abs_confdir/cadical/build/libcadical.a"; then -+ [ if test -z "$CADICAL_HOME"; then - AC_MSG_FAILURE([must give --with-cadical-dir=PATH, define environment variable CADICAL_HOME, or use contrib/get-cadical to setup CaDiCaL for CVC4!]) - fi - ] -@@ -36,7 +36,7 @@ elif test -n "$with_cadical"; then - AC_MSG_RESULT([no]) - fi - -- if ! test -d "$CADICAL_HOME" || ! test -e "$CADICAL_HOME/build/libcadical.a" ; then -+ if ! test -d "$CADICAL_HOME" ; then - AC_MSG_FAILURE([either $CADICAL_HOME is not a CaDiCaL source tree or it's not yet built $CADICAL_HOME/build/libcadical.a]) - fi - -@@ -51,7 +51,7 @@ elif test -n "$with_cadical"; then - have_libcadical=1 - fi - -- CADICAL_LDFLAGS="-L$CADICAL_HOME/build" -+ CADICAL_LDFLAGS="" - - else - AC_MSG_RESULT([no, user didn't request CaDiCaL]) -@@ -68,11 +68,7 @@ if test -z "$CADICAL_LIBS"; then - AC_LANG_PUSH([C++]) - - cvc4_save_LIBS="$LIBS" -- cvc4_save_LDFLAGS="$LDFLAGS" -- cvc4_save_CPPFLAGS="$CPPFLAGS" - -- LDFLAGS="-L$CADICAL_HOME/build" -- CPPFLAGS="$CPPFLAGS -I$CADICAL_HOME/src" - LIBS="-lcadical" - - AC_LINK_IFELSE( -@@ -80,8 +76,6 @@ if test -z "$CADICAL_LIBS"; then - [[CaDiCaL::Solver test();]])], [CADICAL_LIBS="-lcadical"], - [CADICAL_LIBS=]) - -- LDFLAGS="$cvc4_save_LDFLAGS" -- CPPFLAGS="$cvc4_save_CPPFLAGS" - LIBS="$cvc4_save_LIBS" - - AC_LANG_POP([C++]) diff --git a/cvc4-doxygen.patch b/cvc4-doxygen.patch deleted file mode 100644 index 1b83f24..0000000 --- a/cvc4-doxygen.patch +++ /dev/null @@ -1,72 +0,0 @@ ---- src/expr/expr_manager_template.cpp.orig 2018-06-25 15:13:17.952914014 -0600 -+++ src/expr/expr_manager_template.cpp 2018-07-05 14:39:39.136284939 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file expr_manager_template.cpp -+/*! \file expr_manager.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Christopher L. Conway, Dejan Jovanovic ---- src/expr/expr_manager_template.h.orig 2018-06-25 15:13:17.953914032 -0600 -+++ src/expr/expr_manager_template.h 2018-07-05 14:39:39.137284937 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file expr_manager_template.h -+/*! \file expr_manager.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ---- src/expr/expr_template.h.orig 2018-06-25 15:13:17.958914119 -0600 -+++ src/expr/expr_template.h 2018-07-05 14:39:39.138284935 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file expr_template.h -+/*! \file expr.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Aina Niemetz ---- src/expr/kind_template.h.orig 2018-06-25 15:13:17.962914189 -0600 -+++ src/expr/kind_template.h 2018-07-05 14:39:39.138284935 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file kind_template.h -+/*! \file kind.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Dejan Jovanovic, Andres Noetzli ---- src/expr/metakind_template.h.orig 2018-06-25 15:13:17.966914259 -0600 -+++ src/expr/metakind_template.h 2018-07-05 14:39:39.139284933 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file metakind_template.h -+/*! \file metakind.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Andres Noetzli, Tim King ---- src/expr/type_checker_template.cpp.orig 2018-06-25 15:13:18.004914924 -0600 -+++ src/expr/type_checker_template.cpp 2018-07-05 14:39:39.139284933 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file type_checker_template.cpp -+/*! \file type_checker.cpp - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King, Andrew Reynolds ---- src/expr/type_properties_template.h.orig 2018-06-25 15:13:18.007914976 -0600 -+++ src/expr/type_properties_template.h 2018-07-05 14:39:39.139284933 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file type_properties_template.h -+/*! \file type_properties.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King ---- src/util/rational.h.in.orig 2018-06-25 15:13:19.197935796 -0600 -+++ src/util/rational.h.in 2018-07-05 14:39:39.139284933 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file rational.h.in -+/*! \file rational.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, Tim King diff --git a/cvc4-flags.patch b/cvc4-flags.patch new file mode 100644 index 0000000..5a8e62d --- /dev/null +++ b/cvc4-flags.patch @@ -0,0 +1,46 @@ +--- CMakeLists.txt.orig 2019-04-16 15:54:30.334111544 -0600 ++++ CMakeLists.txt 2019-04-17 11:23:52.404867885 -0600 +@@ -125,7 +125,7 @@ option(BUILD_BINDINGS_PYTHON "Build Pyth + #-----------------------------------------------------------------------------# + # Internal cmake variables + +-set(OPTIMIZATION_LEVEL 3) ++set(OPTIMIZATION_LEVEL 2) + set(GPL_LIBS "") + + #-----------------------------------------------------------------------------# +--- src/parser/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/parser/CMakeLists.txt 2019-04-17 11:21:41.680050119 -0600 +@@ -81,10 +81,6 @@ foreach(lang Cvc Smt1 Smt2 Tptp) + set_source_files_properties(${gen_src_files} PROPERTIES LANGUAGE CXX) + set_source_files_properties(${gen_src_files} PROPERTIES GENERATED TRUE) + +- # We don't want to enable -Wall for code generated by ANTLR. +- set_source_files_properties( +- ${gen_src_files} PROPERTIES COMPILE_FLAGS -Wno-all) +- + # Add generated source files to the parser source files + list(APPEND libcvc4parser_src_files ${gen_src_files}) + endforeach() +--- src/prop/bvminisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/prop/bvminisat/mtl/template.mk 2019-04-17 11:22:27.662986017 -0600 +@@ -22,7 +22,7 @@ CXX ?= g++ + CFLAGS ?= -Wall -Wno-parentheses + LFLAGS ?= -Wall + +-COPTIMIZE ?= -O3 ++COPTIMIZE ?= -O2 + + CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS + LFLAGS += -lz +--- src/prop/minisat/mtl/template.mk.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/prop/minisat/mtl/template.mk 2019-04-17 11:22:15.879002442 -0600 +@@ -22,7 +22,7 @@ CXX ?= g++ + CFLAGS ?= -Wall -Wno-parentheses + LFLAGS ?= -Wall + +-COPTIMIZE ?= -O3 ++COPTIMIZE ?= -O2 + + CFLAGS += -I$(MROOT) -D __STDC_LIMIT_MACROS -D __STDC_FORMAT_MACROS + LFLAGS += -lz diff --git a/cvc4-swig4.patch b/cvc4-swig4.patch new file mode 100644 index 0000000..710e744 --- /dev/null +++ b/cvc4-swig4.patch @@ -0,0 +1,44 @@ +--- src/bindings/java/CMakeLists.txt.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/bindings/java/CMakeLists.txt 2019-06-06 11:58:39.836849929 -0600 +@@ -131,6 +131,7 @@ set(gen_java_files + ${CMAKE_CURRENT_BINARY_DIR}/LastExceptionBuffer.java + ${CMAKE_CURRENT_BINARY_DIR}/LogicException.java + ${CMAKE_CURRENT_BINARY_DIR}/LogicInfo.java ++ ${CMAKE_CURRENT_BINARY_DIR}/Map_ExprExpr.java + ${CMAKE_CURRENT_BINARY_DIR}/ModalException.java + ${CMAKE_CURRENT_BINARY_DIR}/OptionException.java + ${CMAKE_CURRENT_BINARY_DIR}/Options.java +@@ -177,7 +178,6 @@ set(gen_java_files + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpq_class.java + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_mpz_class.java + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__istream.java +- ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__mapT_CVC4__Expr_CVC4__Expr_t.java + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__ostream.java + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__shared_ptrT_CVC4__SygusPrintCallback_t.java + ${CMAKE_CURRENT_BINARY_DIR}/SWIGTYPE_p_std__string.java +@@ -204,12 +204,12 @@ set(gen_java_files + ${CMAKE_CURRENT_BINARY_DIR}/StatisticsBase.java + ${CMAKE_CURRENT_BINARY_DIR}/StringType.java + ${CMAKE_CURRENT_BINARY_DIR}/SygusConstraintCommand.java +- ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java + ${CMAKE_CURRENT_BINARY_DIR}/SygusGTerm.java + ${CMAKE_CURRENT_BINARY_DIR}/SygusInvConstraintCommand.java + ${CMAKE_CURRENT_BINARY_DIR}/SygusPrintCallback.java + ${CMAKE_CURRENT_BINARY_DIR}/SymbolTable.java + ${CMAKE_CURRENT_BINARY_DIR}/SymbolType.java ++ ${CMAKE_CURRENT_BINARY_DIR}/SynthFunCommand.java + ${CMAKE_CURRENT_BINARY_DIR}/TesterType.java + ${CMAKE_CURRENT_BINARY_DIR}/TheoryId.java + ${CMAKE_CURRENT_BINARY_DIR}/Timer.java +--- src/smt/smt_engine.i.orig 2019-04-09 10:14:31.000000000 -0600 ++++ src/smt/smt_engine.i 2019-06-06 11:24:53.214450924 -0600 +@@ -42,6 +42,9 @@ SWIGEXPORT void JNICALL Java_edu_nyu_acs + swigCPtr = 0; + } + } ++ ++%template(Map_ExprExpr) std::map; ++ + #endif // SWIGJAVA + + %ignore CVC4::SmtEngine::setLogic(const char*); diff --git a/cvc4-symfpu.patch b/cvc4-symfpu.patch deleted file mode 100644 index 727f167..0000000 --- a/cvc4-symfpu.patch +++ /dev/null @@ -1,14 +0,0 @@ ---- config/symfpu.m4.orig 2018-06-25 15:13:17.555907069 -0600 -+++ config/symfpu.m4 2018-07-07 10:34:08.415291211 -0600 -@@ -28,10 +28,10 @@ elif test -n "$with_symfpu"; then - if test -z "$SYMFPU_HOME" && test -e "$ac_abs_confdir/symfpu-CVC4/symfpu/core"; then - SYMFPU_HOME="$ac_abs_confdir/symfpu-CVC4" - AC_MSG_RESULT([yes, $SYMFPU_HOME]) -- have_symfpu_headers=1 - else - AC_MSG_RESULT([no]) - fi -+ have_symfpu_headers=1 - else - AC_MSG_RESULT([no, user didn't request symfpu]) - with_symfpu=no diff --git a/cvc4-vec.patch b/cvc4-vec.patch deleted file mode 100644 index d145d1e..0000000 --- a/cvc4-vec.patch +++ /dev/null @@ -1,24 +0,0 @@ ---- src/theory/quantifiers/conjecture_generator.cpp.orig 2018-06-25 15:13:18.823929253 -0600 -+++ src/theory/quantifiers/conjecture_generator.cpp 2018-07-07 14:37:50.162382038 -0600 -@@ -1089,16 +1089,17 @@ void ConjectureGenerator::getEnumerateUf - vec_sum = 0; - vec.push_back( size_limit ); - }else{ -+ int vecindex = (index < vec.size()) ? vec[index] : 0; - //see if we can iterate current - if (vec_sum < size_limit -- && !te->getEnumerateTerm(types[index], vec[index] + 1).isNull()) -+ && !te->getEnumerateTerm(types[index], vecindex + 1).isNull()) - { -- vec[index]++; -+ vec.assign(index, vecindex + 1); - vec_sum++; - vec.push_back( size_limit - vec_sum ); - }else{ -- vec_sum -= vec[index]; -- vec[index] = 0; -+ vec_sum -= vecindex; -+ vec.assign(index, 0); - index++; - if( index==n.getNumChildren() ){ - success = false; diff --git a/cvc4.spec b/cvc4.spec index 271465b..a6c312f 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -2,8 +2,8 @@ # we currently build without glpk support. Name: cvc4 -Version: 1.6 -Release: 6%{?dist} +Version: 1.7 +Release: 1%{?dist} Summary: Automatic theorem prover for SMT problems # License breakdown: @@ -16,27 +16,23 @@ Summary: Automatic theorem prover for SMT problems # - All other files are distributed under the MIT license License: Boost and BSD and MIT URL: http://cvc4.cs.stanford.edu/ -Source0: http://cvc4.cs.stanford.edu/downloads/builds/src/%{name}-%{version}.tar.gz -# Fix some doxygen problems. Upstream plans to fix this differently. -Patch0: %{name}-doxygen.patch -# Fix various autoconf problems -Patch1: %{name}-autoconf.patch -# Fix detection of cadical -Patch2: %{name}-cadical.patch -# Fix detection of symfpu -Patch3: %{name}-symfpu.patch -# Fix out-of-bounds vector accesses -Patch4: %{name}-vec.patch +Source0: https://github.com/CVC4/CVC4/archive/%{version}/%{name}-%{version}.tar.gz +# Fix detection of ABC +Patch0: %{name}-abc.patch +# Do not override Fedora flags +Patch1: %{name}-flags.patch +# Adapt to swig 4 +Patch2: %{name}-swig4.patch BuildRequires: abc-devel BuildRequires: antlr3-C-devel BuildRequires: antlr3-tool BuildRequires: boost-devel BuildRequires: cadical-devel -BuildRequires: chrpath +BuildRequires: cmake BuildRequires: cryptominisat-devel BuildRequires: cxxtest -BuildRequires: doxygen-latex +BuildRequires: drat2er-devel BuildRequires: gcc-c++ BuildRequires: ghostscript BuildRequires: gmp-devel @@ -45,13 +41,17 @@ BuildRequires: jpackage-utils BuildRequires: lfsc-devel BuildRequires: libtool BuildRequires: perl-interpreter -BuildRequires: python2 +BuildRequires: python3-devel BuildRequires: readline-devel BuildRequires: swig BuildRequires: symfpu-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} +# This can be removed when Fedora 30 reaches EOL +Obsoletes: %{name}-doc < 1.7 +Provides: %{name}-doc = %{version}-%{release} + %description CVC4 is an efficient open-source automatic theorem prover for satisfiability modulo theories (SMT) problems. It can be used to prove @@ -76,13 +76,6 @@ Requires: %{name}-libs%{?_isa} = %{version}-%{release} %description devel Header files and library links for developing applications that use %{name}. -%package doc -Summary: Interface documentation for %{name} -Provides: bundled(jquery) - -%description doc -Interface documentation for %{name}. - %package libs Summary: Library containing an automatic theorem prover for SMT problems @@ -99,68 +92,66 @@ Requires: jpackage-utils %description java Java interface to %{name}. +%package python3 +Summary: Python 3 interface to %{name} +Requires: %{name}-libs%{?_isa} = %{version}-%{release} + +%description python3 +Python 3 interface to %{name}. + %prep -%autosetup -p0 +%autosetup -p0 -n CVC4-%{version} -# Regenerate configure due to patch 1 -autoreconf -fi +# The Java interface uses type punning +sed -i '/include_directories/aadd_compile_options("-fno-strict-aliasing")' \ + src/bindings/java/CMakeLists.txt -# Do not override Fedora's optimization settings -sed -i 's/-O3/-O2/' \ - src/prop/minisat/mtl/template.mk src/prop/minisat/Makefile \ - src/prop/bvminisat/mtl/template.mk src/prop/bvminisat/Makefile +# The header file installation script does not know about DESTDIR +sed -i 's/\${CMAKE_INSTALL_PREFIX}/\\$ENV{DESTDIR}&/' src/CMakeLists.txt -# Avoid hardcoded rpaths and allow boost to use g++ 5.0 and higher. -sed -e 's,^hardcode_libdir_flag_spec=.*,hardcode_libdir_flag_spec="",g' \ - -e 's,runpath_var=LD_RUN_PATH,runpath_var=DIE_RPATH_DIE,g' \ - -e 's,OPTLEVEL=3,OPTLEVEL=2,g' \ - -e '/gcc48/i\ "defined __GNUC__ && __GNUC__ == 8 && !defined __ICC @ gcc80" \\\n "defined __GNUC__ && __GNUC__ == 7 && !defined __ICC @ gcc70" \\\n "defined __GNUC__ && __GNUC__ == 6 && !defined __ICC @ gcc60" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 3 && !defined __ICC @ gcc53" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 2 && !defined __ICC @ gcc52" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 1 && !defined __ICC @ gcc51" \\\n "defined __GNUC__ && __GNUC__ == 5 && __GNUC_MINOR__ == 0 && !defined __ICC @ gcc50" \\' \ - -i configure - -# Change the Java installation paths for Fedora and fix FTBFS -sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \ - -e 's/ -Wno-all//' \ - -i src/bindings/Makefile.am -sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \ - -e 's/ -Wno-all//' \ - -i src/bindings/Makefile.in - -# Fix access to an uninitialized variable -sed -e 's/Kind k;/Kind k = kind::UNDEFINED_KIND;/' \ - -i src/parser/cvc/CvcParser.c - -# Help the documentation generator -cp -p COPYING src/bindings/compat/c - -# Preserve timestamps when installing -for fil in $(find . -name Makefile\*); do - sed -i 's/$(install_sh) -c/$(install_sh) -p/' $fil -done - -# Fix an include path in the tests -sed -i 's,@CXXTEST@,%{_includedir}/cxxtest,' test/unit/Makefile.am +# Fix installation directory on 64-bit arches +if [ "%{_lib}" = "lib64" ]; then + sed -i 's/DESTINATION lib/&64/' src/CMakeLists.txt src/parser/CMakeLists.txt +fi %build -export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc" -if [ "%{__isa_bits}" = "64" ]; then -CPPFLAGS+=" -DLIN64" -else -CPPFLAGS+=" -DLIN" -fi -export CFLAGS="%{optflags} -fsigned-char" -export CXXFLAGS="%{optflags} -fsigned-char" -%configure --enable-gpl --enable-proof --enable-language-bindings=all \ - --disable-silent-rules --with-portfolio --without-compat \ - --with-abc --with-abc-dir=%{_prefix} \ - --with-cadical --with-cadical-dir=%{_prefix} \ - --with-cryptominisat --with-cryptominisat-dir=%{_prefix} \ - --with-lfsc --with-lfsc-dir=%{_prefix} \ - --with-symfpu --with-symfpu-dir=%{_prefix} \ - --with-readline +export CFLAGS="%{optflags} -fsigned-char -DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc" +export CXXFLAGS="$CFLAGS" +%cmake \ + -DCMAKE_SKIP_RPATH:BOOL=YES \ + -DCMAKE_SKIP_INSTALL_RPATH:BOOL=YES \ + -DBUILD_BINDINGS_JAVA:BOOL=ON \ + -DBUILD_BINDINGS_PYTHON:BOOL=ON \ + -DENABLE_GPL:BOOL=ON \ + -DENABLE_OPTIMIZED:STRING=ON \ + -DENABLE_PORTFOLIO:STRING=ON \ + -DENABLE_PROOFS:STRING=ON \ + -DENABLE_SHARED:STRING=ON \ + -DUSE_ABC:STRING=ON \ + -DABC_DIR:STRING=%{_prefix} \ + -DUSE_CADICAL:BOOL=ON \ + -DCADICAL_DIR:STRING=%{_prefix} \ + -DUSE_CRYPTOMINISAT:BOOL=ON \ + -DCRYPTOMINISAT_DIR:STRING=%{_prefix} \ + -DUSE_DRAT2ER:BOOL=ON \ + -DDRAT2ER_DIR:STRING=%{_prefix} \ + -DDrat2Er_INCLUDE_DIR:STRING=%{_includedir}/drat2er \ + -DDrat2Er_LIBRARIES:STRING=-ldrat2er \ + -DDratTrim_LIBRARIES:STRING=-ldrat2er \ + -DUSE_LFSC:BOOL=ON \ + -DLFSC_DIR:STRING=%{_prefix} \ + -DUSE_PYTHON3:BOOL=ON \ + -DUSE_READLINE:STRING=ON \ + -DUSE_SYMFPU:BOOL=ON \ + -DSYMFPU_DIR:STRING=%{_prefix} \ + -DPYTHON_EXECUTABLE:FILEPATH=%{_bindir}/python%{python3_version} \ + -DPYTHON_LIBRARY:FILEPATH=%{_libdir}/libpython%{python3_version}m.so \ + -DPYTHON_INCLUDE_DIR:FILEPATH=%{_includedir}/python%{python3_version}m \ + . -# Workaround libtool reordering -Wl,--as-needed after all the libraries -BUILDS=$(echo $PWD/builds/*linux*/*abc*) -sed -i 's/CC=.g../& -Wl,--as-needed/' $BUILDS/libtool +# Tell swig to build for python 3 +sed -i 's/swig -python/& -py3/' \ + src/bindings/python/CMakeFiles/CVC4_swig_compilation.dir/build.make make %{?_smp_mflags} make doc @@ -168,89 +159,63 @@ make doc %install %make_install -# Remove unwanted libtool files -find %{buildroot}%{_libdir} -name \*.la | xargs rm -f - -# Remove empty directories for language bindings that do not yet exist -rm -fr %{buildroot}%{_libdir}/{csharp,ocaml,perl5,php,pyshared,ruby,tcltk} -rm -fr %{buildroot}%{_datadir}/{csharp,perl5,php,pyshared} - -# Make the Java installation match Fedora requirements -if [ "%{_libdir}/java" != "%{_jnidir}" ]; then - mkdir -p %{buildroot}%{_jnidir} - mv %{buildroot}%{_libdir}/java/cvc4 %{buildroot}%{_jnidir} - rmdir %{buildroot}%{_libdir}/java -fi - -# Remove still more hardcoded rpaths -chrpath -d %{buildroot}%{_bindir}/* \ - %{buildroot}%{_libdir}/lib%{name}*.so.*.*.* \ - %{buildroot}%{_jnidir}/%{name}/lib%{name}*.so.*.*.* - -# Help the debuginfo generator -BUILDS=$(echo $PWD/builds/*linux*/*abc*) -for dir in decision expr main parser printer prop smt theory theory/arith \ - theory/arrays theory/booleans theory/bv theory/datatypes theory/idl \ - theory/quantifiers theory/rewriterules theory/strings theory/uf; do - ln -s $PWD/src/$dir/options $BUILDS/src/$dir -done -ln -s production-abc-proof/src $BUILDS/../src -ln -s $PWD/src/options/base_options $BUILDS/src/options -ln -s $PWD/src/options/base_options_template.cpp $BUILDS/src/options -ln -s $PWD/src/options/options_holder_template.h $BUILDS/src/options -ln -s $PWD/src/options/options_template.cpp $BUILDS/src/options -ln -s $PWD/src/smt/smt_options_template.cpp $BUILDS/src/smt - -%ldconfig_scriptlets libs +# BUG: CVC4 1.7 does not install the Java interface +mkdir -p %{buildroot}%{_javadir} +cp -p src/bindings/java/CVC4.jar %{buildroot}%{_javadir} +mkdir -p %{buildroot}%{_jnidir}/%{name} +cp -p src/bindings/java/libcvc4jni.so %{buildroot}%{_jnidir}/%{name} %check # The tests use a large amount of stack space ulimit -s unlimited -# Do not rebuild when checking -BUILDS=$(echo $PWD/builds/*linux*/*abc*) -sed -e 's/\(units.*:\) all/\1/' \ - -e 's/\(regress.*:\) all/\1/' \ - -i $BUILDS/Makefile $BUILDS/Makefile.builds - -# Fix bad include paths in the test code -sed 's,/barrett/scratch.*/expr/,./,' \ - test/unit/expr/expr_manager_public.cpp \ - test/unit/expr/expr_public.cpp \ - test/unit/expr/type_cardinality_public.cpp - # Fix the Java test's access to the JNI object it needs sed 's,loadLibrary("cvc4jni"),load("%{buildroot}%{_jnidir}/%{name}/libcvc4jni.so"),' \ -i test/system/CVC4JavaTest.java +export LC_ALL=C.UTF-8 export LD_LIBRARY_PATH=%{buildroot}%{_libdir} make check %files -%doc AUTHORS NEWS README RELEASE-NOTES THANKS -%{_bindir}/* +%doc AUTHORS NEWS README.md THANKS +%{_bindir}/%{name} +%{_bindir}/p%{name} %{_datadir}/%{name}/ -%{_mandir}/man1/* -%{_mandir}/man5/* - -%files doc -%license COPYING -%doc doc/doxygen/* +%{_mandir}/man1/%{name}.1* +%{_mandir}/man1/p%{name}.1* +%{_mandir}/man5/%{name}.5* %files libs -%license COPYING -%{_libdir}/lib%{name}*.so.* +%license COPYING licenses/channel.h-LICENSE +%{_libdir}/lib%{name}.so.6 +%{_libdir}/lib%{name}parser.so.6 %files devel %{_includedir}/%{name}/ -%{_libdir}/lib%{name}*.so +%{_libdir}/lib%{name}.so +%{_libdir}/lib%{name}parser.so %{_mandir}/man3/* %files java -%{_javadir}/*.jar +%{_javadir}/CVC4.jar %{_jnidir}/%{name}/ +%files python3 +%{python3_sitearch}/CVC4.py +%{python3_sitearch}/_CVC4.so +%{python3_sitearch}/__pycache__/CVC4.* + %changelog +* Wed Jun 12 2019 Jerry James - 1.7-1 +- New upstream release +- Drop -autoconf, -cadical, -doxygen, -symfpu, and -vec patches +- Drop -doc subpackage; upstream no longer supports doxygen +- Build with python 3 instead of python 2 +- Build with drat2er support +- Add -abc and -flags patches +- Add -swig4 patch (bz 1707353) + * Sun Feb 17 2019 Igor Gnatenko - 1.6-6 - Rebuild for readline 8.0 diff --git a/sources b/sources index 1748ab6..3b9fac1 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (cvc4-1.6.tar.gz) = 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4 +SHA512 (cvc4-1.7.tar.gz) = b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6