diff --git a/.gitignore b/.gitignore index 1c8e76a..9ffab0f 100644 --- a/.gitignore +++ b/.gitignore @@ -1,3 +1 @@ /Yices-*.tar.gz -/yices-*.tar.gz -/cudd-*.tar.gz diff --git a/README.md b/README.md deleted file mode 100644 index df2e238..0000000 --- a/README.md +++ /dev/null @@ -1,11 +0,0 @@ -# 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. diff --git a/changelog b/changelog deleted file mode 100644 index 826b5cd..0000000 --- a/changelog +++ /dev/null @@ -1,109 +0,0 @@ -* Tue Feb 20 2024 Jerry James - 2.6.4-12 -- Fix the SPDX expression - -* Fri Feb 9 2024 Jerry James - 2.6.4-11 -- Rebuild for cryptominisat 5.11.21 - -* Wed Jan 31 2024 Jerry James - 2.6.4-10 -- Rebuild for cryptominisat 5.11.15 - -* Sat Jan 27 2024 Fedora Release Engineering - 2.6.4-9 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_40_Mass_Rebuild - -* Wed Jan 10 2024 Jerry James - 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 - 2.6.4-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_39_Mass_Rebuild - -* Sat Jan 21 2023 Fedora Release Engineering - 2.6.4-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_38_Mass_Rebuild - -* Mon Nov 28 2022 Jerry James - 2.6.4-5 -- Regenerate the cudd configure script to fix FTBFS -- Convert License tag to SPDX - -* Mon Nov 28 2022 Timm Bäder - 2.6.4-5 -- Get rid of an implicit int function declaration in a configure check - -* Sat Jul 23 2022 Fedora Release Engineering - 2.6.4-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_37_Mass_Rebuild - -* Sat Jan 22 2022 Fedora Release Engineering - 2.6.4-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_36_Mass_Rebuild - -* Tue Jan 11 2022 Jerry James - 2.6.4-2 -- Build with kissat support - -* Mon Oct 25 2021 Jerry James - 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 - 2.6.2-8 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_35_Mass_Rebuild - -* Thu Jan 28 2021 Fedora Release Engineering - 2.6.2-7 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_34_Mass_Rebuild - -* Fri Nov 27 2020 Jerry James - 2.6.2-6 -- Rebuild for cryptominisat 5.8.0 - -* Mon Aug 3 2020 Jerry James - 2.6.2-5 -- Rebuild for cadical 1.3.0 - -* Wed Jul 29 2020 Fedora Release Engineering - 2.6.2-4 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_33_Mass_Rebuild - -* Sat Apr 25 2020 Jerry James - 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 - 2.6.2-2 -- Use native sphinx 3 support for enum instead of cenum extension (bz 1823515) - -* Thu Mar 26 2020 Jerry James - 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 - 2.6.1-6 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_32_Mass_Rebuild - -* Thu Jan 23 2020 Jerry James - 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 - 2.6.1-4 -- Add -fwrapv to build flags; thanks to Jeff Law for the diagnosis - -* Sat Jul 27 2019 Fedora Release Engineering - 2.6.1-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_31_Mass_Rebuild - -* Sun Feb 03 2019 Fedora Release Engineering - 2.6.1-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_30_Mass_Rebuild - -* Tue Oct 30 2018 Jerry James - 2.6.1-1 -- New upstream version - -* Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild - -* Wed Jul 4 2018 Jerry James - 2.6.0-1 -- New upstream version - -* Fri Feb 09 2018 Fedora Release Engineering - 2.5.4-3 -- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild - -* Tue Jan 2 2018 Jerry James - 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 - 2.5.4-1 -- Initial RPM diff --git a/implicit-int.patch b/implicit-int.patch deleted file mode 100644 index 579b87e..0000000 --- a/implicit-int.patch +++ /dev/null @@ -1,12 +0,0 @@ -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 --main(void) -+int main(void) - { - if (HUGE_VAL != HUGE_VAL * 3 || HUGE_VAL != HUGE_VAL / 3) return 1; - return 0; diff --git a/sources b/sources index 5aa08fc..cc68492 100644 --- a/sources +++ b/sources @@ -1,2 +1 @@ -SHA512 (yices-2.7.0.tar.gz) = 0ed9811bfc505793078aa87afd86177a79bb5b9a4ec579fa0c43076cc997ff432d66588e996c1303d91bfb2163110312f30f1fc75a4d2f60d5786499bdd26b92 -SHA512 (cudd-3.0.0.tar.gz) = a26728fedc3033ae2a842000f43f215b4abc914cd00fe0097fd483e59dc630568bfa6a115baa93af94b2f70f3d538761a12143fdb757167e90395c9fd244318c +SHA512 (Yices-2.6.1.tar.gz) = 586f24a8e3da45726ee69f4b3a744f2c04c3b400304319c00667c81c6799a846906ed580a9c4dd0df87a23ddb8e4fefb0b8ab60c13c19dc29243ba116717d1f2 diff --git a/yices-cryptominisat.patch b/yices-cryptominisat.patch deleted file mode 100644 index 78d4a74..0000000 --- a/yices-cryptominisat.patch +++ /dev/null @@ -1,114 +0,0 @@ ---- a/src/solvers/cdcl/delegate.c -+++ b/src/solvers/cdcl/delegate.c -@@ -21,11 +21,11 @@ - #include - - #ifdef HAVE_CADICAL --#include "ccadical.h" -+#include - #endif - - #ifdef HAVE_CRYPTOMINISAT --#include "cryptominisat5/cmsat_c.h" -+#include - #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; diff --git a/yices.spec b/yices.spec index 7b990a7..a139512 100644 --- a/yices.spec +++ b/yices.spec @@ -1,66 +1,29 @@ -%global giturl https://github.com/SRI-CSL/yices2 - Name: yices -Version: 2.7.0 -Release: %autorelease +Version: 2.6.1 +Release: 1%{?dist} Summary: SMT solver -# 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 +License: GPLv3+ URL: http://yices.csl.sri.com/ -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 +Source0: https://github.com/SRI-CSL/yices2/archive/Yices-%{version}.tar.gz -# 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: 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 +BuildRequires: tex(latex) %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. @@ -70,8 +33,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 @@ -81,60 +44,19 @@ 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 -%autosetup -n yices2-yices-%{version} -a 1 -p1 +%setup -q -n yices2-Yices-%{version} -%conf # Do not try to avoid -fstack-protector -sed -i 's/@NO_STACK_PROTECTOR@//' make.include.in +sed -i '/NO_STACK_PROTECTOR=""/,/AC_SUBST(NO_STACK_PROTECTOR)/d' configure.ac -# 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 +# Generate the configure script 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 @@ -143,29 +65,17 @@ 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 - -guess=$(./config.guess) -if [ "%{_host}" != "$guess" ]; then - mv configs/make.include.%{_host} configs/make.include.${guess} -fi -%make_build MODE=debug +mv configs/make.include.%{_host} configs/make.include.$(./config.guess) +make %{?_smp_mflags} MODE=debug # Build the manual -make doc - -# Build the interface documentation -make -C doc/sphinx html -rm doc/sphinx/build/html/.buildinfo +pushd doc/manual +pdflatex manual +bibtex manual +pdflatex manual +pdflatex manual +popd %install make install prefix=%{buildroot}%{_prefix} exec_prefix=%{buildroot}%{_prefix} \ @@ -179,27 +89,42 @@ cp -p doc/*.1 %{buildroot}%{_mandir}/man1 make check MODE=debug %files -%doc doc/SMT-LIB-LANGUAGE doc/YICES-LANGUAGE -%license copyright.txt LICENSE.txt -%{_libdir}/libyices.so.2.7{,.*} +%doc doc/YICES-LANGUAGE +%license LICENSE.txt +%{_libdir}/*.so.* %files devel %{_includedir}/%{name}/ -%{_libdir}/libyices.so +%{_libdir}/*.so %files tools %{_bindir}/yices %{_bindir}/yices-sat %{_bindir}/yices-smt %{_bindir}/yices-smt2 -%{_mandir}/man1/yices.1* -%{_mandir}/man1/yices-sat.1* -%{_mandir}/man1/yices-smt.1* -%{_mandir}/man1/yices-smt2.1* +%{_mandir}/man1/* %files doc -%doc doc/manual/manual.pdf doc/sphinx/build/html examples -%license copyright.txt LICENSE.txt +%doc doc/manual/manual.pdf examples +%license LICENSE.txt %changelog -%autochangelog +* Tue Oct 30 2018 Jerry James - 2.6.1-1 +- New upstream version + +* Sat Jul 14 2018 Fedora Release Engineering - 2.6.0-2 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_29_Mass_Rebuild + +* Wed Jul 4 2018 Jerry James - 2.6.0-1 +- New upstream version + +* Fri Feb 09 2018 Fedora Release Engineering - 2.5.4-3 +- Rebuilt for https://fedoraproject.org/wiki/Fedora_28_Mass_Rebuild + +* Tue Jan 2 2018 Jerry James - 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 - 2.5.4-1 +- Initial RPM