Z3Py extra files

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

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
+
+
+

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

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

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

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()