z3: Portability fixes.

This commit is contained in:
jperkin 2022-05-13 10:41:38 +00:00
parent 971c72e443
commit 993b697e65
8 changed files with 86 additions and 9 deletions

View file

@ -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.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
${PLIST.java}lib/com.microsoft.z3.jar
${PLIST.java}lib/libz3java.so

View file

@ -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

View file

@ -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

View file

@ -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 2020/05/31 20:49:34 joerg Exp $
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')

View file

@ -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 {

View file

@ -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);

View file

@ -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):

View file

@ -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 {