rpms/cvc4
3
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

New upstream release.

Browse Source 
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).
This commit is contained in:
Jerry James 2019-06-13 06:32:44 -06:00
parent e594904ab3
commit ded5ca8205
10 changed files with 246 additions and 420 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

54
cvc4-abc.patch Normal file
View File

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

123
cvc4-autoconf.patch
View File

@ -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 <exception>], [[
+ [AC_LANG_PROGRAM([#include <exception>], [[
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],

50
cvc4-cadical.patch
View File

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

72
cvc4-doxygen.patch
View File

@ -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

46
cvc4-flags.patch Normal file
View File

@ -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

44
cvc4-swig4.patch Normal file
View File

@ -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<CVC4::Expr, CVC4::Expr>;
+
#endif // SWIGJAVA
%ignore CVC4::SmtEngine::setLogic(const char*);

14
cvc4-symfpu.patch
View File

@ -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

24
cvc4-vec.patch
View File

@ -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;

237
cvc4.spec
View File

@ -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 <loganjerry@gmail.com> - 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 <ignatenkobrain@fedoraproject.org> - 1.6-6
- Rebuild for readline 8.0

2
sources
View File

@ -1 +1 @@
SHA512 (cvc4-1.6.tar.gz) = 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4
SHA512 (cvc4-1.7.tar.gz) = b91dfac7ddf979a3474f562eb98f2d6f17a53efa38c1be5502429309a0c059e1f2b0d85ee95e5aee17d35f34c825f01f879ec4aaf26025b1fcac835c33a867c6