如何在Linux中为Python3安装Z3

Question

我正试图在python3中运行一个将Z3作为依赖项的程序(导入Z3)

我可以安装Z3的不稳定版本(假设它支持Python3)，但它只安装了python2.7的库。

以下是该项目的说明：

python scripts/mk_make.py
cd build
make
sudo make install

有人知道如何为Python3安装Z3吗？

谢谢。

Answer 1

我不得不修改scripts/mk_util.py，以便将Python2中的几行转换为Python3，并在其他几行中用空格替换tab，之后它就工作了！。

似乎有人无意中引入了与Python3不兼容的更改。

我注意到Leonardo de Moura关于这件事，他对z3 git repo进行了更改。

这是一条路径，以防万一

--- z3-original/scripts/mk_util.py
+++ z3/scripts/mk_util.py
@@ -640,7 +640,7 @@
def is_clang_in_gpp_form(cc):
version_string = subprocess.check_output([cc, '--version'])
-    return version_string.find('clang') != -1
+    return str(version_string).find('clang') != -1
def is_CXX_clangpp():
if is_compiler(CXX, 'g++'):
@@ -1485,7 +1485,7 @@
print('Java Compiler:  %s' % JAVAC)
else:
global CXX, CC, GMP, FOCI2, CPPFLAGS, CXXFLAGS, LDFLAGS, EXAMP_DEBUG_FLAG
-   OS_DEFINES = ""
+        OS_DEFINES = ""
ARITH = "internal"
check_ar()
CXX = find_cxx_compiler()
@@ -1508,7 +1508,7 @@
SLIBEXTRAFLAGS = '%s %s' % (SLIBEXTRAFLAGS,FOCI2LIB)
CPPFLAGS = '%s -D_FOCI2' % CPPFLAGS
else:
-                print "FAILEDn"
+                print("FAILEDn")
FOCI2 = False
if GIT_HASH:
CPPFLAGS = '%s -DZ3GITHASH=%s' % (CPPFLAGS, GIT_HASH)
@@ -1536,21 +1536,21 @@
SLIBFLAGS = '-dynamiclib'
elif sysname == 'Linux':
CXXFLAGS       = '%s -fno-strict-aliasing -D_LINUX_' % CXXFLAGS
-       OS_DEFINES     = '-D_LINUX'
+            OS_DEFINES     = '-D_LINUX'
SO_EXT         = '.so'
LDFLAGS        = '%s -lrt' % LDFLAGS
SLIBFLAGS      = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
elif sysname == 'FreeBSD':
CXXFLAGS       = '%s -fno-strict-aliasing -D_FREEBSD_' % CXXFLAGS
-       OS_DEFINES     = '-D_FREEBSD_'
+            OS_DEFINES     = '-D_FREEBSD_'
SO_EXT         = '.so'
LDFLAGS        = '%s -lrt' % LDFLAGS
SLIBFLAGS      = '-shared'
SLIBEXTRAFLAGS = '%s -lrt' % SLIBEXTRAFLAGS
elif sysname[:6] ==  'CYGWIN':
CXXFLAGS    = '%s -D_CYGWIN -fno-strict-aliasing' % CXXFLAGS
-       OS_DEFINES     = '-D_CYGWIN'
+            OS_DEFINES     = '-D_CYGWIN'
SO_EXT      = '.dll'
SLIBFLAGS   = '-shared'
else:
@@ -1586,7 +1586,7 @@
config.write('SLINK_FLAGS=%sn' % SLIBFLAGS)
config.write('SLINK_EXTRA_FLAGS=%sn' % SLIBEXTRAFLAGS)
config.write('SLINK_OUT_FLAG=-o n')
-   config.write('OS_DEFINES=%sn' % OS_DEFINES)
+        config.write('OS_DEFINES=%sn' % OS_DEFINES)
if is_verbose():
print('Host platform:  %s' % sysname)
print('C++ Compiler:   %s' % CXX)

Answer 2

对于以后对此有疑问的人。

我创建了一个从"python"到"python3"的别名，然后在z3 git repo上运行install命令。

alias python=python3 #alias for the script to use.
python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install