Rebuilt for https://fedoraproject.org/wiki/Fedora_45_Mass_Rebuild

Using the current date breaks build reproducibility.

.gitignore

@@ -1 +1,3 @@
 /Yices-*.tar.gz
+/yices-*.tar.gz
+/cudd-*.tar.gz

README.md

@@ -0,0 +1,11 @@
+# yices
+
+[Yices 2](https://yices.csl.sri.com/) is a solver for
+[Satisfiability Modulo Theories](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)
+(SMT) problems.  Yices 2 can process input written in the SMT-LIB language, or
+in Yices' own specification language.  The package provides a
+[C API](https://github.com/SRI-CSL/yices2/blob/master/src/include/yices.h).
+Separately, bindings for [Java](https://github.com/SRI-CSL/yices2_java_bindings),
+[Python](https://github.com/SRI-CSL/yices2_python_bindings),
+[Go](https://github.com/SRI-CSL/yices2_go_bindings), and
+[OCaml](https://github.com/SRI-CSL/yices2_ocaml_bindings) are available.

changelog

@@ -0,0 +1,109 @@
+* Tue Feb 20 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-12
+- Fix the SPDX expression
+
+* Fri Feb  9 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-11
+- Rebuild for cryptominisat 5.11.21
+
+* Wed Jan 31 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-10
+- Rebuild for cryptominisat 5.11.15
+
+* Sat Jan 27 2024 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-9
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild
+
+* Wed Jan 10 2024 Jerry James <loganjerry@gmail.com> - 2.6.4-8
+- Rebuild for cadical 1.9.4
+- Update font licenses from LPPL-1.0 to LPPL-1.3a
+- Stop building for 32-bit x86
+
+* Sat Jul 22 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild
+
+* Sat Jan 21 2023 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild
+
+* Mon Nov 28 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-5
+- Regenerate the cudd configure script to fix FTBFS
+- Convert License tag to SPDX
+
+* Mon Nov 28 2022 Timm Bäder <tbaeder@redhat.com> - 2.6.4-5
+- Get rid of an implicit int function declaration in a configure check
+
+* Sat Jul 23 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild
+
+* Sat Jan 22 2022 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.4-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild
+
+* Tue Jan 11 2022 Jerry James <loganjerry@gmail.com> - 2.6.4-2
+- Build with kissat support
+
+* Mon Oct 25 2021 Jerry James <loganjerry@gmail.com> - 2.6.4-1
+- Version 2.6.4
+- Drop upstreamed -big-endian and -sphinx3 patches
+- Enable tests on 32-bit platforms
+
+* Fri Jul 23 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-8
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild
+
+* Thu Jan 28 2021 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-7
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild
+
+* Fri Nov 27 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-6
+- Rebuild for cryptominisat 5.8.0
+
+* Mon Aug  3 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-5
+- Rebuild for cadical 1.3.0
+
+* Wed Jul 29 2020 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.2-4
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild
+
+* Sat Apr 25 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-3
+- Rebuild for cryptominisat 5.7.0
+- Switch to upstream's solution for sphinx 3 support
+
+* Thu Apr 16 2020 Jerry James <loganjerry@gmail.com> - 2.6.2-2
+- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515)
+
+* Thu Mar 26 2020 Jerry James <loganjerry@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
+- 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@fedoraproject.org> - 2.6.1-6
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild
+
+* Thu Jan 23 2020 Jerry James <loganjerry@gmail.com> - 2.6.1-5
+- Add -missing-typedef patch to fix FTBFS with gcc 10
+- Set -doc subpackage to noarch
+
+* Fri Nov 22 2019 Jerry James <loganjerry@gmail.com> - 2.6.1-4
+- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis
+
+* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
+
+* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
+
+* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
+- New upstream version
+
+* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
+
+* Wed Jul  4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
+- New upstream version
+
+* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
+- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
+
+* Tue Jan  2 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-2
+- Add a -doc subpackage
+- Fix end of line encodings
+- Fix permissions on yices_debug_version.c
+
+* Mon Jan  1 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-1
+- Initial RPM

implicit-int.patch

@@ -0,0 +1,12 @@
+diff -ruN yices2-Yices-2.6.4/cudd-cudd-3.0.0/configure.ac yices2-Yices-2.6.4.orig/cudd-cudd-3.0.0/configure.ac
+--- a/cudd-cudd-3.0.0/configure.ac	2016-01-20 23:59:33.000000000 +0100
++++ b/cudd-cudd-3.0.0/configure.ac	2022-11-28 12:32:24.297791070 +0100
+@@ -131,7 +131,7 @@
+ AC_CACHE_VAL(ac_cv_have_ieee_754,
+ [ AC_TRY_RUN([
+ #include <math.h>
+-main(void)
++int main(void)
+ {
+     if (HUGE_VAL != HUGE_VAL * 3 || HUGE_VAL != HUGE_VAL / 3) return 1;
+     return 0;

sources

@@ -1 +1,2 @@
-SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2
+SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92
+SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c

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 <cadical/ccadical.h>
+ #endif
+ 
+ #ifdef HAVE_CRYPTOMINISAT
+-#include "cryptominisat5/cmsat_c.h"
++#include <cryptominisat5/cryptominisat_c.h>
+ #endif
+ 
+ #ifdef HAVE_KISSAT
+@@ -308,44 +308,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 YICES_STATUS_SAT;
+-  case CMSAT_UNSAT: return YICES_STATUS_UNSAT;
++  switch (cmsat_solve((SATSolver *)solver).x) {
++  case L_TRUE: return YICES_STATUS_SAT;
++  case L_FALSE: return YICES_STATUS_UNSAT;
+   default: return YICES_STATUS_UNKNOWN;
+   }
+ }
+@@ -356,28 +356,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;

yices.spec

@@ -1,29 +1,66 @@
+%global giturl  https://github.com/SRI-CSL/yices2
+
 Name:           yices
-Version:        2.6.1
-Release:        3%{?dist}
+Version:        2.7.0
+Release:        %autorelease
 Summary:        SMT solver
 
-License:        GPLv3+
+# The yices code is GPL-3.0-or-later.  The cudd code is BSD-3-Clause.
+License:        GPL-3.0-or-later AND BSD-3-Clause
 URL:            http://yices.csl.sri.com/
-Source0:        https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz
+VCS :           git:%{giturl}.git
+Source0:        %{giturl}/archive/yices-%{version}.tar.gz
+# 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
+# Adapt to newer versions of cryptominisat
+Patch:          %{name}-cryptominisat.patch
+# Get rid of an implicit-int function declaration in a configure check.
+Patch:          implicit-int.patch
 
+# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
+ExcludeArch:    %{ix86}
+
+BuildRequires:  cadical-devel
+BuildRequires:  cryptominisat-devel
 BuildRequires:  gcc
+BuildRequires:  gcc-c++
 BuildRequires:  gmp-devel
 BuildRequires:  gperf
+BuildRequires:  kissat-devel
+BuildRequires:  latexmk
 BuildRequires:  libpoly-devel
 BuildRequires:  libtool
-BuildRequires:  tex(latex)
+BuildRequires:  make
+BuildRequires:  %{py3_dist sphinx}
+BuildRequires:  tex(amsfonts.sty)
+BuildRequires:  tex(cite.sty)
+BuildRequires:  tex(epstopdf.sty)
+BuildRequires:  tex(listings.sty)
+BuildRequires:  tex(xcolor.sty)
+BuildRequires:  texlive-bibtex
+BuildRequires:  texlive-cm
+BuildRequires:  texlive-courier
+BuildRequires:  texlive-ec
+BuildRequires:  texlive-helvetic
+BuildRequires:  texlive-latex
+BuildRequires:  texlive-makeindex
+BuildRequires:  texlive-times
+
+# 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
-real and integer arithmetic, bitvectors, scalar types, and tuples.
+Yices 2 is an efficient SMT solver that decides the satisfiability of formulas
+containing uninterpreted function symbols with equality, linear real and
+integer arithmetic, bitvectors, scalar types, and tuples.
 
-Yices 2 can process input written in the SMT-LIB notation (both versions
-2.0 and 1.2 are supported).
+Yices 2 can process input written in the SMT-LIB notation (both versions 2.0
+and 1.2 are supported).
 
-Alternatively, you can write specifications using the Yices 2
-specification language, which includes tuples and scalar types.
+Alternatively, you can write specifications using the Yices 2 specification
+language, which includes tuples and scalar types.
 
 Yices 2 can also be used as a library in other software.
 
@@ -33,8 +70,8 @@ Requires:       %{name}%{?_isa} = %{version}-%{release}
 Requires:       gmp-devel%{?_isa}
 
 %description devel
-This package contains the header files necessary for developing programs
-which use yices.
+This package contains the header files necessary for developing programs which
+use yices.
 
 %package tools
 Summary:        Command line tools that use the yices library
@@ -44,19 +81,60 @@ Requires:       %{name}%{?_isa} = %{version}-%{release}
 Command line tools that use the yices library.
 
 %package doc
+# The content is GPL-3.0-or-later.  Other licenses are due to files copied in
+# by Sphinx and due to fonts embedded in PDFs.
+# Sphinx file licenses:
+# _static/_sphinx_javascript_frameworks_compat.js: BSD-2-Clause
+# _static/basic.css: BSD-2-Clause
+# _static/classic.css: BSD-2-Clause
+# _static/default.css: BSD-2-Clause
+# _static/doctools.js: BSD-2-Clause
+# _static/documentation_options.js: BSD-2-Clause
+# _static/epub.css: BSD-2-Clause
+# _static/file.png: BSD-2-Clause
+# _static/jquery*.js: MIT
+# _static/language_data.js: BSD-2-Clause
+# _static/minus.png: BSD-2-Clause
+# _static/plus.png: BSD-2-Clause
+# _static/searchtools.js: BSD-2-Clause
+# _static/sidebar.js: BSD-2-Clause
+# _static/underscore*.js: MIT
+# genindex.html: BSD-2-Clause
+# search.html: BSD-2-Clause
+# searchindex.js: BSD-2-Clause
+#
+# Font licenses:
+# AMS: OFL-1.1-RFN
+# CM: Knuth-CTAN
+# DejaVu: LPPL-1.3a
+# LaTeX: LPPL-1.3a
+# Nimbus: AGPL-3.0-only
+License:        GPL-3.0-or-later AND BSD-2-Clause AND MIT AND OFL-1.1-RFN AND Knuth-CTAN AND LPPL-1.3a AND AGPL-3.0-only
 Summary:        Documentation for yices
+BuildArch:      noarch
 
 %description doc
 This package contains yices documentation.
 
 %prep
-%setup -q -n yices2-Yices-%{version}
+%autosetup -n yices2-yices-%{version} -a 1 -p1
 
+%conf
 # 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
 
-# Generate the configure script
+# Do not override our build flags
+sed -i 's/ -O3//;s/ -fomit-frame-pointer//' src/Makefile tests/unit/Makefile
+
+# Use $SOURCE_DATE_EPOCH (or current date)
+sed -i "s/^now=.*/now=$(date +%Y-%m-%d ${SOURCE_DATE_EPOCH:+--date=@$SOURCE_DATE_EPOCH})/" \
+  utils/make_source_version
+
+# Generate the configure scripts
 autoreconf -fi
+cd cudd-cudd-3.0.0
+autoreconf -fi
+cd -
 
 # Fix end of line encodings
 sed -i 's/\r//' examples/{jinpeng,problem_with_input}.ys
@@ -65,17 +143,29 @@ 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='%{build_cflags} -fPIC' CXXFLAGS='%{build_cxxflags} -fPIC'
+%make_build
+cd -
+
+export CPPFLAGS="-I$PWD/cudd-cudd-3.0.0/cudd -DHAVE_CADICAL -DHAVE_CRYPTOMINISAT -DHAVE_KISSAT"
+export LDFLAGS="%{build_ldflags} -L$PWD/cudd-cudd-3.0.0/cudd/.libs"
+export LIBS='-lcadical -lcryptominisat5 -lkissat'
 %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} \
@@ -89,48 +179,27 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1
 make check MODE=debug
 
 %files
-%doc doc/YICES-LANGUAGE
-%license LICENSE.txt
-%{_libdir}/*.so.*
+%doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE
+%license copyright.txt LICENSE.txt
+%{_libdir}/libyices.so.2.7{,.*}
 
 %files devel
 %{_includedir}/%{name}/
-%{_libdir}/*.so
+%{_libdir}/libyices.so
 
 %files tools
 %{_bindir}/yices
 %{_bindir}/yices-sat
 %{_bindir}/yices-smt
 %{_bindir}/yices-smt2
-%{_mandir}/man1/*
+%{_mandir}/man1/yices.1*
+%{_mandir}/man1/yices-sat.1*
+%{_mandir}/man1/yices-smt.1*
+%{_mandir}/man1/yices-smt2.1*
 
 %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
-* Sat Jul 27 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild
-
-* Sun Feb 03 2019 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.1-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild
-
-* Tue Oct 30 2018 Jerry James <loganjerry@gmail.com> - 2.6.1-1
-- New upstream version
-
-* Sat Jul 14 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.6.0-2
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild
-
-* Wed Jul  4 2018 Jerry James <loganjerry@gmail.com> - 2.6.0-1
-- New upstream version
-
-* Fri Feb 09 2018 Fedora Release Engineering <releng@fedoraproject.org> - 2.5.4-3
-- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild
-
-* Tue Jan  2 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-2
-- Add a -doc subpackage
-- Fix end of line encodings
-- Fix permissions on yices_debug_version.c
-
-* Mon Jan  1 2018 Jerry James <loganjerry@gmail.com> - 2.5.4-1
-- Initial RPM
+%autochangelog