[pkgsrc/trunk]: pkgsrc/math/z3 z3: Portability fixes.

[jperkin <jperkin%pkgsrc.org@localhost>]

details:   https://anonhg.NetBSD.org/pkgsrc/rev/e0c9bca232e7
branches:  trunk
changeset: 379215:e0c9bca232e7
user:      jperkin <jperkin%pkgsrc.org@localhost>
date:      Fri May 13 10:41:38 2022 +0000

description:
z3: Portability fixes.

diffstat:

 math/z3/PLIST                                         |   6 +++---
 math/z3/distinfo                                      |  10 +++++++---
 math/z3/patches/patch-scripts_mk__genfile__common.py  |   4 +++-
 math/z3/patches/patch-scripts_mk__util.py             |  16 ++++++++++++++--
 math/z3/patches/patch-src_sat_ba__solver.cpp          |  14 ++++++++++++++
 math/z3/patches/patch-src_sat_sat__lookahead.cpp      |  15 +++++++++++++++
 math/z3/patches/patch-src_sat_sat__solver.cpp         |  15 +++++++++++++++
 math/z3/patches/patch-src_solver_parallel__tactic.cpp |  15 +++++++++++++++
 8 files changed, 86 insertions(+), 9 deletions(-)

diffs (159 lines):

diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/PLIST
--- a/math/z3/PLIST     Fri May 13 10:39:35 2022 +0000
+++ b/math/z3/PLIST     Fri May 13 10:41:38 2022 +0000
@@ -1,4 +1,4 @@
-@comment $NetBSD: PLIST,v 1.3 2018/12/18 06:46:39 kamil Exp $
+@comment $NetBSD: PLIST,v 1.4 2022/05/13 10:41:38 jperkin Exp $
 bin/z3
 include/z3++.h
 include/z3.h
@@ -14,7 +14,9 @@
 include/z3_spacer.h
 include/z3_v1.h
 include/z3_version.h
+${PLIST.java}lib/com.microsoft.z3.jar
 lib/libz3.so
+${PLIST.java}lib/libz3java.so
 ${PLIST.ocaml}lib/ocaml/site-lib/Z3/META
 ${PLIST.ocaml}lib/ocaml/site-lib/Z3/dllz3ml.so
 ${PLIST.ocaml}lib/ocaml/site-lib/Z3/libz3ml.a
@@ -31,5 +33,3 @@
 ${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
-${PLIST.java}lib/com.microsoft.z3.jar
-${PLIST.java}lib/libz3java.so
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/distinfo
--- a/math/z3/distinfo  Fri May 13 10:39:35 2022 +0000
+++ b/math/z3/distinfo  Fri May 13 10:41:38 2022 +0000
@@ -1,7 +1,11 @@
-$NetBSD: distinfo,v 1.11 2021/10/26 10:56:13 nia Exp $
+$NetBSD: distinfo,v 1.12 2022/05/13 10:41:38 jperkin 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) = ecedf747f4a5b4cb410898a6cb65eed2aad46d27
-SHA1 (patch-scripts_mk__util.py) = 79106c08ce39901d13eaab5a18173fcb0479dc96
+SHA1 (patch-scripts_mk__genfile__common.py) = 442da5eb2dcdfa4e4a5d70dc377c29053f58be5a
+SHA1 (patch-scripts_mk__util.py) = f7059330a8ea44a566448557fae3967051e237cb
+SHA1 (patch-src_sat_ba__solver.cpp) = 1e80b79c76f8e3766a60be3065ff8bd932249178
+SHA1 (patch-src_sat_sat__lookahead.cpp) = c091d8b267b5476e438888e82c9161599873264c
+SHA1 (patch-src_sat_sat__solver.cpp) = 3421afbf641c47cf3b44ece9168ff3f768168343
+SHA1 (patch-src_solver_parallel__tactic.cpp) = 029a2625e19cfcfb18c4b69279dea257cfd5482f
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-scripts_mk__genfile__common.py
--- a/math/z3/patches/patch-scripts_mk__genfile__common.py      Fri May 13 10:39:35 2022 +0000
+++ b/math/z3/patches/patch-scripts_mk__genfile__common.py      Fri May 13 10:41:38 2022 +0000
@@ -1,4 +1,6 @@
-$NetBSD: patch-scripts_mk__genfile__common.py,v 1.1 2020/05/31 20:49:34 joerg Exp $
+$NetBSD: patch-scripts_mk__genfile__common.py,v 1.2 2022/05/13 10:41:38 jperkin Exp $
+
+Python 3 compat.
 
 --- scripts/mk_genfile_common.py.orig  2018-11-19 20:21:17.000000000 +0000
 +++ scripts/mk_genfile_common.py
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-scripts_mk__util.py
--- a/math/z3/patches/patch-scripts_mk__util.py Fri May 13 10:39:35 2022 +0000
+++ b/math/z3/patches/patch-scripts_mk__util.py Fri May 13 10:41:38 2022 +0000
@@ -1,4 +1,6 @@
-$NetBSD: patch-scripts_mk__util.py,v 1.6 2020/05/31 20:49:34 joerg Exp $
+$NetBSD: patch-scripts_mk__util.py,v 1.7 2022/05/13 10:41:38 jperkin 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
@@ -31,7 +33,17 @@
          EXE_EXT = ''
          LIB_EXT = '.a'
          if GPROF:
-@@ -2822,6 +2824,7 @@ def mk_config():
+@@ -2778,7 +2780,8 @@ def mk_config():
+             EXE_EXT        = '.exe'
+             LIB_EXT        = '.lib'
+         else:
+-            raise MKException('Unsupported platform: %s' % sysname)
++            SO_EXT         = '.so'
++            SLIBFLAGS      = '-shared'
+         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():
          config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)
          config.write('SLINK_EXTRA_FLAGS=%s\n' % SLIBEXTRAFLAGS)
          config.write('SLINK_OUT_FLAG=-o \n')
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-src_sat_ba__solver.cpp
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_sat_ba__solver.cpp      Fri May 13 10:41:38 2022 +0000
@@ -0,0 +1,14 @@
+$NetBSD: patch-src_sat_ba__solver.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+
+Avoid ambiguous function call.
+
+--- src/sat/ba_solver.cpp.orig 2018-11-19 20:21:17.000000000 +0000
++++ src/sat/ba_solver.cpp
+@@ -23,6 +23,7 @@ Revision History:
+ #include "util/mpz.h"
+ #include "sat/sat_simplifier_params.hpp"
+ 
++using std::pow;
+ 
+ namespace sat {
+ 
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-src_sat_sat__lookahead.cpp
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_sat_sat__lookahead.cpp  Fri May 13 10:41:38 2022 +0000
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_sat_sat__lookahead.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+
+Avoid ambiguous function call.
+
+--- src/sat/sat_lookahead.cpp.orig     2018-11-19 20:21:17.000000000 +0000
++++ src/sat/sat_lookahead.cpp
+@@ -27,6 +27,8 @@ Notes:
+ #include "sat/sat_scc.h"
+ #include "util/union_find.h"
+ 
++using std::pow;
++
+ namespace sat {
+     lookahead::scoped_ext::scoped_ext(lookahead& p): p(p) {
+         if (p.m_s.m_ext) p.m_s.m_ext->set_lookahead(&p); 
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-src_sat_sat__solver.cpp
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_sat_sat__solver.cpp     Fri May 13 10:41:38 2022 +0000
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_sat_sat__solver.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+
+Avoid ambiguous function call.
+
+--- src/sat/sat_solver.cpp.orig        2018-11-19 20:21:17.000000000 +0000
++++ src/sat/sat_solver.cpp
+@@ -31,6 +31,8 @@ Revision History:
+ // define to update glue during propagation
+ #define UPDATE_GLUE
+ 
++using std::pow;
++
+ namespace sat {
+ 
+     solver::solver(params_ref const & p, reslimit& l):
diff -r 34e9d51ce66c -r e0c9bca232e7 math/z3/patches/patch-src_solver_parallel__tactic.cpp
--- /dev/null   Thu Jan 01 00:00:00 1970 +0000
+++ b/math/z3/patches/patch-src_solver_parallel__tactic.cpp     Fri May 13 10:41:38 2022 +0000
@@ -0,0 +1,15 @@
+$NetBSD: patch-src_solver_parallel__tactic.cpp,v 1.1 2022/05/13 10:41:38 jperkin Exp $
+
+Avoid ambiguous function call.
+
+--- src/solver/parallel_tactic.cpp.orig        2018-11-19 20:21:17.000000000 +0000
++++ src/solver/parallel_tactic.cpp
+@@ -42,6 +42,8 @@ Notes:
+ #include "solver/parallel_tactic.h"
+ #include "solver/parallel_params.hpp"
+ 
++using std::pow;
++
+ class parallel_tactic : public tactic {
+ 
+