CVS commit: pkgsrc/math/py-z3solver

["Jonathan Perkin" <jperkin%netbsd.org@localhost>]

Module Name:    pkgsrc
Committed By:   jperkin
Date:           Mon May  9 09:08:28 UTC 2022

Modified Files:
        pkgsrc/math/py-z3solver: distinfo
Added Files:
        pkgsrc/math/py-z3solver/patches: patch-core_scripts_mk__util.py
            patch-core_src_ast_value__generator.cpp
            patch-core_src_sat_sat__lookahead.cpp
            patch-core_src_sat_sat__solver.cpp
            patch-core_src_sat_smt_ba__solver.cpp
            patch-core_src_smt_smt__lookahead.cpp
            patch-core_src_solver_parallel__tactic.cpp

Log Message:
py-z3solver: Portability fixes.


To generate a diff of this commit:
cvs rdiff -u -r1.5 -r1.6 pkgsrc/math/py-z3solver/distinfo
cvs rdiff -u -r0 -r1.3 \
    pkgsrc/math/py-z3solver/patches/patch-core_scripts_mk__util.py
cvs rdiff -u -r0 -r1.1 \
    pkgsrc/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp \
    pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp \
    pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp \
    pkgsrc/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp \
    pkgsrc/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp \
    pkgsrc/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp

Please note that diffs are not public domain; they are subject to the
copyright notices on the relevant files.

Modified files:

Index: pkgsrc/math/py-z3solver/distinfo
diff -u pkgsrc/math/py-z3solver/distinfo:1.5 pkgsrc/math/py-z3solver/distinfo:1.6
--- pkgsrc/math/py-z3solver/distinfo:1.5        Tue Oct 26 10:56:06 2021
+++ pkgsrc/math/py-z3solver/distinfo    Mon May  9 09:08:27 2022
@@ -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

Added files:

Index: pkgsrc/math/py-z3solver/patches/patch-core_scripts_mk__util.py
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_scripts_mk__util.py:1.3
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_scripts_mk__util.py      Mon May  9 09:08:27 2022
@@ -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

Index: pkgsrc/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_ast_value__generator.cpp     Mon May  9 09:08:27 2022
@@ -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;
+ 
+ 
+ /*
Index: pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__lookahead.cpp       Mon May  9 09:08:27 2022
@@ -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); 
Index: pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_sat_sat__solver.cpp  Mon May  9 09:08:27 2022
@@ -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 {
+ 
+ 
Index: pkgsrc/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_sat_smt_ba__solver.cpp       Mon May  9 09:08:27 2022
@@ -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 {
+ 
Index: pkgsrc/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_smt_smt__lookahead.cpp       Mon May  9 09:08:27 2022
@@ -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): 
Index: pkgsrc/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp
diff -u /dev/null pkgsrc/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp:1.1
--- /dev/null   Mon May  9 09:08:28 2022
+++ pkgsrc/math/py-z3solver/patches/patch-core_src_solver_parallel__tactic.cpp  Mon May  9 09:08:27 2022
@@ -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 {
+ 
+