public inbox for git-commits@fedoraproject.org
help / color / mirror / Atom feed
* [rpms/cvc5] rawhide: Version 1.4.0
@ 2026-09-25 20:09 Jerry James
0 siblings, 0 replies; only message in thread
From: Jerry James @ 2026-09-25 20:09 UTC (permalink / raw)
To: git-commits
A new commit has been pushed.
Repo : rpms/cvc5
Branch : rawhide
Commit : 661ff190aa8d00592899050121286d740fe69c2d
Author : Jerry James <loganjerry@gmail.com>
Date : 2026-09-25T14:09:29-06:00
Stats : +50/-44 in 5 file(s)
URL : https://src.fedoraproject.org/rpms/cvc5/c/661ff190aa8d00592899050121286d740fe69c2d?branch=rawhide
Log:
Version 1.4.0
- Drop upstreamed cocoalib patch
- Disable the cadical option "inprobing" to fix tests
- Build with mpfr and normaliz support
---
diff --git a/cvc5-cadical.patch b/cvc5-cadical.patch
index e40b98a..75936fc 100644
--- a/cvc5-cadical.patch
+++ b/cvc5-cadical.patch
@@ -1,5 +1,5 @@
---- cvc5-cvc5-1.3.4/cmake/FindCaDiCaL.cmake.orig 2026-05-14 18:23:18.851442566 -0600
-+++ cvc5-cvc5-1.3.4/cmake/FindCaDiCaL.cmake 2026-05-14 18:24:09.896924282 -0600
+--- cvc5-cvc5-1.4.0/cmake/FindCaDiCaL.cmake.orig 2026-09-18 14:24:16.686749666 -0600
++++ cvc5-cvc5-1.4.0/cmake/FindCaDiCaL.cmake 2026-09-18 14:27:07.659997509 -0600
@@ -65,7 +65,7 @@ if(CaDiCaL_INCLUDE_DIR AND CaDiCaL_LIBRA
# Minimum supported version
set(CaDiCaL_FIND_VERSION "2.1.0")
@@ -9,9 +9,20 @@
# Set FOUND_SYSTEM to true; check_system_version will unset this if the
# version is less than the minimum required
---- cvc5-cvc5-1.3.4/src/prop/cadical/proof_tracer.cpp.orig 2026-05-07 09:27:40.000000000 -0600
-+++ cvc5-cvc5-1.3.4/src/prop/cadical/proof_tracer.cpp 2026-05-14 18:27:30.903325248 -0600
-@@ -48,7 +48,7 @@ ProofTracer::ProofTracer(const CadicalPr
+--- cvc5-cvc5-1.4.0/src/prop/cadical/cadical.cpp.orig 2026-09-17 15:10:12.000000000 -0600
++++ cvc5-cvc5-1.4.0/src/prop/cadical/cadical.cpp 2026-09-25 13:21:24.786405329 -0600
+@@ -101,7 +101,7 @@ void CadicalSolver::initialize()
+ d_solver->set("lucky", 0);
+ // ilb currently does not play well with user propagators
+ d_solver->set("ilb", 0);
+- d_solver->set("ilbassumptions", 0);
++ d_solver->set("inprobing", 0);
+ d_solver->connect_fixed_listener(d_propagator.get());
+ d_solver->connect_external_propagator(d_propagator.get());
+ }
+--- cvc5-cvc5-1.4.0/src/prop/cadical/proof_tracer.cpp.orig 2026-09-17 15:10:12.000000000 -0600
++++ cvc5-cvc5-1.4.0/src/prop/cadical/proof_tracer.cpp 2026-09-18 14:27:07.660311245 -0600
+@@ -99,7 +99,7 @@ ProofTracer::ProofTracer(const CadicalPr
{
}
@@ -20,7 +31,7 @@
CVC5_UNUSED bool redundant,
const std::vector<int>& clause,
CVC5_UNUSED bool restored)
-@@ -59,10 +59,11 @@ void ProofTracer::add_original_clause(ui
+@@ -110,10 +110,11 @@ void ProofTracer::add_original_clause(ui
Trace("cadical::prooftracer") << d_clauses.at(clause_id) << std::endl;
}
@@ -34,7 +45,7 @@
{
(void)redundant;
d_clauses.emplace(
-@@ -72,9 +73,9 @@ void ProofTracer::add_derived_clause(CVC
+@@ -123,9 +124,9 @@ void ProofTracer::add_derived_clause(CVC
}
void ProofTracer::add_assumption_clause(
@@ -46,7 +57,7 @@
{
// Assumption clauses are the negation of the core of failed/unsat
// assumptions.
-@@ -85,7 +86,7 @@ void ProofTracer::add_assumption_clause(
+@@ -136,7 +137,7 @@ void ProofTracer::add_assumption_clause(
}
void ProofTracer::conclude_unsat(CVC5_UNUSED CaDiCaL::ConclusionType type,
@@ -55,7 +66,7 @@
{
// Store final clause ids that concluded unsat.
d_final_clauses = clause_ids;
-@@ -93,13 +94,13 @@ void ProofTracer::conclude_unsat(CVC5_UN
+@@ -144,13 +145,13 @@ void ProofTracer::conclude_unsat(CVC5_UN
void ProofTracer::compute_proof_core(std::vector<uint64_t>& core) const
{
@@ -72,7 +83,7 @@
visit.pop_back();
if (visited.insert(clause_id).second)
-@@ -137,7 +138,7 @@ std::shared_ptr<ProofNode> ProofTracer::
+@@ -188,7 +189,7 @@ std::shared_ptr<ProofNode> ProofTracer::
}
std::unordered_map<uint64_t, std::shared_ptr<ProofNode>> steps;
@@ -81,8 +92,8 @@
{
const auto& clause = d_clauses.at(cid);
if (clause.type == ClauseType::DERIVED)
---- cvc5-cvc5-1.3.4/src/prop/cadical/proof_tracer.h.orig 2026-05-07 09:27:40.000000000 -0600
-+++ cvc5-cvc5-1.3.4/src/prop/cadical/proof_tracer.h 2026-05-14 20:43:28.201176941 -0600
+--- cvc5-cvc5-1.4.0/src/prop/cadical/proof_tracer.h.orig 2026-09-17 15:10:12.000000000 -0600
++++ cvc5-cvc5-1.4.0/src/prop/cadical/proof_tracer.h 2026-09-18 14:27:07.660551513 -0600
@@ -56,38 +56,39 @@ class ProofTracer : public CaDiCaL::Trac
struct ClauseInfo
{
diff --git a/cvc5-cocoalib.patch b/cvc5-cocoalib.patch
deleted file mode 100644
index 7c0a892..0000000
--- a/cvc5-cocoalib.patch
+++ /dev/null
@@ -1,10 +0,0 @@
---- cvc5-cvc5-1.1.2/src/theory/ff/uni_roots.cpp.orig 2024-03-01 10:21:00.000000000 -0700
-+++ cvc5-cvc5-1.1.2/src/theory/ff/uni_roots.cpp 2024-03-29 10:15:03.668891240 -0600
-@@ -29,7 +29,6 @@
- #include <CoCoA/RingZZ.H>
- #include <CoCoA/SmallFpImpl.H>
- #include <CoCoA/SparsePolyOps-RingElem.H>
--#include <CoCoA/SparsePolyOps-vector.H>
- #include <CoCoA/factor.H>
- #include <CoCoA/factorization.H>
- #include <CoCoA/random.H>
diff --git a/cvc5-skip-himem-tests.patch b/cvc5-skip-himem-tests.patch
index c50f4f9..9aa878b 100644
--- a/cvc5-skip-himem-tests.patch
+++ b/cvc5-skip-himem-tests.patch
@@ -1,6 +1,6 @@
---- cvc5-cvc5-1.3.1/test/api/cpp/issues/CMakeLists.txt.orig 2025-09-24 08:43:04.000000000 -0600
-+++ cvc5-cvc5-1.3.1/test/api/cpp/issues/CMakeLists.txt 2025-09-25 08:34:20.392502538 -0600
-@@ -49,8 +49,8 @@ cvc5_add_api_test(proj-issue666 "issues"
+--- cvc5-cvc5-1.4.0/test/api/cpp/issues/CMakeLists.txt.orig 2026-09-17 15:10:12.000000000 -0600
++++ cvc5-cvc5-1.4.0/test/api/cpp/issues/CMakeLists.txt 2026-09-18 14:24:28.854136171 -0600
+@@ -46,8 +46,8 @@ cvc5_add_api_test(proj-issue666 "issues"
if (NOT ENABLE_SAFE_MODE AND NOT ENABLE_STABLE_MODE)
cvc5_add_api_test(issue4889 "issues")
@@ -11,9 +11,9 @@
cvc5_add_api_test(proj-issue377 "issues")
cvc5_add_api_test(proj-issue388 "issues")
cvc5_add_api_test(proj-issue413 "issues")
---- cvc5-cvc5-1.3.1/test/regress/cli/CMakeLists.txt.orig 2025-09-24 08:43:04.000000000 -0600
-+++ cvc5-cvc5-1.3.1/test/regress/cli/CMakeLists.txt 2025-09-25 08:34:20.392970530 -0600
-@@ -4028,8 +4028,8 @@ set(regress_3_tests
+--- cvc5-cvc5-1.4.0/test/regress/cli/CMakeLists.txt.orig 2026-09-17 15:10:12.000000000 -0600
++++ cvc5-cvc5-1.4.0/test/regress/cli/CMakeLists.txt 2026-09-18 14:25:13.010075217 -0600
+@@ -4304,8 +4304,8 @@ set(regress_3_tests
regress3/arith/abz5_1400.smtv1.smt2
regress3/arith_prp-13-24.smt2
regress3/auflia-fuzz06.smtv1.smt2
@@ -24,7 +24,7 @@
regress3/bmc-ibm-2.smtv1.smt2
regress3/bmc-ibm-5.smtv1.smt2
regress3/bmc-ibm-7.smtv1.smt2
-@@ -4044,7 +4044,7 @@ set(regress_3_tests
+@@ -4320,7 +4320,7 @@ set(regress_3_tests
regress3/bv-core-ext_con_004_001_1024.smtv1.smt2
regress3/bv-fuzz15.smtv1.smt2
regress3/bv-fuzz16.smtv1.smt2
@@ -33,7 +33,7 @@
regress3/cegisunif-depth1.sy
regress3/decision-uflia-xs-09-16-3-4-1-5.smtv1.smt2
regress3/DRAGON_1.lus.sy
-@@ -4057,7 +4057,7 @@ set(regress_3_tests
+@@ -4333,7 +4333,7 @@ set(regress_3_tests
regress3/interpol2.smt2
regress3/inv_gen_n_c11.sy
regress3/issue11616.smt2
@@ -42,7 +42,7 @@
regress3/issue4707-bv-to-bool-large.smt2
regress3/lpsat-goal-9.smt2
regress3/nia-max-square.sy
-@@ -4070,7 +4070,7 @@ set(regress_3_tests
+@@ -4346,7 +4346,7 @@ set(regress_3_tests
regress3/qwh.35.405.shuffled-as.sat03-1651.smtv1.smt2
regress3/sixfuncs.sy
regress3/specsharp-WindowsCard.15.RTE.Terminate_System.Int32.smt2
@@ -51,10 +51,10 @@
regress3/strings/extf_d_perf.smt2
regress3/strings/issue8926-sygus-inst.smt2
regress3/strings/norn-dis-0707-3.smt2
-@@ -4083,9 +4083,9 @@ set(regress_3_tests
-
+@@ -4360,9 +4360,9 @@ set(regress_3_tests
set(regress_4_tests
regress4/bug143.smtv1.smt2
+ regress4/bv/abstract/abv-klee-select-index.smt2
- regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
+ #regress4/C880mul.miter.shuffled-as.sat03-348.smtv1.smt2
regress4/fischer3-mutex-16.smtv1.smt2
diff --git a/cvc5.spec b/cvc5.spec
index 190b2ad..15583b7 100644
--- a/cvc5.spec
+++ b/cvc5.spec
@@ -7,12 +7,12 @@
# The cvc5_pythonic_api project needs cvc5 to build, and cvc5 needs
# cvc5_pythonic_api to build. See cmake/FindCVC5PythonicAPI.cmake for the git
# commit needed by this version of cvc5.
-%global pcommit cdcac7cb2da79d922fc44628c1c3c5f60c2eeec4
+%global pcommit a0d6c75bca0dca4a26c0d570e7b969272c9a7de1
%global giturl https://github.com/cvc5/cvc5
Name: cvc5
-Version: 1.3.4
+Version: 1.4.0
Release: %autorelease
Summary: Automatic theorem prover for SMT problems
@@ -29,15 +29,12 @@ Patch: %{name}-flags.patch
# Skip tests that require huge amounts of memory
# Patch courtesy of Scott Talbert
Patch: %{name}-skip-himem-tests.patch
-# Adapt to cocoalib 0.99850
-Patch: %{name}-cocoalib.patch
# Adapt to cadical 2.2.0
Patch: %{name}-cadical.patch
# See https://fedoraproject.org/wiki/Changes/EncourageI686LeafRemoval
ExcludeArch: %{ix86}
BuildSystem: cmake
-BuildOption(conf): --debug-find
BuildOption(conf): -DBUILD_BINDINGS_JAVA:BOOL=ON
BuildOption(conf): -DBUILD_BINDINGS_PYTHON:BOOL=ON
BuildOption(conf): -DBUILD_DOCS:BOOL=OFF
@@ -51,6 +48,8 @@ BuildOption(conf): -DUSE_CRYPTOMINISAT:BOOL=ON
BuildOption(conf): -DUSE_DEFAULT_LINKER:BOOL=ON
BuildOption(conf): -DUSE_EDITLINE:BOOL=ON
BuildOption(conf): -DUSE_KISSAT:BOOL=ON
+BuildOption(conf): -DUSE_MPFR:BOOL=ON
+BuildOption(conf): -DUSE_NORMALIZ:BOOL=ON
BuildOption(conf): -DUSE_POLY:BOOL=ON
BuildRequires: cadical-devel
@@ -62,9 +61,11 @@ BuildRequires: git-core
BuildRequires: java-25-devel
BuildRequires: javapackages-tools
BuildRequires: kissat-devel
+BuildRequires: libnormaliz-devel
BuildRequires: libpoly-devel
BuildRequires: pkgconfig(gmp)
BuildRequires: pkgconfig(libedit)
+BuildRequires: pkgconfig(mpfr)
BuildRequires: pkgconfig(sqlite3)
BuildRequires: procps-ng
BuildRequires: pyproject-rpm-macros
@@ -80,7 +81,6 @@ BuildRequires: symfpu-devel
# Needed for some of the tests; we do not currently execute those tests
#BuildRequires: ethos
-#BuildRequires: lfsc-devel
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
@@ -104,8 +104,6 @@ performance and reduce the memory overhead of its predecessors.
%package devel
Summary: Headers and other files for developing with %{name}
Requires: %{name}-libs%{?_isa} = %{version}-%{release}
-Requires: gmp-devel%{?_isa}
-Requires: symfpu-devel
%description devel
Header files and library links for developing applications that use %{name}.
@@ -148,7 +146,14 @@ sed -e 's,\(--ethos-binary \).*,\1%{_bindir}/ethos,' \
-i test/regress/cli/CMakeLists.txt
# Without this, the python interface has version 0.0.0
-sed -i 's/CVC5_WHEEL_VERSION/CVC5_VERSION/' src/api/python/__init__.py.in
+#sed -i 's/CVC5_WHEEL_VERSION/CVC5_VERSION/' src/api/python/__init__.py.in
+
+# Upstream avoids this flag for build time reasons; we want it
+sed -i '/-fno-var-tracking-assignments/d' src/CMakeLists.txt
+
+# Our build of the cvc5 binary includes one reference to a cocoalib symbol
+sed -i '/USE_EDITLINE/itarget_link_libraries(cvc5-bin PUBLIC -lcocoa)' \
+ src/main/CMakeLists.txt
%conf -p
export BUILDFLAGS='-DABC_USE_STDINT_H -I%{_jvmdir}/java/include -I%{_jvmdir}/java/include/linux -I%{_includedir}/abc -I%{_includedir}/cryptominisat5'
diff --git a/sources b/sources
index 22b34b9..79acb9a 100644
--- a/sources
+++ b/sources
@@ -1,2 +1,2 @@
-SHA512 (cvc5-1.3.4.tar.gz) = 6e65593e9493dd2db1acc38cdf38fe3285a9ca966ded7f4ecb349927e6fce17b6d4f6cb7f9d950ab5f48f50eb59f4f7a995b74f9d244455f5f460ac66e1a6dd9
-SHA512 (cdcac7cb2da79d922fc44628c1c3c5f60c2eeec4.zip) = d1e98917c330a58ed09c8f16fbcf1eb478dc8cb05c9b08b8a7e4415810341de0e575d047f7772c645d4d408b1f904be9ecca647798c74827540cb1b9c8da42da
+SHA512 (cvc5-1.4.0.tar.gz) = ee9578878c7e541f82a5f6c9535cd4ba764fb6d5dcdc0bf69e50cd360b2b56bc66adca1f6babd5971c5175818b3e716cb7b411488adcbf207e21ac59d0fd6d84
+SHA512 (a0d6c75bca0dca4a26c0d570e7b969272c9a7de1.zip) = c1432b74b41b4a644cc2675cc0040878dc40963f9e78c4540fb39cd4163d8eaed6938ecf664dc3aff652dbee06e88295d6a77c0403736a77a3a9d6c6d893be09
^ permalink raw reply related [flat|nested] only message in thread
only message in thread, other threads:[~2026-09-25 20:09 UTC | newest]
Thread overview: (only message) (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2026-09-25 20:09 [rpms/cvc5] rawhide: Version 1.4.0 Jerry James
This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox