mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

python bindings: add core functions with _bytes suffix that do not decode strings

Browse source
This commit is contained in:
Audrey Dutcher 2019-02-18 23:59:27 -07:00
parent 591abead4b
commit c2cb2c9fad
1 changed files with 27 additions and 20 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
scripts/update_api.py
View file

@ -338,11 +338,19 @@ def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handl
""") """)
for sig in _API2PY: for sig in _API2PY:
mk_py_wrapper_single(sig)
if sig[1] == STRING:
mk_py_wrapper_single(sig, decode_string=False)
def mk_py_wrapper_single(sig, decode_string=True):
name = sig[0] name = sig[0]
result = sig[1] result = sig[1]
params = sig[2] params = sig[2]
num = len(params) num = len(params)
core_py.write("def %s(" % name) def_name = name
if not decode_string:
def_name += '_bytes'
core_py.write("def %s(" % def_name)
display_args(num) display_args(num)
comma = ", " if num != 0 else "" comma = ", " if num != 0 else ""
core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name)) core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name))
@ -352,12 +360,11 @@ def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handl
core_py.write(")\n") core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped: if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped:
core_py.write(" _elems.Check(a0)\n") core_py.write(" _elems.Check(a0)\n")
if result == STRING: if result == STRING and decode_string:
core_py.write(" return _to_pystr(r)\n") core_py.write(" return _to_pystr(r)\n")
elif result != VOID: elif result != VOID:
core_py.write(" return r\n") core_py.write(" return r\n")
core_py.write("\n") core_py.write("\n")
core_py
## .NET API native interface ## .NET API native interface