diff --git a/examples/python/example.py b/examples/python/example.py index e0c9374e7..a17668506 100644 --- a/examples/python/example.py +++ b/examples/python/example.py @@ -1,4 +1,30 @@ -# Copyright (c) Microsoft Corporation 2015 +# Copyright (c) Microsoft Corporation 2015, 2016 + +# The Z3 Python API requires libz3.dll/.so/.dylib in the +# PATH/LD_LIBRARY_PATH/DYLD_LIBRARY_PATH +# environment variable and the PYTHON_PATH environment variable +# needs to point to the `python' directory that contains `z3/z3.py' +# (which is at bin/python in our binary releases). + +# If you obtained example.py as part of our binary release zip files, +# which you unzipped into a directory called `MYZ3', then follow these +# instructions to run the example: + +# Running this example on Windows: +# set PATH=%PATH%;MYZ3\bin +# set PYTHONPATH=MYZ3\bin\python +# python example.py + +# Running this example on Linux: +# export LD_LIBRARY_PATH=$LD_LIBRARY_PATH:MYZ3/bin +# export PYTHONPATH=MYZ3/bin/python +# python example.py + +# Running this example on OSX: +# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin +# export PYTHONPATH=MYZ3/bin/python +# python example.py + from z3 import * diff --git a/scripts/mk_project.py b/scripts/mk_project.py index c03d76b5f..b18e7801b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -94,6 +94,7 @@ def init_project_def(): add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') + add_python(_libz3Component) add_python_install(_libz3Component) # Examples add_cpp_example('cpp_example', 'c++') diff --git a/scripts/mk_unix_dist.py b/scripts/mk_unix_dist.py index 4905a7141..527797e66 100644 --- a/scripts/mk_unix_dist.py +++ b/scripts/mk_unix_dist.py @@ -26,6 +26,7 @@ DOTNET_ENABLED=True DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False +PYTHON_ENABLED=True def set_verbose(flag): global VERBOSE @@ -55,6 +56,7 @@ def display_help(): print(" --nodotnet do not include .NET bindings in the binary distribution files.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") + print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") exit(0) @@ -69,7 +71,8 @@ def parse_options(): 'nojava', 'nodotnet', 'dotnet-key=', - 'githash' + 'githash', + 'nopython' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -84,6 +87,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--nopython': + PYTHON_ENABLED = False elif opt == '--dotnet-key': DOTNET_KEY_FILE = arg elif opt == '--nojava': @@ -111,6 +116,8 @@ def mk_build_dir(path): if GIT_HASH: opts.append('--githash=%s' % mk_util.git_hash()) opts.append('--git-describe') + if PYTHON_ENABLED: + opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) @@ -181,6 +188,7 @@ def mk_dist_dir(): mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED + mk_util.PYTHON_ENABLED = PYTHON_ENABLED mk_unix_dist(build_path, dist_path) if is_verbose(): print("Generated distribution folder at '%s'" % dist_path) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 873af8432..cf06a10a7 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -63,6 +63,7 @@ DOTNET_COMPONENT='dotnet' JAVA_COMPONENT='java' ML_COMPONENT='ml' CPP_COMPONENT='cpp' +PYTHON_COMPONENT='python' ##################### IS_WINDOWS=False IS_LINUX=False @@ -81,6 +82,7 @@ ONLY_MAKEFILES = False Z3PY_SRC_DIR=None VS_PROJ = False TRACE = False +PYTHON_ENABLED=False DOTNET_ENABLED=False DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None) JAVA_ENABLED=False @@ -675,7 +677,7 @@ def display_help(exit_code): # Parse configuration option for mk_make script def parse_options(): global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM - global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED + global DOTNET_ENABLED, DOTNET_KEY_FILE, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED global LINUX_X64, SLOW_OPTIMIZE, USE_OMP try: options, remainder = getopt.gnu_getopt(sys.argv[1:], @@ -748,6 +750,7 @@ def parse_options(): elif opt in ('', '--noomp'): USE_OMP = False elif opt in ('--python'): + PYTHON_ENABLED = True PYTHON_INSTALL_ENABLED = True else: print("ERROR: Invalid command line option '%s'" % opt) @@ -844,6 +847,9 @@ def is_ml_enabled(): def is_dotnet_enabled(): return DOTNET_ENABLED +def is_python_enabled(): + return PYTHON_ENABLED + def is_python_install_enabled(): return PYTHON_INSTALL_ENABLED @@ -1382,6 +1388,32 @@ class DLLComponent(Component): shutil.copy('%s.a' % os.path.join(build_path, self.dll_name), '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) +class PythonComponent(Component): + def __init__(self, name, libz3Component): + assert isinstance(libz3Component, DLLComponent) + global PYTHON_ENABLED + Component.__init__(self, name, None, []) + self.libz3Component = libz3Component + + def main_component(self): + return False + + def mk_win_dist(self, build_path, dist_path): + if not is_python_enabled(): + return + + src = os.path.join(build_path, 'python', 'z3') + dst = os.path.join(dist_path, INSTALL_BIN_DIR, 'python', 'z3') + if os.path.exists(dst): + shutil.rmtree(dst) + shutil.copytree(src, dst) + + def mk_unix_dist(self, build_path, dist_path): + self.mk_win_dist(build_path, dist_path) + + def mk_makefile(self, out): + return + class PythonInstallComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) @@ -1484,6 +1516,7 @@ class PythonInstallComponent(Component): os.path.join('python', 'z3', '*.pyc'), os.path.join(self.pythonPkgDir,'z3'), in_prefix=self.in_prefix_install) + if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR) @@ -2173,6 +2206,15 @@ class PythonExampleComponent(ExampleComponent): print("Copied Z3Py example '%s' to '%s'" % (py, os.path.join(BUILD_DIR, 'python'))) out.write('_ex_%s: \n\n' % self.name) + def mk_win_dist(self, build_path, dist_path): + full = os.path.join(EXAMPLE_DIR, self.path) + py = 'example.py' + shutil.copyfile(os.path.join(full, py), + os.path.join(dist_path, INSTALL_BIN_DIR, 'python', py)) + + def mk_unix_dist(self, build_path, dist_path): + self.mk_win_dist(build_path, dist_path) + def reg_component(name, c): global _Id, _Components, _ComponentNames, _Name2Component @@ -2213,6 +2255,10 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps) reg_component(name, c) +def add_python(libz3Component): + name = 'python' + reg_component(name, PythonComponent(name, libz3Component)) + def add_python_install(libz3Component): name = 'python_install' reg_component(name, PythonInstallComponent(name, libz3Component)) @@ -3230,11 +3276,6 @@ def mk_vs_proj_dll(name, components): def mk_win_dist(build_path, dist_path): for c in get_components(): c.mk_win_dist(build_path, dist_path) - # Add Z3Py to bin directory - print("Adding to %s\n" % dist_path) - for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)): - shutil.copy(os.path.join(build_path, pyc), - os.path.join(dist_path, INSTALL_BIN_DIR, pyc)) def mk_unix_dist(build_path, dist_path): for c in get_components(): diff --git a/scripts/mk_win_dist.py b/scripts/mk_win_dist.py index 145e356fb..65d780f0d 100644 --- a/scripts/mk_win_dist.py +++ b/scripts/mk_win_dist.py @@ -28,6 +28,7 @@ DOTNET_ENABLED=True DOTNET_KEY_FILE=None JAVA_ENABLED=True GIT_HASH=False +PYTHON_ENABLED=True def set_verbose(flag): global VERBOSE @@ -60,12 +61,13 @@ def display_help(): print(" --nodotnet do not include .NET bindings in the binary distribution files.") print(" --dotnet-key= sign the .NET assembly with the private key in .") print(" --nojava do not include Java bindings in the binary distribution files.") + print(" --nopython do not include Python bindings in the binary distribution files.") print(" --githash include git hash in the Zip file.") exit(0) # Parse configuration option for mk_make script def parse_options(): - global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE + global FORCE_MK, JAVA_ENABLED, GIT_HASH, DOTNET_ENABLED, DOTNET_KEY_FILE, PYTHON_ENABLED path = BUILD_DIR options, remainder = getopt.gnu_getopt(sys.argv[1:], 'b:hsf', ['build=', 'help', @@ -74,7 +76,8 @@ def parse_options(): 'nojava', 'nodotnet', 'dotnet-key=', - 'githash' + 'githash', + 'nopython' ]) for opt, arg in options: if opt in ('-b', '--build'): @@ -89,6 +92,8 @@ def parse_options(): FORCE_MK = True elif opt == '--nodotnet': DOTNET_ENABLED = False + elif opt == '--nopython': + PYTHON_ENABLED = False elif opt == '--dotnet-key': DOTNET_KEY_FILE = arg elif opt == '--nojava': @@ -118,6 +123,8 @@ def mk_build_dir(path, x64): if GIT_HASH: opts.append('--githash=%s' % mk_util.git_hash()) opts.append('--git-describe') + if PYTHON_ENABLED: + opts.append('--python') if subprocess.call(opts) != 0: raise MKException("Failed to generate build directory at '%s'" % path) @@ -192,6 +199,7 @@ def mk_dist_dir_core(x64): mk_util.DOTNET_ENABLED = DOTNET_ENABLED mk_util.DOTNET_KEY_FILE = DOTNET_KEY_FILE mk_util.JAVA_ENABLED = JAVA_ENABLED + mk_util.PYTHON_ENABLED = PYTHON_ENABLED mk_win_dist(build_path, dist_path) if is_verbose(): print("Generated %s distribution folder at '%s'" % (platform, dist_path))