Download raw body.
[update] math/z3: update to 4.13.0
On Sat, 31 Aug 2024 21:08:15 +0200,
Klemens Nanni <kn@openbsd.org> wrote:
>
> You're right, :Q remained from an earlier iteration.
> I dropped it, yielding correct commands now, thanks.
>
Here an updated diff where I've backported patch from upstream which fixed
crash on OpenBSD as side effect.
I also drop testing of crash because
- '(declare-datatype)' and '(declare-datatype a)' doesn't work on 4.13 and
simple complains as:
(error "line 1 column 18: unexpected token used as datatype name")
(error "line 1 column 20: invalid datatype declaration, '(' expected got a")
- '(declare-const p Bool) because this case is covered by example models.
So, finally a diff which works without crash on -current/amd64:
Index: Makefile
===================================================================
RCS file: /cvs/ports/math/z3/Makefile,v
retrieving revision 1.33
diff -u -p -r1.33 Makefile
--- Makefile 6 May 2024 12:23:45 -0000 1.33
+++ Makefile 3 Sep 2024 16:05:14 -0000
@@ -1,16 +1,9 @@
COMMENT = Z3 theorem prover
-VERSION = 4.12.2
-REVISION = 1
+DIST_TUPLE = github Z3Prover z3 z3-4.13.0 .
+PKGNAME = ${DISTNAME:S/z3-//}
-GH_ACCOUNT = Z3Prover
-GH_PROJECT = z3
-GH_TAGNAME = ${GH_PROJECT}-${VERSION}
-
-DISTNAME = ${GH_TAGNAME}
-PKGNAME = ${DISTNAME:L}
-
-SHARED_LIBS = z3 4.0 # 4.10
+SHARED_LIBS = z3 4.11
CATEGORIES = math
@@ -19,25 +12,27 @@ WANTLIB += c m pthread ${COMPILER_LIBCXX
# MIT
PERMIT_PACKAGE = Yes
-# c++11
+# C++17
COMPILER = base-clang ports-gcc
MODULES = devel/cmake \
lang/python
-CONFIGURE_ARGS += -DZ3_ENABLE_EXAMPLE_TARGETS=ON \
+MODPY_RUNDEP = No
+
+CONFIGURE_ARGS = -DZ3_BUILD_PYTHON_BINDINGS=ON \
+ -DZ3_ENABLE_EXAMPLE_TARGETS=OFF \
-DZ3_INCLUDE_GIT_HASH=OFF \
- -DZ3_INCLUDE_GIT_DESCRIBE=OFF \
- -DZ3_BUILD_PYTHON_BINDINGS=ON \
-DZ3_USE_LIB_GMP=OFF
DEBUG_PACKAGES = ${BUILD_PACKAGES}
-WRKDIST = ${WRKDIR}/z3-${DISTNAME}
-
-NO_TEST = Yes
-
-pre-configure:
+post-extract:
${SUBST_CMD} ${WRKSRC}/scripts/mk_util.py
+
+post-test:
+ cd ${WRKBUILD} && \
+ find ${WRKSRC}/examples/SMT-LIB2/ -type f -name '*.smt2' \
+ -exec echo \; -print -exec ./z3 {} \;
.include <bsd.port.mk>
Index: distinfo
===================================================================
RCS file: /cvs/ports/math/z3/distinfo,v
retrieving revision 1.14
diff -u -p -r1.14 distinfo
--- distinfo 12 Aug 2023 13:31:09 -0000 1.14
+++ distinfo 3 Sep 2024 16:05:14 -0000
@@ -1,2 +1,2 @@
-SHA256 (z3-4.12.2.tar.gz) = n1jzcQvSCUCFlRp1eRVQ9UeQPXX+fi/LNzxfA/x2G48=
-SIZE (z3-4.12.2.tar.gz) = 5401038
+SHA256 (Z3Prover-z3-z3-4.13.0.tar.gz) = AbzGHINi43u4n9JDD34zheht95FQGb0s5F3p2b2TRQI=
+SIZE (Z3Prover-z3-z3-4.13.0.tar.gz) = 5520232
Index: patches/patch-cmake_cxx_compiler_flags_overrides_cmake
===================================================================
RCS file: /cvs/ports/math/z3/patches/patch-cmake_cxx_compiler_flags_overrides_cmake,v
retrieving revision 1.2
diff -u -p -r1.2 patch-cmake_cxx_compiler_flags_overrides_cmake
--- patches/patch-cmake_cxx_compiler_flags_overrides_cmake 11 Mar 2022 19:36:33 -0000 1.2
+++ patches/patch-cmake_cxx_compiler_flags_overrides_cmake 3 Sep 2024 16:05:14 -0000
@@ -1,3 +1,5 @@
+Removed hardcoded optimizations
+
Index: cmake/cxx_compiler_flags_overrides.cmake
--- cmake/cxx_compiler_flags_overrides.cmake.orig
+++ cmake/cxx_compiler_flags_overrides.cmake
Index: patches/patch-scripts_mk_util_py
===================================================================
RCS file: /cvs/ports/math/z3/patches/patch-scripts_mk_util_py,v
retrieving revision 1.10
diff -u -p -r1.10 patch-scripts_mk_util_py
--- patches/patch-scripts_mk_util_py 9 Feb 2023 06:53:56 -0000 1.10
+++ patches/patch-scripts_mk_util_py 3 Sep 2024 16:05:14 -0000
@@ -1,7 +1,11 @@
+- Remove hardcoded optimizations
+- Fix .so versioning
+- use -fPIC to build shared libs on all archs
+
Index: scripts/mk_util.py
--- scripts/mk_util.py.orig
+++ scripts/mk_util.py
-@@ -2607,7 +2607,6 @@ def mk_config():
+@@ -2609,7 +2609,6 @@ def mk_config():
EXAMP_DEBUG_FLAG = '-g'
CPPFLAGS = '%s -DZ3DEBUG -D_DEBUG' % CPPFLAGS
else:
@@ -9,7 +13,7 @@ Index: scripts/mk_util.py
if GPROF:
CXXFLAGS += '-fomit-frame-pointer'
CPPFLAGS = '%s -DNDEBUG -D_EXTERNAL_RELEASE' % CPPFLAGS
-@@ -2632,7 +2631,7 @@ def mk_config():
+@@ -2634,7 +2633,7 @@ def mk_config():
SO_EXT = '.so'
SLIBFLAGS = '-shared'
elif sysname == 'OpenBSD':
@@ -18,15 +22,12 @@ Index: scripts/mk_util.py
SLIBFLAGS = '-shared'
elif sysname == 'SunOS':
SO_EXT = '.so'
-@@ -2648,9 +2647,8 @@ def mk_config():
+@@ -2650,7 +2649,7 @@ def mk_config():
LIB_EXT = '.lib'
else:
raise MKException('Unsupported platform: %s' % sysname)
- if is64():
-- if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-- CXXFLAGS = '%s -fPIC' % CXXFLAGS
-+ if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
-+ CXXFLAGS = '%s -fPIC' % CXXFLAGS
++ if true:
+ if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
+ CXXFLAGS = '%s -fPIC' % CXXFLAGS
elif not LINUX_X64:
- CXXFLAGS = '%s -m32' % CXXFLAGS
- LDFLAGS = '%s -m32' % LDFLAGS
Index: patches/patch-src_util_memory_manager_cpp
===================================================================
RCS file: patches/patch-src_util_memory_manager_cpp
diff -N patches/patch-src_util_memory_manager_cpp
--- /dev/null 1 Jan 1970 00:00:00 -0000
+++ patches/patch-src_util_memory_manager_cpp 3 Sep 2024 16:05:14 -0000
@@ -0,0 +1,111 @@
+https://github.com/Z3Prover/z3/issues/6902
+Index: src/util/memory_manager.cpp
+--- src/util/memory_manager.cpp.orig
++++ src/util/memory_manager.cpp
+@@ -29,6 +29,8 @@ Copyright (c) 2015 Microsoft Corporation
+ # define malloc_usable_size _msize
+ #endif
+
++#define SIZE_T_ALIGN 2
++
+ // The following two function are automatically generated by the mk_make.py script.
+ // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
+ // For example, rational.h contains
+@@ -278,7 +280,7 @@ void memory::deallocate(void * p) {
+ size_t sz = malloc_usable_size(p);
+ void * real_p = p;
+ #else
+- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
++ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
+ size_t sz = *sz_p;
+ void * real_p = reinterpret_cast<void*>(sz_p);
+ #endif
+@@ -291,7 +293,7 @@ void memory::deallocate(void * p) {
+
+ void * memory::allocate(size_t s) {
+ #ifndef HAS_MALLOC_USABLE_SIZE
+- s = s + sizeof(size_t); // we allocate an extra field!
++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
+ #endif
+ g_memory_thread_alloc_size += s;
+ g_memory_thread_alloc_count += 1;
+@@ -308,7 +310,7 @@ void * memory::allocate(size_t s) {
+ return r;
+ #else
+ *(static_cast<size_t*>(r)) = s;
+- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
+ #endif
+ }
+
+@@ -320,10 +322,10 @@ void* memory::reallocate(void *p, size_t s) {
+ if (sz >= s)
+ return p;
+ #else
+- size_t *sz_p = reinterpret_cast<size_t*>(p)-1;
++ size_t *sz_p = reinterpret_cast<size_t*>(p)-SIZE_T_ALIGN;
+ size_t sz = *sz_p;
+ void *real_p = reinterpret_cast<void*>(sz_p);
+- s = s + sizeof(size_t); // we allocate an extra field!
++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
+ #endif
+ g_memory_thread_alloc_size += s - sz;
+ g_memory_thread_alloc_count += 1;
+@@ -341,7 +343,7 @@ void* memory::reallocate(void *p, size_t s) {
+ return r;
+ #else
+ *(static_cast<size_t*>(r)) = s;
+- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
+ #endif
+ }
+
+@@ -358,7 +360,7 @@ void memory::deallocate(void * p) {
+ size_t sz = malloc_usable_size(p);
+ void * real_p = p;
+ #else
+- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
++ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
+ size_t sz = *sz_p;
+ void * real_p = reinterpret_cast<void*>(sz_p);
+ #endif
+@@ -368,7 +370,7 @@ void memory::deallocate(void * p) {
+
+ void * memory::allocate(size_t s) {
+ #ifndef HAS_MALLOC_USABLE_SIZE
+- s = s + sizeof(size_t); // we allocate an extra field!
++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
+ #endif
+ g_memory_alloc_size += s;
+ g_memory_alloc_count += 1;
+@@ -389,7 +391,7 @@ void * memory::allocate(size_t s) {
+ return r;
+ #else
+ *(static_cast<size_t*>(r)) = s;
+- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
+ #endif
+ }
+
+@@ -401,10 +403,10 @@ void* memory::reallocate(void *p, size_t s) {
+ if (sz >= s)
+ return p;
+ #else
+- size_t * sz_p = reinterpret_cast<size_t*>(p) - 1;
++ size_t * sz_p = reinterpret_cast<size_t*>(p) - SIZE_T_ALIGN;
+ size_t sz = *sz_p;
+ void * real_p = reinterpret_cast<void*>(sz_p);
+- s = s + sizeof(size_t); // we allocate an extra field!
++ s = s + SIZE_T_ALIGN * sizeof(size_t); // we allocate an extra field!
+ #endif
+ g_memory_alloc_size += s - sz;
+ g_memory_alloc_count += 1;
+@@ -425,7 +427,7 @@ void* memory::reallocate(void *p, size_t s) {
+ return r;
+ #else
+ *(static_cast<size_t*>(r)) = s;
+- return static_cast<size_t*>(r) + 1; // we return a pointer to the location after the extra field
++ return static_cast<size_t*>(r) + SIZE_T_ALIGN; // we return a pointer to the location after the extra field
+ #endif
+ }
+
Index: pkg/PLIST
===================================================================
RCS file: /cvs/ports/math/z3/pkg/PLIST,v
retrieving revision 1.9
diff -u -p -r1.9 PLIST
--- pkg/PLIST 11 Mar 2022 19:36:33 -0000 1.9
+++ pkg/PLIST 3 Sep 2024 16:05:14 -0000
@@ -1,4 +1,4 @@
-@conflict py3-z3-solver-*
+@conflict ${MODPY_PY_PREFIX}z3-solver-*
@bin bin/z3
include/z3++.h
include/z3.h
@@ -22,6 +22,8 @@ lib/cmake/z3/Z3Targets${MODCMAKE_BUILD_S
lib/cmake/z3/Z3Targets.cmake
@lib lib/libz3.so.${LIBz3_VERSION}
lib/pkgconfig/z3.pc
+lib/python${MODPY_VERSION}/
+lib/python${MODPY_VERSION}/site-packages/
lib/python${MODPY_VERSION}/site-packages/z3/
lib/python${MODPY_VERSION}/site-packages/z3/__init__.py
lib/python${MODPY_VERSION}/site-packages/z3/z3.py
--
wbr, Kirill
[update] math/z3: update to 4.13.0