[packages/z3] - updated to 4.12.2 (new soname)

[qboosh]

commit 4567459447eb1f6528a1f6008ef3495cdc50f843
Author: Jakub Bogusz <qboosh at pld-linux.org>
Date:   Fri Nov 10 20:22:55 2023 +0100

    - updated to 4.12.2 (new soname)

 z3-sse.patch | 24 ++++++++++++++++++++++++
 z3.spec      | 20 ++++++++++++++++----
 2 files changed, 40 insertions(+), 4 deletions(-)
---
diff --git a/z3.spec b/z3.spec
index 2c4d46c..4d5d05d 100644
--- 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
diff --git a/z3-sse.patch b/z3-sse.patch
new file mode 100644
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")
================================================================

---- gitweb:

http://git.pld-linux.org/gitweb.cgi/packages/z3.git/commitdiff/4567459447eb1f6528a1f6008ef3495cdc50f843