tribes/guix
1
0
Fork 1
mirror of https://git.savannah.gnu.org/git/guix.git synced 2026-05-09 02:35:54 +02:00
Code Activity

gnu: cvc5: Restore compatibility with packaged symfpu.

Browse Source 
* packages/patches/cvc5-symfpu-compatibility.patch: New patch.
* gnu/local.mk (dist_patch_DATA) Register it.
* gnu/packages/maths.scm (cvc5)[patches]: Use it.

Change-Id: Ie8b9b24efed45365a1e974396d6e3d9c5367bf1e
This commit is contained in:
Sören Tempel
2026-04-20 18:23:36 +02:00
parent fbd6b6ff8c
commit 88e2e42aa2
3 changed files with 168 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
gnu/local.mk
+1
View File
@@ -1178,6 +1178,7 @@ dist_patch_DATA = \
%D%/packages/patches/curlftpfs-fix-no_verify_hostname.patch \
%D%/packages/patches/cursynth-wave-rand.patch \
%D%/packages/patches/cvc5-reproducible-build.patch \
%D%/packages/patches/cvc5-symfpu-compatibility.patch \
%D%/packages/patches/cvs-CVE-2017-12836.patch \
%D%/packages/patches/cyrus-sasl-fix-time-h.patch \
%D%/packages/patches/d-feet-drop-unused-meson-argument.patch \
gnu/packages/maths.scm
+2 -1
View File
@@ -458,7 +458,8 @@ programming languages.")
(url "https://github.com/cvc5/cvc5/")
(commit (string-append "cvc5-" version))))
(file-name (git-file-name name version))
(patches (search-patches "cvc5-reproducible-build.patch"))
(patches (search-patches "cvc5-reproducible-build.patch"
"cvc5-symfpu-compatibility.patch"))
(sha256
(base32 "0ynz7di4dyyiiydgmf0z9dc2jl7nm44xi0amch29rcgznwr4wy5m"))))
(build-system cmake-build-system)
gnu/packages/patches/cvc5-symfpu-compatibility.patch
+165
View File
@@ -0,0 +1,165 @@
Ensures that cvc5 is compatible with our version of SymFPU.
Taken from: https://github.com/cvc5/cvc5/commit/2ed457049cf52bd0f21a6332c1be487d82bf5678
diff --git a/cmake/FindSymFPU.cmake b/cmake/FindSymFPU.cmake
index 765ee8d36..05a86e9ee 100644
--- a/cmake/FindSymFPU.cmake
+++ b/cmake/FindSymFPU.cmake
@@ -29,8 +29,8 @@ if(NOT SymFPU_FOUND_SYSTEM)
include(ExternalProject)
include(deps-helper)
- set(SymFPU_COMMIT "e6ac3af9c2c574498ea171c957425b407625448b")
- set(SymFPU_CHECKSUM "823aa663fcc2f6844ae5e9ea83ceda4ed393cdb3dadefce9b3c7c41cd0f4f702")
+ set(SymFPU_COMMIT "227a7246b8ce513b393cc2645d6d65d3490ea1de")
+ set(SymFPU_CHECKSUM "ff22e37dbc133120ada5760878974811737bec65b12a8883f92b1ed9e3f96e99")
ExternalProject_Add(
SymFPU-EP
diff --git a/src/theory/fp/fp_word_blaster.cpp b/src/theory/fp/fp_word_blaster.cpp
index 7f2086c35..3efb0eeed 100644
--- a/src/theory/fp/fp_word_blaster.cpp
+++ b/src/theory/fp/fp_word_blaster.cpp
@@ -119,6 +119,23 @@ CVC5_SYM_ITE_DFN(traits::ubv);
#undef CVC5_SYM_ITE_DFN
+#define CVC5_SYM_ITE_BOOL_DFN(T) \
+ template <> \
+ struct ite<bool, T> \
+ { \
+ static const T iteOp(const bool& cond, const T& l, const T& r) \
+ { \
+ return cond ? l : r; \
+ } \
+ }
+
+CVC5_SYM_ITE_BOOL_DFN(traits::rm);
+CVC5_SYM_ITE_BOOL_DFN(traits::prop);
+CVC5_SYM_ITE_BOOL_DFN(traits::sbv);
+CVC5_SYM_ITE_BOOL_DFN(traits::ubv);
+
+#undef CVC5_SYM_ITE_BOOL_DFN
+
template <>
traits::ubv orderEncode<traits, traits::ubv>(const traits::ubv& b)
{
@@ -564,6 +581,13 @@ symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularAdd(
return *this + op;
}
+template <bool isSigned>
+symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularSubtract(
+ const symbolicBitVector<isSigned>& op) const
+{
+ return *this - op;
+}
+
template <bool isSigned>
symbolicBitVector<isSigned> symbolicBitVector<isSigned>::modularNegate() const
{
diff --git a/src/theory/fp/fp_word_blaster.h b/src/theory/fp/fp_word_blaster.h
index 6ce365382..8179ceb32 100644
--- a/src/theory/fp/fp_word_blaster.h
+++ b/src/theory/fp/fp_word_blaster.h
@@ -242,6 +242,8 @@ class symbolicBitVector : public nodeWrapper
symbolicBitVector<isSigned> modularDecrement() const;
symbolicBitVector<isSigned> modularAdd(
const symbolicBitVector<isSigned>& op) const;
+ symbolicBitVector<isSigned> modularSubtract(
+ const symbolicBitVector<isSigned>& op) const;
symbolicBitVector<isSigned> modularNegate() const;
/*** Comparisons ***/
diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp
index af56c2b87..181069427 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.cpp
+++ b/src/util/floatingpoint_literal_symfpu_traits.cpp
@@ -223,6 +223,13 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularAdd(
return *this + op;
}
+template <bool isSigned>
+wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularSubtract(
+ const wrappedBitVector<isSigned>& op) const
+{
+ return *this - op;
+}
+
template <bool isSigned>
wrappedBitVector<isSigned> wrappedBitVector<isSigned>::modularNegate() const
{
diff --git a/src/util/floatingpoint_literal_symfpu_traits.h b/src/util/floatingpoint_literal_symfpu_traits.h
index 78fc69a18..b49ef3a2a 100644
--- a/src/util/floatingpoint_literal_symfpu_traits.h
+++ b/src/util/floatingpoint_literal_symfpu_traits.h
@@ -199,6 +199,8 @@ class wrappedBitVector : public BitVector
wrappedBitVector<isSigned> modularDecrement() const;
wrappedBitVector<isSigned> modularAdd(
const wrappedBitVector<isSigned>& op) const;
+ wrappedBitVector<isSigned> modularSubtract(
+ const wrappedBitVector<isSigned>& op) const;
wrappedBitVector<isSigned> modularNegate() const;
/** Bit-vector equality. */
diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index 915a19e09..35ff58bc7 100644
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -949,12 +949,15 @@ set(regress_0_tests
regress0/fp/issue6164.smt2
regress0/fp/issue7002.smt2
regress0/fp/issue7569.smt2
+ regress0/fp/issue9505.smt2
regress0/fp/issue9854.smt2
regress0/fp/issue9858.smt2
regress0/fp/issue9864.smt2
regress0/fp/issue9966.smt2
regress0/fp/issue9972.smt2
regress0/fp/issue9972-2.smt2
+ regress0/fp/issue11139.smt2
+ regress0/fp/issue12335.smt2
regress0/fp/issuepr650.smt2
regress0/fp/proj-issue329-prereg-context.smt2
regress0/fp/proj-issue477-fp-set-comprehension.smt2
diff --git a/test/regress/cli/regress0/fp/issue11139.smt2 b/test/regress/cli/regress0/fp/issue11139.smt2
new file mode 100644
index 000000000..f4c00360e
--- /dev/null
+++ b/test/regress/cli/regress0/fp/issue11139.smt2
@@ -0,0 +1,9 @@
+; COMMAND-LINE: --check-models
+; EXPECT: sat
+(set-logic QF_FP)
+(declare-const FP_VAR_a (_ FloatingPoint 11 53))
+(declare-const FP_VAR_b (_ FloatingPoint 11 53))
+(assert ( = (fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)
+(fp.div RTN (fp.fma RTP FP_VAR_a FP_VAR_a
+(fp #b0 #b00000000000 #b0000000000000000000000000000000000000000000000000000)) FP_VAR_b)))
+(check-sat)
diff --git a/test/regress/cli/regress0/fp/issue12335.smt2 b/test/regress/cli/regress0/fp/issue12335.smt2
new file mode 100644
index 000000000..bc2580a89
--- /dev/null
+++ b/test/regress/cli/regress0/fp/issue12335.smt2
@@ -0,0 +1,7 @@
+; EXPECT: sat
+(set-logic FP)
+(declare-const x Float32)
+(declare-const a Float32)
+(assert (forall ((V Float32) (A Float32)) (or (not (fp.lt V x)) (not (fp.eq a a)) (not (fp.gt A (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))) (not (fp.eq (fp.div RNE A V) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)))))))
+(assert (fp.geq a (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))
+(check-sat)
diff --git a/test/regress/cli/regress0/fp/issue9505.smt2 b/test/regress/cli/regress0/fp/issue9505.smt2
new file mode 100644
index 000000000..05674b8ff
--- /dev/null
+++ b/test/regress/cli/regress0/fp/issue9505.smt2
@@ -0,0 +1,6 @@
+; COMMAND-LINE: --fp-exp
+; EXPECT: sat
+(set-logic QF_FP)
+(declare-fun m () (_ FloatingPoint 4 12))
+(assert (fp.eq (fp (_ bv0 1) (_ bv0 8) (_ bv0 23)) ((_ to_fp 8 24) roundNearestTiesToEven (fp.rem m (fp (_ bv0 1) (_ bv9 4) (_ bv1536 11))))))
+(check-sat)