From 44a98920d17b46a8e9e9d7b016bb19c303cdc109 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 11 Oct 2012 21:34:36 -0700 Subject: [PATCH] improved z3py installation Signed-off-by: Leonardo de Moura --- Makefile.in | 4 ++-- dll/z3.def | 8 ++++---- dll/z3_dbg.def | 8 ++++---- lib/api.py | 5 ++--- python/README-linux.txt | 26 -------------------------- python/README-osx.txt | 24 ------------------------ python/README-win.txt | 16 ---------------- python/README.txt | 23 +++++++++++++++++++---- python/exec-linux.sh | 2 -- python/exec-osx.sh | 2 -- python/run-linux.sh | 2 -- python/run-osx.sh | 2 -- python/run.sh | 2 -- python/z3core.py | 5 ++--- 14 files changed, 33 insertions(+), 96 deletions(-) delete mode 100644 python/README-linux.txt delete mode 100644 python/README-osx.txt delete mode 100644 python/README-win.txt delete mode 100644 python/exec-linux.sh delete mode 100644 python/exec-osx.sh delete mode 100644 python/run-linux.sh delete mode 100644 python/run-osx.sh delete mode 100644 python/run.sh diff --git a/Makefile.in b/Makefile.in index a24bb823d..fd4366d13 100644 --- a/Makefile.in +++ b/Makefile.in @@ -350,7 +350,7 @@ uninstall: @rm -f $(PREFIX)/include/z3_macros.h @rm -f $(PREFIX)/include/z3++.h -install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@ +install-z3py: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @echo "Installing Python bindings at $(PYTHON_PACKAGE_DIR)." @$(PYTHON) python/example.py > /dev/null @@ -363,7 +363,7 @@ install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@ @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR) @if python python/z3test.py; then echo "Z3Py was successfully installed."; else echo "Failed to execute Z3Py regressions..."; exit 1; fi -uninstall-python: +uninstall-z3py: @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @echo "Uninstalling Python bindings from $(PYTHON_PACKAGE_DIR)." @rm -f $(PYTHON_PACKAGE_DIR)/z3.pyc diff --git a/dll/z3.def b/dll/z3.def index c663ed5c4..d56875d92 100644 --- a/dll/z3.def +++ b/dll/z3.def @@ -232,10 +232,10 @@ EXPORTS Z3_get_quantifier_pattern_ast @230 Z3_get_quantifier_num_no_patterns @231 Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_bound_name @233 - Z3_get_quantifier_bound_sort @234 - Z3_get_quantifier_body @235 - Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_num_bound @233 + Z3_get_quantifier_bound_name @234 + Z3_get_quantifier_bound_sort @235 + Z3_get_quantifier_body @236 Z3_simplify @237 Z3_simplify_ex @238 Z3_simplify_get_help @239 diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def index 0d70389ee..0c830c94e 100644 --- a/dll/z3_dbg.def +++ b/dll/z3_dbg.def @@ -232,10 +232,10 @@ EXPORTS Z3_get_quantifier_pattern_ast @230 Z3_get_quantifier_num_no_patterns @231 Z3_get_quantifier_no_pattern_ast @232 - Z3_get_quantifier_bound_name @233 - Z3_get_quantifier_bound_sort @234 - Z3_get_quantifier_body @235 - Z3_get_quantifier_num_bound @236 + Z3_get_quantifier_num_bound @233 + Z3_get_quantifier_bound_name @234 + Z3_get_quantifier_bound_sort @235 + Z3_get_quantifier_body @236 Z3_simplify @237 Z3_simplify_ex @238 Z3_simplify_get_help @239 diff --git a/lib/api.py b/lib/api.py index 1382a9a18..71449f43b 100644 --- a/lib/api.py +++ b/lib/api.py @@ -57,10 +57,9 @@ def _find_lib(): _dir = os.path.dirname(os.path.abspath(__file__)) libs = ['z3.dll', 'libz3.so', 'libz3.dylib'] if sys.maxsize > 2**32: - winlibdir = 'x64' + locs = [_dir, '%s%s..%sx64%sexternal' % (_dir, os.sep, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] else: - winlibdir = 'bin' - locs = [_dir, '%s%s..%s%s' % (_dir, os.sep, os.sep, winlibdir), '%s%s..%slib' % (_dir, os.sep, os.sep), '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] + locs = [_dir, '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] for loc in locs: for lib in libs: f = '%s%s%s' % (loc, os.sep, lib) diff --git a/python/README-linux.txt b/python/README-linux.txt deleted file mode 100644 index 037e609cc..000000000 --- a/python/README-linux.txt +++ /dev/null @@ -1,26 +0,0 @@ -In your Python application you should include: - - from z3 import * - -Installing the Z3 Python bindings - -Option 1: Install Z3 Python bindings in your python distribution ----------------------------------------------------------------- - -To install the Z3 python bindings in your system, use - sudo make install-python -in the Z3 root directory. -After installing the Z3 python bindings, you can try the example application - python example.py - -Option 2: Set PYTHONPATH ------------------------- - -You may also use Z3Py by including this directory in your PYTHONPATH. -Z3Py searches for libz3.so in set of predefined places that includes the directory where Z3Py is stored. -You may also manually initialize Z3Py using the command z3.init(path-to-libz3.so) - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide - - diff --git a/python/README-osx.txt b/python/README-osx.txt deleted file mode 100644 index b3fd134aa..000000000 --- a/python/README-osx.txt +++ /dev/null @@ -1,24 +0,0 @@ -In your Python application you should include: - - from z3 import * - -Installing the Z3 Python bindings - -Option 1: Install Z3 Python bindings in your python distribution ----------------------------------------------------------------- - -To install the Z3 python bindings in your system, use - sudo make install-python -in the Z3 root directory. -After installing the Z3 python bindings, you can try the example application - python example.py - -Option 2: Set PYTHONPATH ------------------------- - -You may also use Z3Py by including this directory in your PYTHONPATH. -Z3Py searches for libz3.dylib in set of predefined places that includes the directory where Z3Py is stored. -You may also manually initialize Z3Py using the command z3.init(path-to-libz3.dylib) - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/README-win.txt b/python/README-win.txt deleted file mode 100644 index 7ff47a2e4..000000000 --- a/python/README-win.txt +++ /dev/null @@ -1,16 +0,0 @@ -To run the test script execute: -python example.py - -To create scripts using Z3Py, the Z3 python directory must be in your PYTHONPATH. -If you copy the z3*.py files to a different directory, you must also copy the z3.dll. -Remark: if you are using python 32-bit, you must copy the z3.dll in the bin directory. -If you are using python 64-bit, you must copy the z3.dll in the x64 directory. - -You may also manually initialize Z3Py using the command z3.init(path-to-z3.dll) - -In your Python application you should include: - - from z3 import * - -Learn more about Z3Py at: -http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/README.txt b/python/README.txt index 04791f5f7..9831c6fc6 100644 --- a/python/README.txt +++ b/python/README.txt @@ -1,5 +1,20 @@ -To run the test script execute: -python example.py - -Learn more about Z3Py at: +You can learn more about Z3Py at: http://rise4fun.com/Z3Py/tutorial/guide + +On Windows, you must build Z3 before using Z3Py. +To build Z3, you should executed the following command +in the Z3 root directory at the Visual Studio Command Prompt + + msbuild /p:configuration=external + +If you are using a 64-bit Python interpreter, you should use + + msbuild /p:configuration=external /p:platform=x64 + + +On Linux and OSX, you must install Z3Py, before trying example.py. +To install Z3Py on Linux and OSX, you should execute the following +command in the Z3 root directory + + sudo make install-z3py + diff --git a/python/exec-linux.sh b/python/exec-linux.sh deleted file mode 100644 index 6a775a767..000000000 --- a/python/exec-linux.sh +++ /dev/null @@ -1,2 +0,0 @@ -export PYTHONPATH=../../python:$PYTHONPATH -python example.py \ No newline at end of file diff --git a/python/exec-osx.sh b/python/exec-osx.sh deleted file mode 100644 index c32d0884f..000000000 --- a/python/exec-osx.sh +++ /dev/null @@ -1,2 +0,0 @@ -export PYTHONPATH=../../python:$PYTHONPATH -python example.py diff --git a/python/run-linux.sh b/python/run-linux.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run-linux.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/run-osx.sh b/python/run-osx.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run-osx.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/run.sh b/python/run.sh deleted file mode 100644 index dc0e24d2c..000000000 --- a/python/run.sh +++ /dev/null @@ -1,2 +0,0 @@ -export LD_LIBRARY_PATH=. -python example.py diff --git a/python/z3core.py b/python/z3core.py index 90894e9ff..588e9fa86 100644 --- a/python/z3core.py +++ b/python/z3core.py @@ -8,10 +8,9 @@ def _find_lib(): _dir = os.path.dirname(os.path.abspath(__file__)) libs = ['z3.dll', 'libz3.so', 'libz3.dylib'] if sys.maxsize > 2**32: - winlibdir = 'x64' + locs = [_dir, '%s%s..%sx64%sexternal' % (_dir, os.sep, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] else: - winlibdir = 'bin' - locs = [_dir, '%s%s..%s%s' % (_dir, os.sep, os.sep, winlibdir), '%s%s..%slib' % (_dir, os.sep, os.sep), '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] + locs = [_dir, '%s%s..%sexternal' % (_dir, os.sep, os.sep), '%s%s..%sbin%sexternal' % (_dir, os.sep, os.sep, os.sep)] for loc in locs: for lib in libs: f = '%s%s%s' % (loc, os.sep, lib)