diff --git a/.gitignore b/.gitignore index 13dc190..93e2f5f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,2 +1 @@ -/cvc4-1.4.tar.gz -/cvc4-1.5.tar.gz +/cvc4-*.tar.gz diff --git a/cvc4-autoconf.patch b/cvc4-autoconf.patch index 47c9175..373b81a 100644 --- a/cvc4-autoconf.patch +++ b/cvc4-autoconf.patch @@ -1,11 +1,11 @@ ---- config/abc.m4.orig 2017-06-23 15:54:52.168048722 -0600 -+++ config/abc.m4 2017-08-20 20:14:22.805836603 -0600 -@@ -26,21 +26,17 @@ elif test -n "$with_abc"; then - fi - ] - ) +--- 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 ++ 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 @@ -26,18 +26,17 @@ 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 2017-06-23 15:54:52.169048740 -0600 -+++ config/antlr.m4 2017-08-20 16:50:37.987445083 -0600 -@@ -30,7 +30,7 @@ been generated already. To obtain ANTLR - ANTLR_VERSION="`$ANTLR -version 2>&1 | sed 's,.*Version *\([[0-9.]]*\).*,\1,'`" +--- 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.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 -@@ -121,8 +121,8 @@ AC_DEFUN([AC_LIB_ANTLR],[ +@@ -130,8 +131,8 @@ AC_DEFUN([AC_LIB_ANTLR],[ } ])], [ @@ -48,8 +47,8 @@ AC_MSG_WARN([your antlr parser generator is version $ANTLR_VERSION, which doesn't match the library!]) fi ], ---- config/boost.m4.orig 2017-06-23 15:54:52.173048811 -0600 -+++ config/boost.m4 2017-08-20 16:51:21.940334791 -0600 +--- 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. @@ -59,23 +58,18 @@ grep -v "^#" | tr -d '\r\n ' | $SED -n -e "$1" >conftest.i 2>&1], ---- config/cryptominisat.m4.orig 2017-06-23 15:54:52.175048847 -0600 -+++ config/cryptominisat.m4 2017-08-20 20:37:04.578276194 -0600 -@@ -27,11 +27,11 @@ elif test -n "$with_cryptominisat"; then - ] - ) +--- 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/cryptominisat" ; then +- 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 -- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include" -+ CPPFLAGS="$CPPFLAGS -I/usr/include/cryptominisat4" - - AC_MSG_CHECKING([how to link cryptominisat]) - -@@ -47,7 +47,7 @@ elif test -n "$with_cryptominisat"; then +@@ -54,7 +54,7 @@ elif test -n "$with_cryptominisat"; then have_libcryptominisat=1 fi @@ -84,18 +78,20 @@ else AC_MSG_RESULT([no, user didn't request cryptominisat]) -@@ -67,7 +67,7 @@ if test -z "$CRYPTOMINISAT_LIBS"; then +@@ -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="" - LIBS="-lcryptominisat4 $1" ++ CPPFLAGS="$CPPFLAGS -I/usr/include/cryptominisat5" + LIBS="-lcryptominisat5 $1" AC_LINK_IFELSE( ---- configure.ac.orig 2017-07-10 11:00:06.970280980 -0600 -+++ configure.ac 2017-08-20 16:49:09.874665731 -0600 -@@ -257,7 +257,7 @@ if test $cross_compiling = "no"; then +--- 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( @@ -104,7 +100,7 @@ int result = 1; try { throw std::exception(); -@@ -265,7 +265,7 @@ if test $cross_compiling = "no"; then +@@ -302,7 +302,7 @@ if test $cross_compiling = "no"; then result = 0; } return result; @@ -113,7 +109,7 @@ [AC_MSG_RESULT([yes])], [AC_MSG_ERROR([C++ exceptions do not work.])] ) -@@ -612,10 +612,6 @@ fi +@@ -657,11 +657,6 @@ fi AC_MSG_RESULT([$enable_debug_symbols]) @@ -121,6 +117,7 @@ - CVC4CXXFLAGS="${CVC4CXXFLAGS:+$CVC4CXXFLAGS }-ggdb3" - CVC4CFLAGS="${CVC4CFLAGS:+$CVC4CFLAGS }-ggdb3" -fi +- + AC_MSG_CHECKING([whether to enable Valgrind instrumentation]) - AC_MSG_CHECKING([whether to include statistics are turned on in libcvc4]) - + AC_ARG_ENABLE([valgrind], diff --git a/cvc4-cadical.patch b/cvc4-cadical.patch new file mode 100644 index 0000000..bdd21b5 --- /dev/null +++ b/cvc4-cadical.patch @@ -0,0 +1,50 @@ +--- 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-constant.patch b/cvc4-constant.patch deleted file mode 100644 index b817da3..0000000 --- a/cvc4-constant.patch +++ /dev/null @@ -1,25 +0,0 @@ ---- src/theory/datatypes/kinds.orig 2017-06-23 15:54:52.988063375 -0600 -+++ src/theory/datatypes/kinds 2017-07-15 20:30:31.268986539 -0600 -@@ -108,4 +108,22 @@ typerule DT_SIZE ::CVC4::theory::datatyp - operator DT_HEIGHT_BOUND 2 "datatypes height bound" - typerule DT_HEIGHT_BOUND ::CVC4::theory::datatypes::DtHeightBoundTypeRule - -+constant TUPLE_SELECT_OP \ -+ ::CVC4::TupleSelect \ -+ ::CVC4::TupleSelectHashFunction \ -+ "util/tuple.h" \ -+ "operator for a tuple select" -+ -+constant RECORD_OP \ -+ ::CVC4::Record \ -+ ::CVC4::RecordHashFunction \ -+ "expr/record.h" \ -+ "operator for a record" -+ -+constant RECORD_SELECT_OP \ -+ ::CVC4::RecordSelect \ -+ ::CVC4::RecordSelectHashFunction \ -+ "expr/record.h" \ -+ "operator for a record select" -+ - endtheory diff --git a/cvc4-doxygen.patch b/cvc4-doxygen.patch index c15b89b..1b83f24 100644 --- a/cvc4-doxygen.patch +++ b/cvc4-doxygen.patch @@ -1,23 +1,14 @@ ---- src/base/tls.h.in.orig 2017-07-07 16:15:02.906706503 -0600 -+++ src/base/tls.h.in 2017-07-12 19:10:48.346237676 -0600 -@@ -1,5 +1,5 @@ - /********************* */ --/*! \file tls.h.in -+/*! \file tls.h - ** \verbatim - ** Top contributors (to current version): - ** Morgan Deters, ACSYS, Paul Meng ---- src/expr/expr_manager_template.cpp.orig 2017-07-07 16:15:02.958707425 -0600 -+++ src/expr/expr_manager_template.cpp 2017-07-12 19:09:30.706471535 -0600 +--- 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, Tim King, Christopher L. Conway ---- src/expr/expr_manager_template.h.orig 2017-07-07 16:15:02.959707443 -0600 -+++ src/expr/expr_manager_template.h 2017-07-12 19:07:01.962904981 -0600 + ** 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 @@ -25,57 +16,57 @@ ** \verbatim ** Top contributors (to current version): ** Morgan Deters, Dejan Jovanovic, Christopher L. Conway ---- src/expr/expr_template.h.orig 2017-07-07 16:15:02.962707496 -0600 -+++ src/expr/expr_template.h 2017-07-12 19:07:17.361860105 -0600 +--- 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, Christopher L. Conway ---- src/expr/kind_template.h.orig 2017-07-07 16:15:02.964707531 -0600 -+++ src/expr/kind_template.h 2017-07-12 19:07:36.314804876 -0600 + ** 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, Paul Meng ---- src/expr/metakind_template.h.orig 2017-07-07 16:15:02.966707567 -0600 -+++ src/expr/metakind_template.h 2017-07-12 19:08:17.474684935 -0600 + ** 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, Paul Meng, Tim King ---- src/expr/type_checker_template.cpp.orig 2017-07-07 16:15:02.991708010 -0600 -+++ src/expr/type_checker_template.cpp 2017-07-12 19:08:59.234563245 -0600 + ** 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, Paul Meng ---- src/expr/type_properties_template.h.orig 2017-07-07 16:15:02.995708080 -0600 -+++ src/expr/type_properties_template.h 2017-07-12 19:08:31.650643627 -0600 + ** 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, Paul Meng, Tim King ---- src/util/rational.h.in.orig 2017-07-07 16:15:03.587718569 -0600 -+++ src/util/rational.h.in 2017-07-12 19:11:15.186152866 -0600 + ** 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, Paul Meng, Tim King + ** Morgan Deters, Tim King diff --git a/cvc4-libs.patch b/cvc4-libs.patch deleted file mode 100644 index 62b3c99..0000000 --- a/cvc4-libs.patch +++ /dev/null @@ -1,47 +0,0 @@ ---- configure.orig 2017-07-10 11:00:38.291785982 -0600 -+++ configure 2017-07-15 12:34:56.893412904 -0600 -@@ -20324,7 +20324,7 @@ See \`config.log' for more details" "$LI - - fi - -- if ! test -d "$ABC_HOME" || ! test -x "$ABC_HOME/arch_flags"; then -+ if ! test -d "$ABC_HOME" ; then - { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 - $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} - as_fn_error $? "either $ABC_HOME is not an abc source tree or it's not yet built -@@ -20333,15 +20333,15 @@ See \`config.log' for more details" "$LI - - { $as_echo "$as_me:${as_lineno-$LINENO}: checking for arch_flags to use with libabc" >&5 - $as_echo_n "checking for arch_flags to use with libabc... " >&6; } -- libabc_arch_flags="$("$ABC_HOME/arch_flags")" -+ libabc_arch_flags="" - { $as_echo "$as_me:${as_lineno-$LINENO}: result: $libabc_arch_flags" >&5 - $as_echo "$libabc_arch_flags" >&6; } -- CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/src $libabc_arch_flags" -+ CVC4CPPFLAGS="${CVC4CPPFLAGS:+$CVC4CPPFLAGS }-I$ABC_HOME/include/abc" - ABC_LDFLAGS="-L$ABC_HOME" - - cvc4_save_LDFLAGS="$LDFLAGS" - ABC_LIBS= -- CPPFLAGS="$CPPFLAGS -I$ABC_HOME/src $libabc_arch_flags" -+ CPPFLAGS="$CPPFLAGS -I$ABC_HOME/include/abc" - LDFLAGS="$LDFLAGS $ABC_LDFLAGS" - ac_fn_c_check_header_mongrel "$LINENO" "base/abc/abc.h" "ac_cv_header_base_abc_abc_h" "$ac_includes_default" - if test "x$ac_cv_header_base_abc_abc_h" = xyes; then : -@@ -21274,14 +21274,14 @@ See \`config.log' for more details" "$LI - fi - - -- if ! test -d "$CRYPTOMINISAT_HOME" || ! test -x "$CRYPTOMINISAT_HOME/install/bin/cryptominisat" ; then -+ if ! test -d "$CRYPTOMINISAT_HOME" ; then - { { $as_echo "$as_me:${as_lineno-$LINENO}: error: in \`$ac_pwd':" >&5 - $as_echo "$as_me: error: in \`$ac_pwd':" >&2;} - as_fn_error $? "either $CRYPTOMINISAT_HOME is not an cryptominisat install tree or it's not yet built - See \`config.log' for more details" "$LINENO" 5; } - fi - -- CPPFLAGS="$CPPFLAGS -I$CRYPTOMINISAT_HOME/install/include" -+ CPPFLAGS="$CPPFLAGS -I/usr/include/cryptominisat4" - - { $as_echo "$as_me:${as_lineno-$LINENO}: checking how to link cryptominisat" >&5 - $as_echo_n "checking how to link cryptominisat... " >&6; } diff --git a/cvc4-symfpu.patch b/cvc4-symfpu.patch new file mode 100644 index 0000000..727f167 --- /dev/null +++ b/cvc4-symfpu.patch @@ -0,0 +1,14 @@ +--- 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 new file mode 100644 index 0000000..d145d1e --- /dev/null +++ b/cvc4-vec.patch @@ -0,0 +1,24 @@ +--- 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 2f1b88e..ee581a6 100644 --- a/cvc4.spec +++ b/cvc4.spec @@ -2,8 +2,8 @@ # we currently build without glpk support. Name: cvc4 -Version: 1.5 -Release: 6%{?dist} +Version: 1.6 +Release: 1%{?dist} Summary: Automatic theorem prover for SMT problems # License breakdown: @@ -11,29 +11,30 @@ Summary: Automatic theorem prover for SMT problems # o src/util/channel.h # o examples/hashsmt/sha1.hpp # - Files containing code under the BSD license: -# o proofs/lfsc_checker/* # o src/parser/antlr_input_imports.cpp # o src/parser/bounded_token_buffer.cpp # - All other files are distributed under the MIT license -# But we link with readline, so it all gets subsumed by GPLv3+ anyway. -License: GPLv3+ +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 -# Adapt to the way the Fedora libraries are constructed. -Patch1: %{name}-libs.patch -# Fix undefined symbols in the JNI interface -Patch2: %{name}-constant.patch # Fix various autoconf problems -Patch3: %{name}-autoconf.patch +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 BuildRequires: abc-devel BuildRequires: antlr3-C-devel BuildRequires: antlr3-tool BuildRequires: boost-devel +BuildRequires: cadical-devel BuildRequires: chrpath -BuildRequires: cryptominisat4-devel +BuildRequires: cryptominisat-devel BuildRequires: cxxtest BuildRequires: doxygen-latex BuildRequires: gcc-c++ @@ -41,11 +42,13 @@ BuildRequires: ghostscript BuildRequires: gmp-devel BuildRequires: java-devel BuildRequires: jpackage-utils +BuildRequires: lfsc-devel BuildRequires: libtool BuildRequires: perl-interpreter BuildRequires: python2 BuildRequires: readline-devel BuildRequires: swig +BuildRequires: symfpu-devel Requires: %{name}-libs%{?_isa} = %{version}-%{release} @@ -97,13 +100,9 @@ Requires: jpackage-utils Java interface to %{name}. %prep -%setup -q -%patch0 -%patch1 -%patch2 -%patch3 +%autosetup -p0 -# Regenerate due to patch 3 +# Regenerate configure due to patch 1 autoreconf -fi # Do not override Fedora's optimization settings @@ -130,12 +129,6 @@ sed -e "s|^\(javalibdir =.*\)jni|\1java/%{name}|" \ sed -e 's/Kind k;/Kind k = kind::UNDEFINED_KIND;/' \ -i src/parser/cvc/CvcParser.c -# Make lfsc documentation available -cp -p proofs/lfsc_checker/AUTHORS AUTHORS.lfsc -cp -p proofs/lfsc_checker/COPYING COPYING.lfsc -cp -p proofs/lfsc_checker/NEWS NEWS.lfsc -cp -p proofs/lfsc_checker/README README.lfsc - # Help the documentation generator cp -p COPYING src/bindings/compat/c @@ -149,7 +142,7 @@ sed -i 's,@CXXTEST@,%{_includedir}/cxxtest,' test/unit/Makefile.am %build export CPPFLAGS="-I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc" -if [ "%{__isa_bits}" == "64" ]; then +if [ "%{__isa_bits}" = "64" ]; then CPPFLAGS+=" -DLIN64" else CPPFLAGS+=" -DLIN" @@ -157,9 +150,13 @@ 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 --with-abc --with-abc-dir=%{_prefix} \ - --with-cryptominisat --with-cryptominisat-dir=%{_prefix} --with-readline \ - --without-compat + --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 # Workaround libtool reordering -Wl,--as-needed after all the libraries BUILDS=$(echo $PWD/builds/*linux*/*abc*) @@ -230,14 +227,14 @@ export LD_LIBRARY_PATH=%{buildroot}%{_libdir} make check %files -%doc AUTHORS AUTHORS.lfsc NEWS NEWS.lfsc README README.lfsc RELEASE-NOTES THANKS -%license COPYING.lfsc +%doc AUTHORS NEWS README RELEASE-NOTES THANKS %{_bindir}/* %{_datadir}/%{name}/ %{_mandir}/man1/* %{_mandir}/man5/* %files doc +%license COPYING %doc doc/doxygen/* %files libs @@ -254,6 +251,9 @@ make check %{_jnidir}/%{name}/ %changelog +* Tue Jul 10 2018 Jerry James - 1.6-1 +- New upstream release + * Wed Feb 07 2018 Fedora Release Engineering - 1.5-6 - Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild diff --git a/sources b/sources index fec4061..1748ab6 100644 --- a/sources +++ b/sources @@ -1 +1 @@ -SHA512 (cvc4-1.5.tar.gz) = 654a8e4eee499bce34cc82e002bbcc1ed8e124425a341435750d2dc65097e5e4f6bcf3376663800d644bef0bcdf94b98b862eb5e9f8d63823f416c7775ba17dc +SHA512 (cvc4-1.6.tar.gz) = 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4