New upstream release.
This commit is contained in:
parent
8636619694
commit
a2a8a7c534
3
.gitignore
vendored
3
.gitignore
vendored
@ -1,2 +1 @@
|
||||
/cvc4-1.4.tar.gz
|
||||
/cvc4-1.5.tar.gz
|
||||
/cvc4-*.tar.gz
|
||||
|
@ -1,9 +1,9 @@
|
||||
--- 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
|
||||
--- 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])
|
||||
@ -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],
|
||||
|
50
cvc4-cadical.patch
Normal file
50
cvc4-cadical.patch
Normal file
@ -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++])
|
@ -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
|
@ -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
|
||||
|
@ -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; }
|
14
cvc4-symfpu.patch
Normal file
14
cvc4-symfpu.patch
Normal file
@ -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
|
24
cvc4-vec.patch
Normal file
24
cvc4-vec.patch
Normal file
@ -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;
|
58
cvc4.spec
58
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 <loganjerry@gmail.com> - 1.6-1
|
||||
- New upstream release
|
||||
|
||||
* Wed Feb 07 2018 Fedora Release Engineering <releng@fedoraproject.org> - 1.5-6
|
||||
- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
|
||||
|
||||
|
2
sources
2
sources
@ -1 +1 @@
|
||||
SHA512 (cvc4-1.5.tar.gz) = 654a8e4eee499bce34cc82e002bbcc1ed8e124425a341435750d2dc65097e5e4f6bcf3376663800d644bef0bcdf94b98b862eb5e9f8d63823f416c7775ba17dc
|
||||
SHA512 (cvc4-1.6.tar.gz) = 0887b3f74a4b9e51e634591c7cf39d730110ca5d930149bab4816a49e383eeea8ccadf8474d22f5529cc03ddd045acacf8a2b92434b882adf352f4de4075fcd4
|
||||
|
Loading…
Reference in New Issue
Block a user