- updated to 4.12.2 (new soname)

diff --git a/z3-sse.patch b/z3-sse.patch
new file mode 100644 (file)
index 0000000..c3b53c2
--- /dev/null
+++ b/z3-sse.patch
@@ -0,0 +1,24 @@
+--- z3-z3-4.12.2/src/util/hwf.cpp.orig 2023-05-12 21:59:04.000000000 +0200
++++ z3-z3-4.12.2/src/util/hwf.cpp      2023-11-06 19:03:19.396855936 +0100
+@@ -33,7 +33,9 @@ Revision History:
+ 
+ #if defined(__x86_64__) || defined(_M_X64) ||    \
+     defined(__i386) || defined(_M_IX86)
++#  ifdef __SSE2__
+ #define USE_INTRINSICS
++#  endif
+ #endif
+ 
+ #include "util/hwf.h"
+--- z3-z3-4.12.2/CMakeLists.txt.orig   2023-11-06 19:03:42.240065517 +0100
++++ z3-z3-4.12.2/CMakeLists.txt        2023-11-06 19:16:21.029288136 +0100
+@@ -250,7 +250,8 @@ endif()
+ # FP math
+ ################################################################################
+ # FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard"
+-if ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686"))
++option(USE_SSE2 ON)
++if (USE_SSE2 AND ((TARGET_ARCHITECTURE STREQUAL "x86_64") OR (TARGET_ARCHITECTURE STREQUAL "i686")))
+   if ((CMAKE_CXX_COMPILER_ID MATCHES "GNU") OR (CMAKE_CXX_COMPILER_ID MATCHES "Clang") OR (CMAKE_CXX_COMPILER_ID MATCHES "Intel"))
+     set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2")
+   elseif (CMAKE_CXX_COMPILER_ID STREQUAL "MSVC")

diff --git a/z3.spec b/z3.spec
index 2c4d46ca29a90bef74b8e9ae764487df02e5187d..4d5d05dfaaf5990f69041cad9864dd0e2d43459b 100644 (file)
--- a/z3.spec
+++ b/z3.spec
@@ -4,23 +4,28 @@
 %bcond_with    dotnet          # .NET API (requires MS .NET SDK + mono)
 %bcond_without ocaml           # OCaml API
 %bcond_without ocaml_opt       # skip building native optimized binaries (bytecode is always built)
+%bcond_with    sse2            # SSE2 instructions
 
 # not yet available on x32 (ocaml 4.02.1), update when upstream will support it
 %ifnarch %{ix86} %{x8664} %{arm} aarch64 ppc sparc sparcv9
 %undefine      with_ocaml_opt
 %endif
+%ifarch %{x8664} x32 pentium4
+%define                with_sse2       1
+%endif
 
 Summary:       High-performance theorem prover developed at Microsoft Research
 Summary(pl.UTF-8):     Wydajne narzędzie do dowodzenia twierdzeń tworzone przez Microsoft Research
 Name:          z3
-Version:       4.8.17
+Version:       4.12.2
 Release:       1
 License:       MIT
 Group:         Applications/Engineering
 #Source0Download: https://github.com/Z3Prover/z3/releases
 Source0:       https://github.com/Z3Prover/z3/archive/z3-%{version}.tar.gz
-# Source0-md5: b0c2c37321f21ae9504a8fc112edd878
+# Source0-md5: 4061317f7948c19abd13041c5a32b057
 Patch0:                %{name}-pld.patch
+Patch1:                %{name}-sse.patch
 URL:           https://github.com/Z3Prover/z3
 BuildRequires: cmake >= 3.4
 %{?with_apidocs:BuildRequires: doxygen}
@@ -127,6 +132,12 @@ API języka Python do biblioteki dowodzenia twierdzeń Z3.
 %prep
 %setup -q -n z3-z3-%{version}
 %patch0 -p1
+%patch1 -p1
+
+%if %{without sse2}
+# no cmake option to disable, just architecture+compiler check
+%{__sed} -i -e 's/if (HAS_SSE2)/if (FALSE)/' CMakeLists.txt
+%endif
 
 %build
 %if %{with ocaml}
@@ -175,6 +186,7 @@ cd build-cmake
        %{?with_dotnet:-DZ3_INSTALL_DOTNET_BINDINGS=ON} \
        -DZ3_INSTALL_JAVA_BINDINGS=ON \
        -DZ3_INSTALL_PYTHON_BINDINGS=ON \
+       %{!?with_sse2:-DUSE_SSE2=OFF} \
        -DZ3_USE_LIB_GMP=ON
 
 %{__make}
@@ -245,9 +257,9 @@ rm -rf $RPM_BUILD_ROOT
 
 %files
 %defattr(644,root,root,755)
-%doc LICENSE.txt README.md RELEASE_NOTES
+%doc LICENSE.txt README.md RELEASE_NOTES.md
 %attr(755,root,root) %{_libdir}/libz3.so.*.*.*.*
-%ghost %attr(755,root,root) %{_libdir}/libz3.so.4.8
+%ghost %attr(755,root,root) %{_libdir}/libz3.so.4.12
 %attr(755,root,root) %{_bindir}/z3
 
 %files devel