py-z3solver: Portability fixes.

8 files changed, 122 insertions, 1 deletions

diff --git a/math/py-z3solver/distinfo b/math/py-z3solver/distinfo
index 67cbbb1255d..41bbb7bffe5 100644
--- a/math/py-z3solver/distinfo
+++ b/math/py-z3solver/distinfo
@@ -1,5 +1,12 @@
-$NetBSD: distinfo,v 1.5 2021/10/26 10:56:06 nia Exp $
+$NetBSD: distinfo,v 1.6 2022/05/09 09:08:27 jperkin Exp $
 
 BLAKE2s (z3-solver-4.8.9.0.tar.gz) = 4dab8466b7321839504e930daae1d0ef0e3866fbcc73a5e8d457a19bb94a18fb
 SHA512 (z3-solver-4.8.9.0.tar.gz) = bc137b505cc24e54e50b1aa3d7ee4161593de17f14198f926beaaf285f210742635f4be22d61456d19688a73f422ca60a24c84eeecf5e783d1dcf26f65a1b8ab
 Size (z3-solver-4.8.9.0.tar.gz) = 4503933 bytes
+SHA1 (patch-core_scripts_mk__util.py) = 195a122a7b6988a607ab2b66da48c79d183aa50e
+SHA1 (patch-core_src_ast_value__generator.cpp) = 7e5a1228b2fa329e14fdc8fc478cc3cffd6c4241
+SHA1 (patch-core_src_sat_sat__lookahead.cpp) = 5817853051f6bee34b417f7d699e8c16f51ce405
+SHA1 (patch-core_src_sat_sat__solver.cpp) = 3fd36f13cfefd2614f7fb6b83b4e64f8f7eadae0
+SHA1 (patch-core_src_sat_smt_ba__solver.cpp) = aad2d3ef2cd0f192bf631bd2e65c4178aa5f2992
+SHA1 (patch-core_src_smt_smt__lookahead.cpp) = b17fda39daebd7904768a7f3383eceb59edb6998
+SHA1 (patch-core_src_solver_parallel__tactic.cpp) = 4e20b03b9710803c17ddecd3e1a97216c3cd66d4
diff --git a/math/py-z3solver/patches/patch-core_scripts_mk__util.py b/math/py-z3solver/patches/patch-core_scripts_mk__util.py
new file mode 100644
index 00000000000..0d214c6ceaf
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_scripts_mk__util.py
@@ -0,0 +1,26 @@
+$NetBSD: patch-core_scripts_mk__util.py,v 1.3 2022/05/09 09:08:27 jperkin Exp $
+
+Try to at least use sensible defaults on unknown platforms.
+
+--- core/scripts/mk_util.py.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/scripts/mk_util.py
+@@ -1263,8 +1263,7 @@ def get_so_ext():
+     elif sysname == 'CYGWIN' or sysname.startswith('MSYS_NT') or sysname.startswith('MINGW'):
+         return 'dll'
+     else:
+-        assert(False)
+-        return 'dll'
++        return 'so'
+ 
+ class DLLComponent(Component):
+     def __init__(self, name, dll_name, path, deps, export_files, reexports, install, static, staging_link=None):
+@@ -2527,7 +2526,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
diff --git a/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp b/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp
new file mode 100644
index 00000000000..133c70b61e1
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp
@@ -0,0 +1,14 @@
+$NetBSD: patch-core_src_ast_value__generator.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/ast/value_generator.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/ast/value_generator.cpp
+@@ -23,6 +23,7 @@
+ #include "ast/seq_decl_plugin.h"
+ #include <cmath>
+ 
++using std::sqrt;
+ 
+ 
+ /*
diff --git a/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp b/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp
new file mode 100644
index 00000000000..f206742b474
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp
@@ -0,0 +1,15 @@
+$NetBSD: patch-core_src_sat_sat__lookahead.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/sat/sat_lookahead.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/sat/sat_lookahead.cpp
+@@ -26,6 +26,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 --git a/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp b/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp
new file mode 100644
index 00000000000..91a93d14af8
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp
@@ -0,0 +1,15 @@
+$NetBSD: patch-core_src_sat_sat__solver.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/sat/sat_solver.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/sat/sat_solver.cpp
+@@ -40,6 +40,8 @@ Revision History:
+ #define ENABLE_TERNARY true
+ #define DYNAMIC_VARS true
+ 
++using std::pow;
++
+ namespace sat {
+ 
+ 
diff --git a/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp b/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp
new file mode 100644
index 00000000000..7f9351a8d19
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp
@@ -0,0 +1,14 @@
+$NetBSD: patch-core_src_sat_smt_ba__solver.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/sat/smt/ba_solver.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/sat/smt/ba_solver.cpp
+@@ -23,6 +23,7 @@ Author:
+ #include "sat/sat_simplifier_params.hpp"
+ #include "sat/sat_xor_finder.h"
+ 
++using std::pow;
+ 
+ namespace sat {
+ 
diff --git a/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp b/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp
new file mode 100644
index 00000000000..5770bf822ec
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp
@@ -0,0 +1,15 @@
+$NetBSD: patch-core_src_smt_smt__lookahead.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/smt/smt_lookahead.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/smt/smt_lookahead.cpp
+@@ -23,6 +23,8 @@ Revision History:
+ #include "smt/smt_lookahead.h"
+ #include "smt/smt_context.h"
+ 
++using std::pow;
++
+ namespace smt {
+ 
+     lookahead::lookahead(context& ctx): 
diff --git a/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp b/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp
new file mode 100644
index 00000000000..a2812287b54
--- /dev/null
+++ b/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp
@@ -0,0 +1,15 @@
+$NetBSD: patch-core_src_solver_parallel__tactic.cpp,v 1.1 2022/05/09 09:08:27 jperkin Exp $
+
+Avoid ambiguous function calls.
+
+--- core/src/solver/parallel_tactic.cpp.orig	2020-09-11 00:52:41.000000000 +0000
++++ core/src/solver/parallel_tactic.cpp
+@@ -52,6 +52,8 @@ tactic * mk_parallel_tactic(solver* s, p
+ #include <cmath>
+ #include <condition_variable>
+ 
++using std::pow;
++
+ class parallel_tactic : public tactic {
+ 
+