diff options
Diffstat (limited to 'rba.tool.core/lib/z3/python/example.py')
-rw-r--r-- | rba.tool.core/lib/z3/python/example.py | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/rba.tool.core/lib/z3/python/example.py b/rba.tool.core/lib/z3/python/example.py new file mode 100644 index 0000000..a176685 --- /dev/null +++ b/rba.tool.core/lib/z3/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 OSX: +# 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()) |