CVS commit: pkgsrc/math/z3

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

Module Name:    pkgsrc
Committed By:   jperkin
Date:           Fri May 13 10:41:38 UTC 2022

Modified Files:
        pkgsrc/math/z3: PLIST distinfo
        pkgsrc/math/z3/patches: patch-scripts_mk__genfile__common.py
            patch-scripts_mk__util.py
Added Files:
        pkgsrc/math/z3/patches: patch-src_sat_ba__solver.cpp
            patch-src_sat_sat__lookahead.cpp patch-src_sat_sat__solver.cpp
            patch-src_solver_parallel__tactic.cpp

Log Message:
z3: Portability fixes.


To generate a diff of this commit:
cvs rdiff -u -r1.3 -r1.4 pkgsrc/math/z3/PLIST
cvs rdiff -u -r1.11 -r1.12 pkgsrc/math/z3/distinfo
cvs rdiff -u -r1.1 -r1.2 \
    pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py
cvs rdiff -u -r1.6 -r1.7 pkgsrc/math/z3/patches/patch-scripts_mk__util.py
cvs rdiff -u -r0 -r1.1 pkgsrc/math/z3/patches/patch-src_sat_ba__solver.cpp \
    pkgsrc/math/z3/patches/patch-src_sat_sat__lookahead.cpp \
    pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp \
    pkgsrc/math/z3/patches/patch-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/z3/PLIST
diff -u pkgsrc/math/z3/PLIST:1.3 pkgsrc/math/z3/PLIST:1.4
--- pkgsrc/math/z3/PLIST:1.3    Tue Dec 18 06:46:39 2018
+++ pkgsrc/math/z3/PLIST        Fri May 13 10:41:38 2022
@@ -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_rcf.h
 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/z3ml
 ${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

Index: pkgsrc/math/z3/distinfo
diff -u pkgsrc/math/z3/distinfo:1.11 pkgsrc/math/z3/distinfo:1.12
--- pkgsrc/math/z3/distinfo:1.11        Tue Oct 26 10:56:13 2021
+++ pkgsrc/math/z3/distinfo     Fri May 13 10:41:38 2022
@@ -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

Index: pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py
diff -u pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py:1.1 pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py:1.2
--- pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py:1.1     Sun May 31 20:49:34 2020
+++ pkgsrc/math/z3/patches/patch-scripts_mk__genfile__common.py Fri May 13 10:41:38 2022
@@ -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

Index: pkgsrc/math/z3/patches/patch-scripts_mk__util.py
diff -u pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.6 pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.7
--- pkgsrc/math/z3/patches/patch-scripts_mk__util.py:1.6        Sun May 31 20:49:34 2020
+++ pkgsrc/math/z3/patches/patch-scripts_mk__util.py    Fri May 13 10:41:38 2022
@@ -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 @@ $NetBSD: patch-scripts_mk__util.py,v 1.6
          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')

Added files:

Index: pkgsrc/math/z3/patches/patch-src_sat_ba__solver.cpp
diff -u /dev/null pkgsrc/math/z3/patches/patch-src_sat_ba__solver.cpp:1.1
--- /dev/null   Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-src_sat_ba__solver.cpp Fri May 13 10:41:38 2022
@@ -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 {
+ 
Index: pkgsrc/math/z3/patches/patch-src_sat_sat__lookahead.cpp
diff -u /dev/null pkgsrc/math/z3/patches/patch-src_sat_sat__lookahead.cpp:1.1
--- /dev/null   Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-src_sat_sat__lookahead.cpp     Fri May 13 10:41:38 2022
@@ -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); 
Index: pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp
diff -u /dev/null pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp:1.1
--- /dev/null   Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-src_sat_sat__solver.cpp        Fri May 13 10:41:38 2022
@@ -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):
Index: pkgsrc/math/z3/patches/patch-src_solver_parallel__tactic.cpp
diff -u /dev/null pkgsrc/math/z3/patches/patch-src_solver_parallel__tactic.cpp:1.1
--- /dev/null   Fri May 13 10:41:38 2022
+++ pkgsrc/math/z3/patches/patch-src_solver_parallel__tactic.cpp        Fri May 13 10:41:38 2022
@@ -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 {
+ 
+