diff --git a/python/README-linux.txt b/python/README-linux.txt new file mode 100644 index 000000000..3f7028f18 --- /dev/null +++ b/python/README-linux.txt @@ -0,0 +1,15 @@ +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: + + from z3 import * + +Learn more about Z3Py at: +http://rise4fun.com/Z3Py/tutorial/guide + + + diff --git a/python/README-osx.txt b/python/README-osx.txt new file mode 100644 index 000000000..3dfcd2ad9 --- /dev/null +++ b/python/README-osx.txt @@ -0,0 +1,12 @@ +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: + + from z3 import * + +Learn more about Z3Py at: +http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/README-win.txt b/python/README-win.txt new file mode 100644 index 000000000..7ff47a2e4 --- /dev/null +++ b/python/README-win.txt @@ -0,0 +1,16 @@ +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 new file mode 100644 index 000000000..04791f5f7 --- /dev/null +++ b/python/README.txt @@ -0,0 +1,5 @@ +To run the test script execute: +python example.py + +Learn more about Z3Py at: +http://rise4fun.com/Z3Py/tutorial/guide diff --git a/python/example.py b/python/example.py new file mode 100644 index 000000000..a8a764a4d --- /dev/null +++ b/python/example.py @@ -0,0 +1,8 @@ +from z3 import * + +x = Real('x') +y = Real('y') +s = Solver() +s.add(x + y > 5, x > 1, y > 1) +print s.check() +print s.model()