diff options
author | 2021-08-03 18:42:39 +0900 | |
---|---|---|
committer | 2021-08-06 19:32:38 +0900 | |
commit | be4f78978faba3d3ceb88df02a7f93a2e09ff1e0 (patch) | |
tree | 1f3f1a96251ac4f655c8a96fc33d5d4ee779cd06 /rba.tool.editor.endpoint/lib/windows/z3/python/example.py | |
parent | 71ca7c6cab863767ef30c8bd05b2bbfda8731cb5 (diff) |
Initial commit
Bug-AGL: SPEC-4033
Signed-off-by: Kenji Hosokawa <khosokawa@jp.adit-jv.com>
Diffstat (limited to 'rba.tool.editor.endpoint/lib/windows/z3/python/example.py')
-rw-r--r-- | rba.tool.editor.endpoint/lib/windows/z3/python/example.py | 36 |
1 files changed, 36 insertions, 0 deletions
diff --git a/rba.tool.editor.endpoint/lib/windows/z3/python/example.py b/rba.tool.editor.endpoint/lib/windows/z3/python/example.py new file mode 100644 index 0000000..a176685 --- /dev/null +++ b/rba.tool.editor.endpoint/lib/windows/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()) |