@@ -1,25 +1,26 @@
-# $NetBSD: Makefile,v 1.4 2020/05/31 20:47:23 joerg Exp $
+# $NetBSD: Makefile,v 1.5 2023/05/11 06:43:43 adam Exp $
 
 .include "../../math/z3/Makefile.common"
 
 PKGNAME=	${PYPKGPREFIX}-${DISTNAME}
-GITHUB_PROJECT=	z3
+COMMENT=	Efficient SMT solver library
 
-COMMENT=	Python bindings for the Z3 theorem prover / SMT solver
+USE_TOOLS+=	cmake ninja
+PYSETUPSUBDIR=	src/api/python
+EGG_NAME=	${DISTNAME:S/z3/z3_solver/}.0
 
-CONFIGURE_ARGS+=	--python
-NO_BUILD=		yes
-PY_PATCHPLIST=		yes
+.include "../../mk/bsd.prefs.mk"
 
-PYZ3DIR=		${PREFIX}/${PYSITELIB}/z3
-INSTALLATION_DIRS+=	${PYZ3DIR}
-INSTALLATION_DIRS+=	${PYZ3DIR}/lib
+post-install:
+	# same binary as in math/z3
+	${RM} ${DESTDIR}${PREFIX}/bin/z3
+.if ${OPSYS} == "Darwin"
+	install_name_tool -id ${PREFIX}/${PYSITELIB}/z3/lib/libz3.${PKGVERSION_NOREV:R}.dylib \
+	${DESTDIR}${PREFIX}/${PYSITELIB}/z3/lib/libz3.${PKGVERSION_NOREV:R}.dylib
+	install_name_tool -id ${PREFIX}/${PYSITELIB}/z3/lib/libz3.dylib \
+	${DESTDIR}${PREFIX}/${PYSITELIB}/z3/lib/libz3.dylib
+.endif
 
-do-install:
-	${LN} -s ${LIBDIR}/libz3.so ${DESTDIR}${PYZ3DIR}/lib/libz3.so
-	${INSTALL_DATA} ${WRKSRC}/build/python/z3/*.py ${DESTDIR}${PYZ3DIR}
-	${PY_COMPILE_ALL} ${DESTDIR}${PYZ3DIR}
-
-.include "../../lang/python/extension.mk"
+.include "../../lang/python/egg.mk"
 .include "../../math/z3/buildlink3.mk"
 .include "../../mk/bsd.pkg.mk"

@@ -1,22 +1,64 @@
-@comment $NetBSD: PLIST,v 1.1 2018/03/13 00:36:05 khorben Exp $
+@comment $NetBSD: PLIST,v 1.2 2023/05/11 06:43:43 adam Exp $
+${PYSITELIB}/${EGG_INFODIR}/PKG-INFO
+${PYSITELIB}/${EGG_INFODIR}/SOURCES.txt
+${PYSITELIB}/${EGG_INFODIR}/dependency_links.txt
+${PYSITELIB}/${EGG_INFODIR}/top_level.txt
 ${PYSITELIB}/z3/__init__.py
 ${PYSITELIB}/z3/__init__.pyc
+${PYSITELIB}/z3/__init__.pyo
+${PYSITELIB}/z3/include/api_ast_map.h
+${PYSITELIB}/z3/include/api_ast_vector.h
+${PYSITELIB}/z3/include/api_context.h
+${PYSITELIB}/z3/include/api_datalog.h
+${PYSITELIB}/z3/include/api_goal.h
+${PYSITELIB}/z3/include/api_model.h
+${PYSITELIB}/z3/include/api_polynomial.h
+${PYSITELIB}/z3/include/api_solver.h
+${PYSITELIB}/z3/include/api_stats.h
+${PYSITELIB}/z3/include/api_tactic.h
+${PYSITELIB}/z3/include/api_util.h
+${PYSITELIB}/z3/include/z3++.h
+${PYSITELIB}/z3/include/z3.h
+${PYSITELIB}/z3/include/z3_algebraic.h
+${PYSITELIB}/z3/include/z3_api.h
+${PYSITELIB}/z3/include/z3_ast_containers.h
+${PYSITELIB}/z3/include/z3_fixedpoint.h
+${PYSITELIB}/z3/include/z3_fpa.h
+${PYSITELIB}/z3/include/z3_logger.h
+${PYSITELIB}/z3/include/z3_macros.h
+${PYSITELIB}/z3/include/z3_optimization.h
+${PYSITELIB}/z3/include/z3_polynomial.h
+${PYSITELIB}/z3/include/z3_private.h
+${PYSITELIB}/z3/include/z3_rcf.h
+${PYSITELIB}/z3/include/z3_replayer.h
+${PYSITELIB}/z3/include/z3_spacer.h
+${PYSITELIB}/z3/include/z3_v1.h
 ${PYSITELIB}/z3/lib/libz3.so
+${PYSITELIB}/z3/lib/libz3.so.4.12
 ${PYSITELIB}/z3/z3.py
 ${PYSITELIB}/z3/z3.pyc
+${PYSITELIB}/z3/z3.pyo
 ${PYSITELIB}/z3/z3consts.py
 ${PYSITELIB}/z3/z3consts.pyc
+${PYSITELIB}/z3/z3consts.pyo
 ${PYSITELIB}/z3/z3core.py
 ${PYSITELIB}/z3/z3core.pyc
+${PYSITELIB}/z3/z3core.pyo
 ${PYSITELIB}/z3/z3num.py
 ${PYSITELIB}/z3/z3num.pyc
+${PYSITELIB}/z3/z3num.pyo
 ${PYSITELIB}/z3/z3poly.py
 ${PYSITELIB}/z3/z3poly.pyc
+${PYSITELIB}/z3/z3poly.pyo
 ${PYSITELIB}/z3/z3printer.py
 ${PYSITELIB}/z3/z3printer.pyc
+${PYSITELIB}/z3/z3printer.pyo
 ${PYSITELIB}/z3/z3rcf.py
 ${PYSITELIB}/z3/z3rcf.pyc
+${PYSITELIB}/z3/z3rcf.pyo
 ${PYSITELIB}/z3/z3types.py
 ${PYSITELIB}/z3/z3types.pyc
+${PYSITELIB}/z3/z3types.pyo
 ${PYSITELIB}/z3/z3util.py
 ${PYSITELIB}/z3/z3util.pyc
+${PYSITELIB}/z3/z3util.pyo

@@ -1,9 +1,8 @@
-# $NetBSD: Makefile,v 1.17 2022/09/25 11:01:34 he Exp $
+# $NetBSD: Makefile,v 1.18 2023/05/11 06:43:43 adam Exp $
 
 .include "Makefile.common"
-PKGREVISION=	4
+
 COMMENT=	The Z3 theorem prover / SMT solver
 
-.include "options.mk"
-
+.include "../../devel/cmake/build.mk"
 .include "../../mk/bsd.pkg.mk"

@@ -1,24 +1,21 @@
-# $NetBSD: Makefile.common,v 1.4 2018/12/18 06:46:39 kamil Exp $
+# $NetBSD: Makefile.common,v 1.5 2023/05/11 06:43:43 adam Exp $
 #
 # used by math/py-z3/Makefile
 # used by math/z3/Makefile
 
-DISTNAME=	z3-4.8.3
-GITHUB_TAG=	${DISTNAME}
+DISTNAME=	z3-4.12.1
 CATEGORIES=	math
 MASTER_SITES=	${MASTER_SITE_GITHUB:=Z3Prover/}
+GITHUB_PROJECT=	z3
+GITHUB_TAG=	${DISTNAME}
+
 DISTINFO_FILE=	${.CURDIR}/../../math/z3/distinfo
 PATCHDIR?=	${.CURDIR}/../../math/z3/patches
 
 MAINTAINER=	dholland@NetBSD.org
-HOMEPAGE=	https://github.com/Z3Prover/z3/
+HOMEPAGE=	https://github.com/Z3Prover/z3
 LICENSE=	mit
 
-WRKSRC=		${WRKDIR}/z3-${DISTNAME}
-HAS_CONFIGURE=	yes
 USE_LANGUAGES=	c c++
-BUILD_DIRS=	build
-
-CONFIGURE_ENV+=		PYTHON=${PYTHONBIN}
 
 .include "../../lang/python/tool.mk"

@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.4 2022/05/13 10:41:38 jperkin Exp $
+@comment $NetBSD: PLIST,v 1.5 2023/05/11 06:43:43 adam Exp $
 bin/z3
 include/z3++.h
 include/z3.h
@@ -14,22 +14,11 @@
 include/z3_spacer.h
 include/z3_v1.h
 include/z3_version.h
-${PLIST.java}lib/com.microsoft.z3.jar
+lib/cmake/z3/Z3Config.cmake
+lib/cmake/z3/Z3ConfigVersion.cmake
+lib/cmake/z3/Z3Targets-relwithdebinfo.cmake
+lib/cmake/z3/Z3Targets.cmake
 lib/libz3.so
-${PLIST.java}lib/libz3java.so
+lib/libz3.so.4.12
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
+lib/libz3.so.${PKGVERSION}.0
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
+lib/pkgconfig/z3.pc
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/libz3ml.a
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3.mli
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3enums.mli
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.a
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cma
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxa
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3ml.cmxs
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmi
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.cmx
-${PLIST.ocaml}lib/ocaml/site-lib/Z3/z3native.mli

@@ -1,14 +1,9 @@
-$NetBSD: distinfo,v 1.13 2022/09/25 11:01:34 he Exp $
+$NetBSD: distinfo,v 1.14 2023/05/11 06:43:43 adam Exp $
 
-BLAKE2s (z3-4.8.3.tar.gz) = 18b9f2b708f35c57c4dfb425521106dd7f938296738087ff761f030bff7a3491
-SHA512 (z3-4.8.3.tar.gz) = 34a2dca0083ed469fdaf5ac062dda26248633245607ddd9ef90629c5f76ae30f87bfa4191c04ba9be7a617bf182a1bd00b59fd2274699e12ece69b86088c8044
-Size (z3-4.8.3.tar.gz) = 4119116 bytes
-SHA1 (patch-scripts_mk__genfile__common.py) = 442da5eb2dcdfa4e4a5d70dc377c29053f58be5a
-SHA1 (patch-scripts_mk__util.py) = f7059330a8ea44a566448557fae3967051e237cb
-SHA1 (patch-src_parsers_util_scanner.cpp) = 284f9ef965c4d4f4954fcbb6437c143c57dde516
-SHA1 (patch-src_parsers_util_scanner.h) = ad1b385672615501a9249b20829256052ce82dbd
-SHA1 (patch-src_sat_ba__solver.cpp) = 1e80b79c76f8e3766a60be3065ff8bd932249178
+BLAKE2s (z3-4.12.1.tar.gz) = 375c80eb90c2cf43b6d42006fcb6618a30a4ce6bb8a761dd8849565ed3ba1ca9
+SHA512 (z3-4.12.1.tar.gz) = 031fba9cc000a8da0025f95fa3f1c7519071d1b7775b377ff3192c505bb4c7e3d267da246c9ae68c940224e055a3c30571d2c0d7fbb042ec9a3d5849543a385c
+Size (z3-4.12.1.tar.gz) = 5470095 bytes
+SHA1 (patch-scripts_mk__util.py) = f092c9aed3c81408a485e9c92d8dddf5db86d6fe
+SHA1 (patch-src_api_python_setup.py) = cfc4a0a388d2a096ce86cbe3ca76b32502ec380e
 SHA1 (patch-src_sat_sat__lookahead.cpp) = c091d8b267b5476e438888e82c9161599873264c
-SHA1 (patch-src_sat_sat__solver.cpp) = 3421afbf641c47cf3b44ece9168ff3f768168343
+SHA1 (patch-src_sat_sat__solver.cpp) = 0e279f291801901eabb11b7cb0268c137a3b41fe
-SHA1 (patch-src_solver_parallel__tactic.cpp) = 029a2625e19cfcfb18c4b69279dea257cfd5482f
-SHA1 (patch-src_util_mpz.cpp) = 499062b5107572184adcb7353ccde7c9f7b28951

@@ -1,39 +1,29 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.7 2022/05/13 10:41:38 jperkin Exp $
+$NetBSD: patch-scripts_mk__util.py,v 1.8 2023/05/11 06:43:43 adam Exp $
 
 Try to at least be slightly more portable.
 
---- scripts/mk_util.py.orig	2018-11-19 20:21:17.000000000 +0000
+--- scripts/mk_util.py.orig	2023-01-18 03:10:26.000000000 +0000
 +++ scripts/mk_util.py
-@@ -803,7 +803,8 @@ def extract_c_includes(fname):
-     # We should generate and error for any occurrence of #include that does not match the previous pattern.
-     non_std_inc_pat = re.compile(".*#include.*")
- 
--    f = open(fname, 'r')
-+    py3args = { 'encoding': 'UTF-8' } if sys.version_info.major >= 3 else {}
-+    f = open(fname, 'r', **py3args)
-     linenum = 1
-     for line in f:
-         m1 = std_inc_pat.match(line)
-@@ -2001,7 +2002,7 @@ class JavaDLLComponent(Component):
-                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
-                           os.path.join('api', 'java', 'Native'))
+@@ -1858,7 +1858,7 @@ class JavaDLLComponent(Component):
+                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) -arch arm64 %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
+                           os.path.join('api', 'java', 'Native'))                
              else:
 -                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
 +                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) $(JAVA_LINK_EXTRA_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT)\n' %
                            os.path.join('api', 'java', 'Native'))
              out.write('%s.jar: libz3java$(SO_EXT) ' % self.package_name)
              deps = ''
-@@ -2694,7 +2695,8 @@ def mk_config():
+@@ -2577,7 +2577,8 @@ def mk_config():
          check_ar()
          CXX = find_cxx_compiler()
          CC  = find_c_compiler()
 -        SLIBEXTRAFLAGS = ''
 +        SLIBEXTRAFLAGS = LDFLAGS
 +        JAVALIBEXTRAFLAGS = LDFLAGS
+ #       SLIBEXTRAFLAGS = '%s -Wl,-soname,libz3.so.0' % LDFLAGS
          EXE_EXT = ''
          LIB_EXT = '.a'
-         if GPROF:
-@@ -2778,7 +2780,8 @@ def mk_config():
+@@ -2647,7 +2648,8 @@ def mk_config():
              EXE_EXT        = '.exe'
              LIB_EXT        = '.lib'
          else:
@@ -43,9 +33,9 @@
          if is64():
              if not sysname.startswith('CYGWIN') and not sysname.startswith('MSYS') and not sysname.startswith('MINGW'):
                  CXXFLAGS     = '%s -fPIC' % CXXFLAGS
-@@ -2822,6 +2825,7 @@ def mk_config():
+@@ -2696,6 +2698,7 @@ def mk_config():
          config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
-         config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
+         config.write('SLINK_EXTRA_FLAGS=-lpthread %s\n' % SLIBEXTRAFLAGS)
          config.write('SLINK_OUT_FLAG=-o \n')
 +        config.write('JAVA_LINK_EXTRA_FLAGS=%s\n' % JAVALIBEXTRAFLAGS)
          config.write('OS_DEFINES=%s\n' % OS_DEFINES)

@@ -1,15 +1,14 @@
-$NetBSD: patch-src_sat_sat__solver.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+$NetBSD: patch-src_sat_sat__solver.cpp,v 1.2 2023/05/11 06:43:43 adam Exp $
 
 Avoid ambiguous function call.
 
---- src/sat/sat_solver.cpp.orig	2018-11-19 20:21:17.000000000 +0000
+--- src/sat/sat_solver.cpp.orig	2023-05-08 13:23:26.000000000 +0000
 +++ src/sat/sat_solver.cpp
-@@ -31,6 +31,8 @@ Revision History:
- // define to update glue during propagation
- #define UPDATE_GLUE
+@@ -37,6 +37,7 @@ Revision History:
+ # include <xmmintrin.h>
+ #endif
  
 +using std::pow;
-+
+ 
  namespace sat {
  
-     solver::solver(params_ref const & p, reslimit& l):