1 files changed, 36 insertions, 0 deletions
diff --git a/rba.tool.editor.endpoint/lib/linux/z3/bin/python/example.py b/rba.tool.editor.endpoint/lib/linux/z3/bin/python/example.py
new file mode 100644
index 0000000..0ae4935
--- /dev/null
+++ b/rba.tool.editor.endpoint/lib/linux/z3/bin/python/example.py
@@ -0,0 +1,36 @@
+# 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 macOS:
+# export DYLD_LIBRARY_PATH=$DYLD_LIBRARY_PATH:MYZ3/bin
+# export PYTHONPATH=MYZ3/bin/python
+# python example.py
+
+
+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())