The package rpms/yices.git has added or updated architecture specific content in its
spec file (ExclusiveArch/ExcludeArch or %ifarch/%ifnarch) in commit(s):
https://src.fedoraproject.org/cgit/rpms/yices.git/commit/?id=26ecb5e37f7c....
Change:
+%ifnarch %{ix86} %{arm}
Thanks.
Full change:
============
commit 26ecb5e37f7ca9b6f55f7769242761890fb434bd
Author: Jerry James <loganjerry(a)gmail.com>
Date: Thu Mar 26 15:26:59 2020 -0600
Disable tests on 32-bit platforms due to failures from overflowing integers.
diff --git a/yices-big-endian.patch b/yices-big-endian.patch
index 005e664..32c6441 100644
--- a/yices-big-endian.patch
+++ b/yices-big-endian.patch
@@ -61,3 +61,18 @@
} rat32_t;
typedef struct {
+--- a/tests/unit/Makefile
++++ b/tests/unit/Makefile
+@@ -84,6 +84,12 @@ static_tests := $(src_c:%.c=$(static_bin
+ libyices := $(libdir)/libyices.a
+ static_libyices := $(static_libdir)/libyices.a
+
++#
++# Whether we are building for a big endian architecture
++#
++ifeq ($(WORDS_BIGENDIAN),yes)
++ CPPFLAGS += -DWORDS_BIGENDIAN
++endif
+
+ #
+ # Whether we have support for mcsat
diff --git a/yices.spec b/yices.spec
index cec23a4..f9274c4 100644
--- a/yices.spec
+++ b/yices.spec
@@ -123,8 +123,10 @@ rm -f %{buildroot}%{_libdir}/libyices.a
mkdir -p %{buildroot}%{_mandir}/man1
cp -p doc/*.1 %{buildroot}%{_mandir}/man1
+%ifnarch %{ix86} %{arm}
%check
make check MODE=debug
+%endif
%files
%doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE
@@ -152,6 +154,8 @@ make check MODE=debug
- Drop upstreamed -missing-typedef patch
- Add -big-endian patch to fix s390x build
- Add -cryptominisat5 patch to fix build with recent cryptominisat releases
+- Skip tests on 32-bit platforms; some tests fail due to the limited size of a
+ C integer
* Fri Jan 31 2020 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.6.1-6
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
commit c31ab501bc80bdc94e078ebae78904c3e087d387
Author: Jerry James <loganjerry(a)gmail.com>
Date: Thu Mar 26 11:48:16 2020 -0600
Version 2.6.2.
Also:
- Drop upstreamed -missing-typedef patch.
- Add -big-endian patch to fix s390x build.
- Add -cryptominisat5 patch to fix build with recent cryptominisat releases.
diff --git a/.gitignore b/.gitignore
index 9ffab0f..6d06f33 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1 +1,2 @@
/Yices-*.tar.gz
+/cudd-*.tar.gz
diff --git a/sources b/sources
index cc68492..5efcc73 100644
--- a/sources
+++ b/sources
@@ -1 +1,2 @@
-SHA512 (Yices-2.6.1.tar.gz) =
586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2
+SHA512 (Yices-2.6.2.tar.gz) =
58990cff2a70d4fae797efdf3c52a15772eb824bc6865682fa64e63b571054eb042a252e52b67b2f89fb191444543f0ad55f9b34086bdd8bcd083ef10422d388
+SHA512 (cudd-3.0.0.tar.gz) =
a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c
diff --git a/yices-big-endian.patch b/yices-big-endian.patch
new file mode 100644
index 0000000..005e664
--- /dev/null
+++ b/yices-big-endian.patch
@@ -0,0 +1,63 @@
+--- a/configure.ac
++++ b/configure.ac
+@@ -152,15 +152,9 @@ dnl
+ dnl Check for endianness
+ dnl --------------------
+ dnl
+-dnl The neorationals code is little-endian only for now.
+-dnl TODO: support big-endian architectures at some point
+-dnl For now, we check here and fail.
+-dnl
+-bigendian=""
+-AC_C_BIGENDIAN([bigendian=yes],[bigendian=no],[bigendian=yes])
+-if test "x$bigendian" = xyes ; then
+- AC_MSG_ERROR([Can't build for your architecture. Yices builds only on
little-endian hardware. Please file an issue at $repo_url])
+-fi
++WORDS_BIGENDIAN=""
++AC_C_BIGENDIAN([WORDS_BIGENDIAN=yes],[WORDS_BIGENDIAN=no],[WORDS_BIGENDIAN=yes])
++AC_SUBST(WORDS_BIGENDIAN)
+
+ dnl
+ dnl CHECK_THREAD_LOCAL
+--- a/make.include.in
++++ b/make.include.in
+@@ -66,6 +66,7 @@ RANLIB=@RANLIB@
+ GPERF=@GPERF@
+ STRIP=@STRIP@
+ NO_STACK_PROTECTOR=@NO_STACK_PROTECTOR@
++WORDS_BIGENDIAN=@WORDS_BIGENDIAN@
+
+ # thread-safe build
+ HAVE_TLS=@HAVE_TLS@
+--- a/src/Makefile
++++ b/src/Makefile
+@@ -595,6 +595,13 @@ libyices_def=libyices.def
+ ###########################
+
+ #
++# Whether we are building for a big endian architecture
++#
++ifeq ($(WORDS_BIGENDIAN),yes)
++ CPPFLAGS += -DWORDS_BIGENDIAN
++endif
++
++#
+ # Whether we have support for mcsat
+ #
+ ifeq ($(ENABLE_MCSAT),yes)
+--- a/src/terms/rationals.h
++++ b/src/terms/rationals.h
+@@ -47,8 +47,13 @@
+ * signed numerator, and a 31 bit unsigned denominator.
+ */
+ typedef struct {
++#ifdef WORDS_BIGENDIAN
++ int32_t num;
++ uint32_t den;
++#else
+ uint32_t den;
+ int32_t num;
++#endif
+ } rat32_t;
+
+ typedef struct {
diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch
new file mode 100644
index 0000000..0e3917a
--- /dev/null
+++ b/yices-cryptominisat.patch
@@ -0,0 +1,114 @@
+--- a/src/solvers/cdcl/delegate.c
++++ b/src/solvers/cdcl/delegate.c
+@@ -21,11 +21,11 @@
+ #include <stdio.h>
+
+ #ifdef HAVE_CADICAL
+-#include "ccadical.h"
++#include <ccadical.h>
+ #endif
+
+ #ifdef HAVE_CRYPTOMINISAT
+-#include "cryptominisat5/cmsat_c.h"
++#include <cryptominisat5/cryptominisat_c.h>
+ #endif
+
+ #include "solvers/cdcl/delegate.h"
+@@ -293,44 +293,44 @@ static void cadical_as_delegate(delegate
+
+ #if HAVE_CRYPTOMINISAT
+ static void cryptominisat_add_empty_clause(void *solver) {
+- cmsat_add_clause(solver, NULL, 0);
++ cmsat_add_clause((SATSolver *)solver, NULL, 0);
+ }
+
+ static void cryptominisat_add_unit_clause(void *solver, literal_t l) {
+- uint32_t c[1];
++ c_Lit c[1];
+
+ assert(l >= 0);
+- c[0] = l;
+- cmsat_add_clause(solver, c, 1);
++ c[0].x = l;
++ cmsat_add_clause((SATSolver *)solver, c, 1);
+ }
+
+ static void cryptominisat_add_binary_clause(void *solver, literal_t l1, literal_t l2) {
+- uint32_t c[2];
++ c_Lit c[2];
+
+ assert(l1 >= 0 && l2 >= 0);
+- c[0] = l1;
+- c[1] = l2;
+- cmsat_add_clause(solver, c, 2);
++ c[0].x = l1;
++ c[1].x = l2;
++ cmsat_add_clause((SATSolver *)solver, c, 2);
+ }
+
+ static void cryptominisat_add_ternary_clause(void *solver, literal_t l1, literal_t l2,
literal_t l3) {
+- uint32_t c[3];
++ c_Lit c[3];
+
+ assert(l1 >= 0 && l2 >= 0 && l3 >= 0);
+- c[0] = l1;
+- c[1] = l2;
+- c[2] = l3;
+- cmsat_add_clause(solver, c, 3);
++ c[0].x = l1;
++ c[1].x = l2;
++ c[2].x = l3;
++ cmsat_add_clause((SATSolver *)solver, c, 3);
+ }
+
+ static void cryptominisat_add_clause(void *solver, uint32_t n, literal_t *a) {
+- cmsat_add_clause(solver, (uint32_t*) a, n);
++ cmsat_add_clause((SATSolver *)solver, (c_Lit *)a, n);
+ }
+
+ static smt_status_t cryptominisat_check(void *solver) {
+- switch (cmsat_solve(solver)) {
+- case CMSAT_SAT: return STATUS_SAT;
+- case CMSAT_UNSAT: return STATUS_UNSAT;
++ switch (cmsat_solve((SATSolver *)solver).x) {
++ case L_TRUE: return STATUS_SAT;
++ case L_FALSE: return STATUS_UNSAT;
+ default: return STATUS_UNKNOWN;
+ }
+ }
+@@ -341,28 +341,23 @@ static smt_status_t cryptominisat_check(
+ * that cryptominisat always produces a full truth assignment.
+ */
+ static bval_t cryptominisat_get_value(void *solver, bvar_t x) {
+- switch (cmsat_var_value(solver, x)) {
+- case CMSAT_VAL_TRUE:
++ slice_lbool model = cmsat_get_model((SATSolver *)solver);
++ if ((size_t)x < model.num_vals && model.vals[x].x == L_TRUE)
+ return VAL_TRUE;
+-
+- case CMSAT_VAL_FALSE:
+- default:
+- return VAL_FALSE;
+- }
++ return VAL_FALSE;
+ }
+
+-static void cryptominisat_set_verbosity(void *solver, uint32_t level) {
++static void cryptominisat_set_verbosity(void *solver __attribute__((unused)), uint32_t
level __attribute__((unused))) {
+ // verbosity 0 --> quiet (this is the default)
+- cmsat_set_verbosity(solver, level);
+ }
+
+ static void cryptominisat_delete(void *solver) {
+- cmsat_free_solver(solver);
++ cmsat_free((SATSolver *)solver);
+ }
+
+ static void cryptominisat_as_delegate(delegate_t *d, uint32_t nvars) {
+- d->solver = cmsat_new_solver();
+- cmsat_new_vars(d->solver, nvars);
++ d->solver = cmsat_new();
++ cmsat_new_vars((SATSolver *)d->solver, nvars);
+ init_ivector(&d->buffer, 0); // not used
+ d->add_empty_clause = cryptominisat_add_empty_clause;
+ d->add_unit_clause = cryptominisat_add_unit_clause;
diff --git a/yices-missing-typedef.patch b/yices-missing-typedef.patch
deleted file mode 100644
index 9528060..0000000
--- a/yices-missing-typedef.patch
+++ /dev/null
@@ -1,13 +0,0 @@
-https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b62d2513a
-
---- a/src/frontend/smt2/smt2_commands.h
-+++ b/src/frontend/smt2/smt2_commands.h
-@@ -129,7 +129,7 @@ enum smt2_errors {
- * - array theory sort and functions
- * - processing of term annotations
- */
--enum smt2_opcodes {
-+typedef enum smt2_opcodes {
- SMT2_EXIT = NUM_BASE_OPCODES, // [exit]
- SMT2_SILENT_EXIT, // [silent-exit]
- SMT2_GET_ASSERTIONS, // [get-assertions]
diff --git a/yices.spec b/yices.spec
index b16384b..cec23a4 100644
--- a/yices.spec
+++ b/yices.spec
@@ -1,21 +1,37 @@
Name: yices
-Version: 2.6.1
-Release: 6%{?dist}
+Version: 2.6.2
+Release: 1%{?dist}
Summary: SMT solver
-License: GPLv3+
+# The yices code is GPLv3+. The cudd code is BSD.
+License: GPLv3+ and BSD
URL:
http://yices.csl.sri.com/
Source0:
https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz
-#
https://github.com/SRI-CSL/yices2/commit/fadc2d5b303cef258cde295a0af2799b...
-Patch0: %{name}-missing-typedef.patch
-
+# The CUDD web site disappeared in 2018. The Fedora package was retired in 2019
+# when there were no more Fedora users. Instead of resurrecting the package for
+# the sole use of yices, we bundle a snapshot of the last released version.
+Source1:
https://github.com/ivmai/cudd/archive/cudd-3.0.0.tar.gz
+# Fix the build on big endian machines
+#
https://github.com/SRI-CSL/yices2/pull/185
+Patch0: %{name}-big-endian.patch
+# Adapt to newer versions of cryptominisat
+Patch1: %{name}-cryptominisat.patch
+
+BuildRequires: cadical-devel
+BuildRequires: cryptominisat-devel
BuildRequires: gcc
+BuildRequires: gcc-c++
BuildRequires: gmp-devel
BuildRequires: gperf
+BuildRequires: latexmk
BuildRequires: libpoly-devel
BuildRequires: libtool
+BuildRequires: python3dist(sphinx)
BuildRequires: tex(latex)
+# See Source1 comment
+Provides: bundled(cudd) = 3.0.0
+
%description
Yices 2 is an efficient SMT solver that decides the satisfiability of
formulas containing uninterpreted function symbols with equality, linear
@@ -54,9 +70,13 @@ This package contains yices documentation.
%prep
%autosetup -n yices2-Yices-%{version} -p1
+%setup -q -n yices2-Yices-%{version} -T -D -a 1
# Do not try to avoid -fstack-protector
-sed -i '/NO_STACK_PROTECTOR=""/,/AC_SUBST(NO_STACK_PROTECTOR)/d'
configure.ac
+sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in
+
+# Do not override our build flags
+sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile
# Generate the configure script
autoreconf -fi
@@ -68,20 +88,32 @@ sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys
sed -i 's/cp/install -m 0644/' utils/make_source_version
%build
+# Build cudd
+cd cudd-cudd-3.0.0
+%configure CFLAGS="%{optflags} -fPIC" CXXFLAGS="%{optflags} -fPIC"
+%make_build
+cd -
+
#bv64_interval_abstraction depends on wrapping for signed overflow
%global optflags %{optflags} -fwrapv
+export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL
-DHAVE_CRYPTOMINISAT"
+export LDFLAGS="$RPM_LD_FLAGS -L$PWD/cudd-cudd-3.0.0/cudd/.libs"
+export LIBS="-lcadical -lcryptominisat5"
%configure --enable-mcsat
-mv configs/make.include.%{_host} configs/make.include.$(./config.guess)
-make %{?_smp_mflags} MODE=debug
+
+guess=$(./config.guess)
+if [ "%{_host}" != "$guess" ]; then
+ mv configs/make.include.%{_host} configs/make.include.${guess}
+fi
+%make_build MODE=debug
# Build the manual
-pushd doc/manual
-pdflatex manual
-bibtex manual
-pdflatex manual
-pdflatex manual
-popd
+make doc
+
+# Build the interface documentation
+make -C doc/sphinx html
+rm doc/sphinx/build/html/.buildinfo
%install
make install prefix=%{buildroot}%{_prefix} exec_prefix=%{buildroot}%{_prefix} \
@@ -95,8 +127,8 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1
make check MODE=debug
%files
-%doc doc/YICES-LANGUAGE
-%license LICENSE.txt
+%doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE
+%license copyright.txt LICENSE.txt
%{_libdir}/*.so.2*
%files devel
@@ -111,10 +143,16 @@ make check MODE=debug
%{_mandir}/man1/*
%files doc
-%doc doc/manual/manual.pdf examples
-%license LICENSE.txt
+%doc doc/manual/manual.pdf doc/sphinx/build/html examples
+%license copyright.txt LICENSE.txt
%changelog
+* Thu Mar 26 2020 Jerry James <loganjerry(a)gmail.com> - 2.6.2-1
+- Version 2.6.2
+- Drop upstreamed -missing-typedef patch
+- Add -big-endian patch to fix s390x build
+- Add -cryptominisat5 patch to fix build with recent cryptominisat releases
+
* Fri Jan 31 2020 Fedora Release Engineering <releng(a)fedoraproject.org> - 2.6.1-6
- Rebuilt for
https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild