mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

Working on python bindings

Browse source 
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2012-10-09 06:39:17 -07:00
parent 39846d3527
commit bd1729239b
3 changed files with 42 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

12
Makefile.in
View file

@ -444,12 +444,12 @@ checkgmake:
# #
################################ ################################
install: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).so $(BIN_DIR)/lib$(Z3).a install: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(BIN_DIR)/lib$(Z3).a
@mkdir -p $(PREFIX)/bin @mkdir -p $(PREFIX)/bin
@mkdir -p $(PREFIX)/lib @mkdir -p $(PREFIX)/lib
@mkdir -p $(PREFIX)/include @mkdir -p $(PREFIX)/include
@cp $(BIN_DIR)/$(Z3) $(PREFIX)/bin @cp $(BIN_DIR)/$(Z3) $(PREFIX)/bin
@cp $(BIN_DIR)/lib$(Z3).so $(PREFIX)/lib @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PREFIX)/lib
@cp $(BIN_DIR)/lib$(Z3).a $(PREFIX)/lib @cp $(BIN_DIR)/lib$(Z3).a $(PREFIX)/lib
@cp lib/z3_api.h $(PREFIX)/include @cp lib/z3_api.h $(PREFIX)/include
@cp lib/z3.h $(PREFIX)/include @cp lib/z3.h $(PREFIX)/include
@ -459,7 +459,7 @@ install: $(BIN_DIR)/$(Z3) $(BIN_DIR)/lib$(Z3).so $(BIN_DIR)/lib$(Z3).a
uninstall: uninstall:
@rm -f $(PREFIX)/bin/$(Z3) @rm -f $(PREFIX)/bin/$(Z3)
@rm -f $(PREFIX)/lib/lib$(Z3).so @rm -f $(PREFIX)/lib/lib$(Z3).@SO_EXT@
@rm -f $(PREFIX)/lib/lib$(Z3).a @rm -f $(PREFIX)/lib/lib$(Z3).a
@rm -f $(PREFIX)/include/z3_api.h @rm -f $(PREFIX)/include/z3_api.h
@rm -f $(PREFIX)/include/z3.h @rm -f $(PREFIX)/include/z3.h
@ -467,7 +467,7 @@ uninstall:
@rm -f $(PREFIX)/include/z3_macros.h @rm -f $(PREFIX)/include/z3_macros.h
@rm -f $(PREFIX)/include/z3++.h @rm -f $(PREFIX)/include/z3++.h
install-python: $(BIN_DIR)/lib$(Z3).so install-python: $(BIN_DIR)/lib$(Z3).@SO_EXT@
@if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @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)." @echo "Installing Python bindings at $(PYTHON_PACKAGE_DIR)."
@cp python/z3.py $(PYTHON_PACKAGE_DIR) @cp python/z3.py $(PYTHON_PACKAGE_DIR)
@ -476,7 +476,7 @@ install-python: $(BIN_DIR)/lib$(Z3).so
@cp python/z3consts.py $(PYTHON_PACKAGE_DIR) @cp python/z3consts.py $(PYTHON_PACKAGE_DIR)
@cp python/z3tactics.py $(PYTHON_PACKAGE_DIR) @cp python/z3tactics.py $(PYTHON_PACKAGE_DIR)
@cp python/z3printer.py $(PYTHON_PACKAGE_DIR) @cp python/z3printer.py $(PYTHON_PACKAGE_DIR)
@cp $(BIN_DIR)/lib$(Z3).so $(PYTHON_PACKAGE_DIR) @cp $(BIN_DIR)/lib$(Z3).@SO_EXT@ $(PYTHON_PACKAGE_DIR)
uninstall-python: uninstall-python:
@if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi @if test $(HAS_PYTHON) -eq 0; then echo "Python is not available in your system."; exit 1; fi
@ -487,4 +487,4 @@ uninstall-python:
@rm -f $(PYTHON_PACKAGE_DIR)/z3consts.py @rm -f $(PYTHON_PACKAGE_DIR)/z3consts.py
@rm -f $(PYTHON_PACKAGE_DIR)/z3tactics.py @rm -f $(PYTHON_PACKAGE_DIR)/z3tactics.py
@rm -f $(PYTHON_PACKAGE_DIR)/z3printer.py @rm -f $(PYTHON_PACKAGE_DIR)/z3printer.py
@rm -f $(PYTHON_PACKAGE_DIR)/$(BIN_DIR)/lib$(Z3).so @rm -f $(PYTHON_PACKAGE_DIR)/$(BIN_DIR)/lib$(Z3).@SO_EXT@

25
python/README-linux.txt
View file

@ -1,15 +1,26 @@
The script exec.sh sets PYTHONPATH, and executes 'python example.py'.
To create scripts using Z3Py, the Z3 python directory must be 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)
In your Python application you should include: In your Python application you should include:
from z3 import * 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: Learn more about Z3Py at:
http://rise4fun.com/Z3Py/tutorial/guide http://rise4fun.com/Z3Py/tutorial/guide

24
python/README-osx.txt
View file

@ -1,12 +1,24 @@
The script exec.sh sets PYTHONPATH, and executes 'python example.py'.
To create scripts using Z3Py, the Z3 python directory must be 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)
In your Python application you should include: In your Python application you should include:
from z3 import * 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: Learn more about Z3Py at:
http://rise4fun.com/Z3Py/tutorial/guide http://rise4fun.com/Z3Py/tutorial/guide