import argparse
import logging
import re
import os
import sys
VERBOSE = True
def is_verbose():
return VERBOSE
IN = 0
OUT = 1
INOUT = 2
IN_ARRAY = 3
OUT_ARRAY = 4
INOUT_ARRAY = 5
OUT_MANAGED_ARRAY = 6
FN_PTR = 7
VOID = 0
VOID_PTR = 1
INT = 2
UINT = 3
INT64 = 4
UINT64 = 5
STRING = 6
STRING_PTR = 7
BOOL = 8
SYMBOL = 9
PRINT_MODE = 10
ERROR_CODE = 11
DOUBLE = 12
FLOAT = 13
CHAR = 14
CHAR_PTR = 15
LBOOL = 16
FIRST_FN_ID = 50
FIRST_OBJ_ID = 100
def is_obj(ty):
return ty >= FIRST_OBJ_ID
def is_fn(ty):
return FIRST_FN_ID <= ty and ty < FIRST_OBJ_ID
Type2Str = { VOID : 'void', VOID_PTR : 'void*', INT : 'int', UINT : 'unsigned', INT64 : 'int64_t', UINT64 : 'uint64_t', DOUBLE : 'double',
FLOAT : 'float', STRING : 'Z3_string', STRING_PTR : 'Z3_string_ptr', BOOL : 'bool', SYMBOL : 'Z3_symbol',
PRINT_MODE : 'Z3_ast_print_mode', ERROR_CODE : 'Z3_error_code', CHAR: 'char', CHAR_PTR: 'Z3_char_ptr', LBOOL : 'Z3_lbool'
}
Type2PyStr = { VOID_PTR : 'ctypes.c_void_p', INT : 'ctypes.c_int', UINT : 'ctypes.c_uint', INT64 : 'ctypes.c_longlong',
UINT64 : 'ctypes.c_ulonglong', DOUBLE : 'ctypes.c_double', FLOAT : 'ctypes.c_float',
STRING : 'ctypes.c_char_p', STRING_PTR : 'ctypes.POINTER(ctypes.c_char_p)', BOOL : 'ctypes.c_bool', SYMBOL : 'Symbol',
PRINT_MODE : 'ctypes.c_uint', ERROR_CODE : 'ctypes.c_uint', CHAR : 'ctypes.c_char', CHAR_PTR: 'ctypes.POINTER(ctypes.c_char)', LBOOL : 'ctypes.c_int'
}
Type2Dotnet = { VOID : 'void', VOID_PTR : 'IntPtr', INT : 'int', UINT : 'uint', INT64 : 'Int64', UINT64 : 'UInt64', DOUBLE : 'double',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'byte**', BOOL : 'byte', SYMBOL : 'IntPtr',
PRINT_MODE : 'uint', ERROR_CODE : 'uint', CHAR : 'char', CHAR_PTR : 'IntPtr', LBOOL : 'int' }
Type2ML = { VOID : 'unit', VOID_PTR : 'ptr', INT : 'int', UINT : 'int', INT64 : 'int64', UINT64 : 'int64', DOUBLE : 'float',
FLOAT : 'float', STRING : 'string', STRING_PTR : 'char**',
BOOL : 'bool', SYMBOL : 'z3_symbol', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'string', LBOOL : 'int' }
Closures = []
class APITypes:
def __init__(self):
self.next_type_id = FIRST_OBJ_ID
self.next_fntype_id = FIRST_FN_ID
def def_Type(self, var, c_type, py_type):
id = self.next_type_id
exec('%s = %s' % (var, id), globals())
Type2Str[id] = c_type
Type2PyStr[id] = py_type
self.next_type_id += 1
def def_Types(self, api_files):
global Closures
pat1 = re.compile(r" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*")
pat2 = re.compile(r"Z3_DECLARE_CLOSURE\((.*),(.*), \((.*)\)\)")
for api_file in api_files:
with open(api_file, 'r') as api:
for line in api:
m = pat1.match(line)
if m:
self.def_Type(m.group(1), m.group(2), m.group(3))
continue
m = pat2.match(line)
if m:
self.fun_Type(m.group(1))
Closures += [(m.group(1), m.group(2), m.group(3))]
continue
for k in Type2Str:
v = Type2Str[k]
if is_obj(k) or is_fn(k):
Type2Dotnet[k] = v
Type2ML[k] = v.lower()
def fun_Type(self, var):
id = self.next_fntype_id
exec('%s = %s' % (var, id), globals())
Type2Str[id] = var
Type2PyStr[id] = var
self.next_fntype_id += 1
def type2str(ty):
global Type2Str
return Type2Str[ty]
def type2pystr(ty):
global Type2PyStr
return Type2PyStr[ty]
def type2dotnet(ty):
global Type2Dotnet
return Type2Dotnet[ty]
def type2ml(ty):
global Type2ML
q = Type2ML[ty]
if q[0:3] == 'z3_':
return q[3:]
else:
return q;
def _in(ty):
return (IN, ty)
def _in_array(sz, ty):
return (IN_ARRAY, ty, sz)
def _fnptr(ty):
return (FN_PTR, ty)
def _out(ty):
return (OUT, ty)
def _out_array(sz, ty):
return (OUT_ARRAY, ty, sz, sz)
def _out_array2(cap, sz, ty):
return (OUT_ARRAY, ty, cap, sz)
def _inout_array(sz, ty):
return (INOUT_ARRAY, ty, sz, sz)
def _out_managed_array(sz,ty):
return (OUT_MANAGED_ARRAY, ty, 0, sz)
def param_kind(p):
return p[0]
def param_type(p):
return p[1]
def param_array_capacity_pos(p):
return p[2]
def param_array_size_pos(p):
return p[3]
def param2str(p):
if param_kind(p) == IN_ARRAY:
return "%s const *" % (type2str(param_type(p)))
elif param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY:
return "%s*" % (type2str(param_type(p)))
elif param_kind(p) == OUT:
return "%s*" % (type2str(param_type(p)))
elif param_kind(p) == FN_PTR:
return "%s*" % (type2str(param_type(p)))
else:
return type2str(param_type(p))
def param2dotnet(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == STRING:
return "out IntPtr"
else:
return "[In, Out] ref %s" % type2dotnet(param_type(p))
elif k == IN_ARRAY:
return "[In] %s[]" % type2dotnet(param_type(p))
elif k == INOUT_ARRAY:
return "[In, Out] %s[]" % type2dotnet(param_type(p))
elif k == OUT_ARRAY:
return "[Out] %s[]" % type2dotnet(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "[Out] out %s[]" % type2dotnet(param_type(p))
else:
return type2dotnet(param_type(p))
def param2pystr(p):
if param_kind(p) == IN_ARRAY or param_kind(p) == OUT_ARRAY or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT:
return "ctypes.POINTER(%s)" % type2pystr(param_type(p))
else:
return type2pystr(param_type(p))
def param2ml(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "int"
elif param_type(p) == INT64 or param_type(p) == UINT64:
return "int64"
elif param_type(p) == STRING:
return "string"
else:
return "ptr"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s list" % type2ml(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "%s list" % type2ml(param_type(p))
else:
return type2ml(param_type(p))
_API2PY = []
def mk_py_binding(name, result, params):
global core_py
global _API2PY
_API2PY.append((name, result, params))
if result != VOID:
core_py.write("_lib.%s.restype = %s\n" % (name, type2pystr(result)))
core_py.write("_lib.%s.argtypes = [" % name)
first = True
for p in params:
if first:
first = False
else:
core_py.write(", ")
core_py.write(param2pystr(p))
core_py.write("]\n")
def extra_API(name, result, params):
mk_py_binding(name, result, params)
reg_dotnet(name, result, params)
def display_args(num):
for i in range(num):
if i > 0:
core_py.write(", ")
core_py.write("a%s" % i)
def display_args_to_z3(params):
i = 0
for p in params:
if i > 0:
core_py.write(", ")
if param_type(p) == STRING:
core_py.write("_str_to_bytes(a%s)" % i)
else:
core_py.write("a%s" % i)
i = i + 1
NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ]
Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
Unchecked = frozenset([ 'Z3_dec_ref', 'Z3_params_dec_ref', 'Z3_model_dec_ref',
'Z3_func_interp_dec_ref', 'Z3_func_entry_dec_ref',
'Z3_goal_dec_ref', 'Z3_tactic_dec_ref', 'Z3_simplifier_dec_ref', 'Z3_probe_dec_ref',
'Z3_fixedpoint_dec_ref', 'Z3_param_descrs_dec_ref',
'Z3_ast_vector_dec_ref', 'Z3_ast_map_dec_ref',
'Z3_apply_result_dec_ref', 'Z3_solver_dec_ref',
'Z3_stats_dec_ref', 'Z3_optimize_dec_ref'])
def mk_py_wrappers():
core_py.write("""
class Elementaries:
def __init__(self, f):
self.f = f
self.get_error_code = _lib.Z3_get_error_code
self.get_error_message = _lib.Z3_get_error_msg
self.OK = Z3_OK
self.Exception = Z3Exception
def Check(self, ctx):
err = self.get_error_code(ctx)
if err != self.OK:
raise self.Exception(self.get_error_message(ctx, err))
def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handler)):
ceh = _error_handler_type(hndlr)
_elems.f(ctx, ceh)
_elems.Check(ctx)
return ceh
def Z3_solver_register_on_clause(ctx, s, user_ctx, on_clause_eh, _elems = Elementaries(_lib.Z3_solver_register_on_clause)):
_elems.f(ctx, s, user_ctx, on_clause_eh)
_elems.Check(ctx)
def Z3_solver_propagate_init(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh, _elems = Elementaries(_lib.Z3_solver_propagate_init)):
_elems.f(ctx, s, user_ctx, push_eh, pop_eh, fresh_eh)
_elems.Check(ctx)
def Z3_solver_propagate_final(ctx, s, final_eh, _elems = Elementaries(_lib.Z3_solver_propagate_final)):
_elems.f(ctx, s, final_eh)
_elems.Check(ctx)
def Z3_solver_propagate_fixed(ctx, s, fixed_eh, _elems = Elementaries(_lib.Z3_solver_propagate_fixed)):
_elems.f(ctx, s, fixed_eh)
_elems.Check(ctx)
def Z3_solver_propagate_eq(ctx, s, eq_eh, _elems = Elementaries(_lib.Z3_solver_propagate_eq)):
_elems.f(ctx, s, eq_eh)
_elems.Check(ctx)
def Z3_solver_propagate_diseq(ctx, s, diseq_eh, _elems = Elementaries(_lib.Z3_solver_propagate_diseq)):
_elems.f(ctx, s, diseq_eh)
_elems.Check(ctx)
def Z3_optimize_register_model_eh(ctx, o, m, user_ctx, on_model_eh, _elems = Elementaries(_lib.Z3_optimize_register_model_eh)):
_elems.f(ctx, o, m, user_ctx, on_model_eh)
_elems.Check(ctx)
""")
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]
result = sig[1]
params = sig[2]
num = len(params)
def_name = name
if not decode_string:
def_name += '_bytes'
core_py.write("def %s(" % def_name)
display_args(num)
comma = ", " if num != 0 else ""
core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name))
lval = "r = " if result != VOID else ""
core_py.write(" %s_elems.f(" % lval)
display_args_to_z3(params)
core_py.write(")\n")
if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped and not name in Unchecked:
core_py.write(" _elems.Check(a0)\n")
if result == STRING and decode_string:
core_py.write(" return _to_pystr(r)\n")
elif result != VOID:
core_py.write(" return r\n")
core_py.write("\n")
_dotnet_decls = []
def reg_dotnet(name, result, params):
global _dotnet_decls
_dotnet_decls.append((name, result, params))
def mk_dotnet(dotnet):
global Type2Str
dotnet.write('// Automatically generated file\n')
dotnet.write('using System;\n')
dotnet.write('using System.Collections.Generic;\n')
dotnet.write('using System.Text;\n')
dotnet.write('using System.Runtime.InteropServices;\n\n')
dotnet.write('#pragma warning disable 1591\n\n')
dotnet.write('namespace Microsoft.Z3\n')
dotnet.write('{\n')
for k in Type2Str:
v = Type2Str[k]
if is_obj(k):
dotnet.write(' using %s = System.IntPtr;\n' % v)
dotnet.write(' using voidp = System.IntPtr;\n')
dotnet.write('\n')
dotnet.write(' public class Native\n')
dotnet.write(' {\n\n')
for name, ret, sig in Closures:
sig = sig.replace("unsigned const*","uint[]")
sig = sig.replace("void*","voidp").replace("unsigned","uint")
sig = sig.replace("Z3_ast*","ref IntPtr").replace("uint*","ref uint").replace("Z3_lbool*","ref int")
ret = ret.replace("void*","voidp").replace("unsigned","uint")
if "*" in sig or "*" in ret:
continue
dotnet.write(' [UnmanagedFunctionPointer(CallingConvention.Cdecl)]\n')
dotnet.write(' public delegate %s %s(%s);\n' % (ret,name,sig))
dotnet.write(' public class LIB\n')
dotnet.write(' {\n')
dotnet.write(' const string Z3_DLL_NAME = \"libz3\";\n'
' \n')
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' public extern static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1);\n\n')
for name, result, params in _dotnet_decls:
dotnet.write(' [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]\n')
dotnet.write(' ')
if result == STRING:
dotnet.write('public extern static IntPtr %s(' % (name))
else:
dotnet.write('public extern static %s %s(' % (type2dotnet(result), name))
first = True
i = 0
for param in params:
if first:
first = False
else:
dotnet.write(', ')
dotnet.write('%s a%d' % (param2dotnet(param), i))
i = i + 1
dotnet.write(');\n\n')
dotnet.write(' }\n')
def mk_dotnet_wrappers(dotnet):
global Type2Str
dotnet.write("\n")
dotnet.write(" public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) {\n")
dotnet.write(" LIB.Z3_set_error_handler(a0, a1);\n")
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
dotnet.write(" }\n\n")
for name, result, params in _dotnet_decls:
if result == STRING:
dotnet.write(' public static string %s(' % (name))
else:
dotnet.write(' public static %s %s(' % (type2dotnet(result), name))
first = True
i = 0
for param in params:
if first:
first = False
else:
dotnet.write(', ')
dotnet.write('%s a%d' % (param2dotnet(param), i))
i = i + 1
dotnet.write(') {\n')
dotnet.write(' ')
if result == STRING:
dotnet.write('IntPtr r = ')
elif result != VOID:
dotnet.write('%s r = ' % type2dotnet(result))
dotnet.write('LIB.%s(' % (name))
first = True
i = 0
for param in params:
if first:
first = False
else:
dotnet.write(', ')
if param_kind(param) == OUT:
if param_type(param) == STRING:
dotnet.write('out ')
else:
dotnet.write('ref ')
elif param_kind(param) == OUT_MANAGED_ARRAY:
dotnet.write('out ')
dotnet.write('a%d' % i)
i = i + 1
dotnet.write(');\n')
if name not in Unwrapped:
if name in NULLWrapped:
dotnet.write(" if (r == IntPtr.Zero)\n")
dotnet.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked:
dotnet.write(" Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);\n")
dotnet.write(" if (err != Z3_error_code.Z3_OK)\n")
dotnet.write(" throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg(a0, (uint)err)));\n")
if result == STRING:
dotnet.write(" return Marshal.PtrToStringAnsi(r);\n")
elif result != VOID:
dotnet.write(" return r;\n")
dotnet.write(" }\n\n")
dotnet.write(" }\n\n")
dotnet.write("}\n\n")
Type2Java = { VOID : 'void', VOID_PTR : 'long', INT : 'int', UINT : 'int', INT64 : 'long', UINT64 : 'long', DOUBLE : 'double',
FLOAT : 'float', STRING : 'String', STRING_PTR : 'StringPtr',
BOOL : 'boolean', SYMBOL : 'long', PRINT_MODE : 'int', ERROR_CODE : 'int', CHAR : 'char', CHAR_PTR : 'long', LBOOL : 'int' }
Type2JavaW = { VOID : 'void', VOID_PTR : 'jlong', INT : 'jint', UINT : 'jint', INT64 : 'jlong', UINT64 : 'jlong', DOUBLE : 'jdouble',
FLOAT : 'jfloat', STRING : 'jstring', STRING_PTR : 'jobject',
BOOL : 'jboolean', SYMBOL : 'jlong', PRINT_MODE : 'jint', ERROR_CODE : 'jint', CHAR : 'jchar', CHAR_PTR : 'jlong', LBOOL : 'jint'}
def type2java(ty):
global Type2Java
if (ty >= FIRST_FN_ID):
return 'long'
else:
return Type2Java[ty]
def type2javaw(ty):
global Type2JavaW
if (ty >= FIRST_FN_ID):
return 'jlong'
else:
return Type2JavaW[ty]
def param2java(p):
k = param_kind(p)
if k == OUT:
if param_type(p) == INT or param_type(p) == UINT:
return "IntPtr"
elif param_type(p) == INT64 or param_type(p) == UINT64 or param_type(p) == VOID_PTR or param_type(p) >= FIRST_OBJ_ID:
return "LongPtr"
elif param_type(p) == STRING:
return "StringPtr"
elif param_type(p) == BOOL:
return "BoolPtr"
else:
raise ValueError(f"ERROR: unreachable code - unexpected param_type: {param_type(p)}")
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
return "%s[]" % type2java(param_type(p))
elif k == OUT_MANAGED_ARRAY:
if param_type(p) == UINT:
return "UIntArrayPtr"
else:
return "ObjArrayPtr"
elif k == FN_PTR:
return "LongPtr"
else:
return type2java(param_type(p))
def param2javaw(p):
k = param_kind(p)
if k == OUT:
return "jobject"
elif k == IN_ARRAY or k == INOUT_ARRAY or k == OUT_ARRAY:
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return "jintArray"
else:
return "jlongArray"
elif k == OUT_MANAGED_ARRAY:
return "jlong"
else:
return type2javaw(param_type(p))
def java_method_name(name):
result = ''
name = name[3:] n = len(name)
i = 0
while i < n:
if name[i] == '_':
i = i + 1
if i < n:
result += name[i].upper()
else:
result += name[i]
i = i + 1
return result
def java_array_element_type(p):
if param_type(p) == INT or param_type(p) == UINT or param_type(p) == BOOL:
return 'jint'
else:
return 'jlong'
def mk_java(java_src, java_dir, package_name):
java_nativef = os.path.join(java_dir, 'Native.java')
java_wrapperf = os.path.join(java_dir, 'Native.cpp')
java_native = open(java_nativef, 'w')
java_native.write('// Automatically generated file\n')
java_native.write('package %s;\n' % package_name)
java_native.write('import %s.enumerations.*;\n' % package_name)
java_native.write('public final class Native {\n')
java_native.write(' public static class IntPtr { public int value; }\n')
java_native.write(' public static class LongPtr { public long value; }\n')
java_native.write(' public static class StringPtr { public String value; }\n')
java_native.write(' public static class ObjArrayPtr { public long[] value; }\n')
java_native.write(' public static class UIntArrayPtr { public int[] value; }\n')
java_native.write(' public static class BoolPtr { public boolean value; }\n')
java_native.write(' public static native void setInternalErrorHandler(long ctx);\n\n')
java_native.write(' static {\n')
java_native.write(' if (!Boolean.parseBoolean(System.getProperty("z3.skipLibraryLoad"))) {\n')
java_native.write(' try {\n')
java_native.write(' System.loadLibrary("z3java");\n')
java_native.write(' } catch (UnsatisfiedLinkError ex) {\n')
java_native.write(' try {\n')
java_native.write(' System.loadLibrary("libz3java");\n')
java_native.write(' } catch (UnsatisfiedLinkError ex2) {\n')
java_native.write(' throw new UnsatisfiedLinkError(\n')
java_native.write(' "Failed to load z3java native library. "\n')
java_native.write(' + "Tried z3java: " + ex.getMessage() + "; "\n')
java_native.write(' + "Tried libz3java: " + ex2.getMessage() + ". "\n')
java_native.write(' + "Make sure both the JNI library and libz3 are in java.library.path "\n')
java_native.write(' + "or set DYLD_LIBRARY_PATH (macOS) / LD_LIBRARY_PATH (Linux).");\n')
java_native.write(' }\n')
java_native.write(' }\n')
java_native.write(' }\n')
java_native.write(' }\n')
java_native.write("""
public static native long propagateInit(Object o, long ctx, long solver);
public static native void propagateRegisterCreated(Object o, long ctx, long solver);
public static native void propagateRegisterFixed(Object o, long ctx, long solver);
public static native void propagateRegisterEq(Object o, long ctx, long solver);
public static native void propagateRegisterDecide(Object o, long ctx, long solver);
public static native void propagateRegisterFinal(Object o, long ctx, long solver);
public static native void propagateRegisterOnBinding(Object o, long ctx, long solver);
public static native void propagateAdd(Object o, long ctx, long solver, long javainfo, long e);
public static native boolean propagateConsequence(Object o, long ctx, long solver, long javainfo, int num_fixed, long[] fixed, long num_eqs, long[] eq_lhs, long[] eq_rhs, long conseq);
public static native boolean propagateNextSplit(Object o, long ctx, long solver, long javainfo, long e, long idx, int phase);
public static native void propagateDestroy(Object o, long ctx, long solver, long javainfo);
public static native long onClauseInit(Object o, long ctx, long solver);
public static native void onClauseDestroy(long javainfo);
public static abstract class UserPropagatorBase implements AutoCloseable {
protected long ctx;
protected long solver;
protected long javainfo;
public UserPropagatorBase(long _ctx, long _solver) {
ctx = _ctx;
solver = _solver;
javainfo = propagateInit(this, ctx, solver);
}
@Override
public void close() {
Native.propagateDestroy(this, ctx, solver, javainfo);
javainfo = 0;
solver = 0;
ctx = 0;
}
protected final void registerCreated() {
Native.propagateRegisterCreated(this, ctx, solver);
}
protected final void registerFixed() {
Native.propagateRegisterFixed(this, ctx, solver);
}
protected final void registerEq() {
Native.propagateRegisterEq(this, ctx, solver);
}
protected final void registerDecide() {
Native.propagateRegisterDecide(this, ctx, solver);
}
protected final void registerFinal() {
Native.propagateRegisterFinal(this, ctx, solver);
}
protected final void registerOnBinding() {
Native.propagateRegisterOnBinding(this, ctx, solver);
}
protected abstract void pushWrapper();
protected abstract void popWrapper(int number);
protected abstract void finWrapper();
protected abstract void eqWrapper(long lx, long ly);
protected abstract UserPropagatorBase freshWrapper(long lctx);
protected abstract void createdWrapper(long le);
protected abstract void fixedWrapper(long lvar, long lvalue);
protected abstract void decideWrapper(long lvar, int bit, boolean is_pos);
protected abstract boolean onBindingWrapper(long q, long inst);
}
""")
java_native.write('\n')
for name, result, params in _dotnet_decls:
java_native.write(' protected static native %s INTERNAL%s(' % (type2java(result), java_method_name(name)))
first = True
i = 0
for param in params:
if first:
first = False
else:
java_native.write(', ')
java_native.write('%s a%d' % (param2java(param), i))
i = i + 1
java_native.write(');\n')
java_native.write('\n\n')
for name, result, params in _dotnet_decls:
java_native.write(' public static %s %s(' % (type2java(result), java_method_name(name)))
first = True
i = 0
for param in params:
if first:
first = False
else:
java_native.write(', ')
java_native.write('%s a%d' % (param2java(param), i))
i = i + 1
java_native.write(')')
if (len(params) > 0 and param_type(params[0]) == CONTEXT) or name in NULLWrapped:
java_native.write(' throws Z3Exception')
java_native.write('\n')
java_native.write(' {\n')
java_native.write(' ')
if result != VOID:
java_native.write('%s res = ' % type2java(result))
java_native.write('INTERNAL%s(' % (java_method_name(name)))
first = True
i = 0
for param in params:
if first:
first = False
else:
java_native.write(', ')
java_native.write('a%d' % i)
i = i + 1
java_native.write(');\n')
if name not in Unwrapped:
if name in NULLWrapped:
java_native.write(" if (res == 0)\n")
java_native.write(" throw new Z3Exception(\"Object allocation failed.\");\n")
else:
if len(params) > 0 and param_type(params[0]) == CONTEXT and name not in Unchecked:
java_native.write(' Z3_error_code err = Z3_error_code.fromInt(INTERNALgetErrorCode(a0));\n')
java_native.write(' if (err != Z3_error_code.Z3_OK)\n')
java_native.write(' throw new Z3Exception(INTERNALgetErrorMsg(a0, err.toInt()));\n')
if result != VOID:
java_native.write(' return res;\n')
java_native.write(' }\n\n')
java_native.write('}\n')
java_wrapper = open(java_wrapperf, 'w')
pkg_str = package_name.replace('.', '_')
java_wrapper.write("// Automatically generated file\n")
with open(java_src + "/NativeStatic.txt") as ins:
for line in ins:
java_wrapper.write(line)
for name, result, params in _dotnet_decls:
java_wrapper.write('DLL_VIS JNIEXPORT %s JNICALL Java_%s_Native_INTERNAL%s(JNIEnv * jenv, jclass cls' % (type2javaw(result), pkg_str, java_method_name(name)))
i = 0
for param in params:
java_wrapper.write(', ')
java_wrapper.write('%s a%d' % (param2javaw(param), i))
i = i + 1
java_wrapper.write(') {\n')
i = 0
for param in params:
k = param_kind(param)
if k == OUT or k == INOUT:
java_wrapper.write(' %s _a%s;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' %s * _a%s = (%s*) jenv->GetIntArrayElements(a%s, NULL);\n' % (type2str(param_type(param)), i, type2str(param_type(param)), i))
else:
java_wrapper.write(' GETLONGAELEMS(%s, a%s, _a%s);\n' % (type2str(param_type(param)), i, i))
elif k == OUT_ARRAY:
java_wrapper.write(' %s * _a%s = (%s *) malloc(((unsigned)a%s) * sizeof(%s));\n' % (type2str(param_type(param)),
i,
type2str(param_type(param)),
param_array_capacity_pos(param),
type2str(param_type(param))))
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->GetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' GETLONGAREGION(%s, a%s, 0, a%s, _a%s);\n' % (type2str(param_type(param)), i, param_array_capacity_pos(param), i))
elif k == IN and param_type(param) == STRING:
java_wrapper.write(' Z3_string _a%s = (Z3_string) jenv->GetStringUTFChars(a%s, NULL);\n' % (i, i))
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write(' %s * _a%s = 0;\n' % (type2str(param_type(param)), i))
i = i + 1
java_wrapper.write(' ')
if result != VOID:
java_wrapper.write('%s result = ' % type2str(result))
java_wrapper.write('%s(' % name)
i = 0
first = True
for param in params:
if first:
first = False
else:
java_wrapper.write(', ')
k = param_kind(param)
if k == OUT or k == INOUT:
java_wrapper.write('&_a%s' % i)
elif k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
java_wrapper.write('_a%s' % i)
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write('&_a%s' % i)
elif k == IN and param_type(param) == STRING:
java_wrapper.write('_a%s' % i)
else:
java_wrapper.write('(%s)a%i' % (param2str(param), i))
i = i + 1
java_wrapper.write(');\n')
i = 0
for param in params:
k = param_kind(param)
if k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->SetIntArrayRegion(a%s, 0, (jsize)a%s, (jint*)_a%s);\n' % (i, param_array_capacity_pos(param), i))
else:
java_wrapper.write(' SETLONGAREGION(a%s, 0, a%s, _a%s);\n' % (i, param_array_capacity_pos(param), i))
java_wrapper.write(' free(_a%s);\n' % i)
elif k == IN_ARRAY or k == OUT_ARRAY:
if param_type(param) == INT or param_type(param) == UINT or param_type(param) == BOOL:
java_wrapper.write(' jenv->ReleaseIntArrayElements(a%s, (jint*)_a%s, JNI_ABORT);\n' % (i, i))
else:
java_wrapper.write(' RELEASELONGAELEMS(a%s, _a%s);\n' % (i, i))
elif k == OUT or k == INOUT:
if param_type(param) == INT or param_type(param) == UINT:
java_wrapper.write(' {\n')
java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "I");\n')
java_wrapper.write(' jenv->SetIntField(a%s, fid, (jint) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
elif param_type(param) == BOOL:
java_wrapper.write(' {\n')
java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "Z");\n')
java_wrapper.write(' jenv->SetBooleanField(a%s, fid, (jboolean) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
elif param_type(param) == STRING:
java_wrapper.write(' {\n')
java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "Ljava/lang/String;");')
java_wrapper.write(' jstring fval = jenv->NewStringUTF(_a%s);\n' % i)
java_wrapper.write(' jenv->SetObjectField(a%s, fid, fval);\n' % i)
java_wrapper.write(' }\n')
else:
java_wrapper.write(' {\n')
java_wrapper.write(' jclass mc = jenv->GetObjectClass(a%s);\n' % i)
java_wrapper.write(' jfieldID fid = jenv->GetFieldID(mc, "value", "J");\n')
java_wrapper.write(' jenv->SetLongField(a%s, fid, (jlong) _a%s);\n' % (i, i))
java_wrapper.write(' }\n')
elif k == OUT_MANAGED_ARRAY:
java_wrapper.write(' *(jlong**)a%s = (jlong*)_a%s;\n' % (i, i))
elif k == IN and param_type(param) == STRING:
java_wrapper.write(' jenv->ReleaseStringUTFChars(a%s, _a%s);\n' % (i, i));
i = i + 1
if result == STRING:
java_wrapper.write(' return jenv->NewStringUTF(result);\n')
elif result != VOID:
java_wrapper.write(' return (%s) result;\n' % type2javaw(result))
java_wrapper.write('}\n')
java_wrapper.write('#ifdef __cplusplus\n')
java_wrapper.write('}\n')
java_wrapper.write('#endif\n')
if is_verbose():
print("Generated '%s'" % java_nativef)
def mk_log_header(file, name, params):
file.write("void log_%s(" % name)
i = 0
for p in params:
if i > 0:
file.write(", ")
file.write("%s a%s" % (param2str(p), i))
i = i + 1
file.write(")")
def log_param(p):
kind = param_kind(p)
ty = param_type(p)
return is_obj(ty) and (kind == OUT or kind == INOUT or kind == OUT_ARRAY or kind == INOUT_ARRAY)
def log_result(result, params):
for p in params:
if log_param(p):
return True
return False
def mk_log_macro(file, name, params):
file.write("#define LOG_%s(" % name)
i = 0
for p in params:
if i > 0:
file.write(", ")
file.write("_ARG%s" % i)
i = i + 1
file.write(") z3_log_ctx _LOG_CTX; ")
auxs = set()
i = 0
for p in params:
if log_param(p):
kind = param_kind(p)
if kind == OUT_ARRAY or kind == INOUT_ARRAY:
cap = param_array_capacity_pos(p)
if cap not in auxs:
auxs.add(cap)
file.write("unsigned _Z3_UNUSED Z3ARG%s = 0; " % cap)
sz = param_array_size_pos(p)
if sz not in auxs:
auxs.add(sz)
file.write("unsigned * _Z3_UNUSED Z3ARG%s = 0; " % sz)
file.write("%s _Z3_UNUSED Z3ARG%s = 0; " % (param2str(p), i))
i = i + 1
file.write("if (_LOG_CTX.enabled()) { log_%s(" % name)
i = 0
for p in params:
if (i > 0):
file.write(', ')
file.write("_ARG%s" %i)
i = i + 1
file.write("); ")
auxs = set()
i = 0
for p in params:
if log_param(p):
kind = param_kind(p)
if kind == OUT_ARRAY or kind == INOUT_ARRAY:
cap = param_array_capacity_pos(p)
if cap not in auxs:
auxs.add(cap)
file.write("Z3ARG%s = _ARG%s; " % (cap, cap))
sz = param_array_size_pos(p)
if sz not in auxs:
auxs.add(sz)
file.write("Z3ARG%s = _ARG%s; " % (sz, sz))
file.write("Z3ARG%s = _ARG%s; " % (i, i))
i = i + 1
file.write("}\n")
def mk_log_result_macro(file, name, result, params):
file.write("#define RETURN_%s" % name)
if is_obj(result):
file.write("(Z3RES)")
file.write(" ")
file.write("if (_LOG_CTX.enabled()) { ")
if is_obj(result):
file.write("SetR(Z3RES); ")
i = 0
for p in params:
if log_param(p):
kind = param_kind(p)
if kind == OUT_ARRAY or kind == INOUT_ARRAY:
cap = param_array_capacity_pos(p)
sz = param_array_size_pos(p)
if cap == sz:
file.write("for (unsigned i = 0; i < Z3ARG%s; ++i) { SetAO(Z3ARG%s[i], %s, i); } " % (sz, i, i))
else:
file.write("for (unsigned i = 0; Z3ARG%s && i < *Z3ARG%s; ++i) { SetAO(Z3ARG%s[i], %s, i); } " % (sz, sz, i, i))
if kind == OUT or kind == INOUT:
file.write("SetO((Z3ARG%s == 0 ? 0 : *Z3ARG%s), %s); " % (i, i, i))
i = i + 1
file.write("} ")
if is_obj(result):
file.write("return Z3RES\n")
else:
file.write("return\n")
def mk_exec_header(file, name):
file.write("void exec_%s(z3_replayer & in)" % name)
def error(msg):
sys.stderr.write(msg)
exit(-1)
next_id = 0
API2Id = {}
def def_API(name, result, params):
global API2Id, next_id
global log_h, log_c
mk_py_binding(name, result, params)
reg_dotnet(name, result, params)
API2Id[next_id] = name
mk_log_header(log_h, name, params)
log_h.write(';\n')
mk_log_header(log_c, name, params)
log_c.write(' {\n R();\n')
mk_exec_header(exe_c, name)
exe_c.write(' {\n')
i = 0
exe_c.write(" ")
if is_obj(result):
exe_c.write("%s result = " % type2str(result))
exe_c.write("%s(\n " % name)
for p in params:
kind = param_kind(p)
ty = param_type(p)
if (i > 0):
exe_c.write(",\n ")
if kind == IN:
if is_obj(ty):
log_c.write(" P(a%s);\n" % i)
exe_c.write("reinterpret_cast<%s>(in.get_obj(%s))" % (param2str(p), i))
elif ty == STRING:
log_c.write(" S(a%s);\n" % i)
exe_c.write("in.get_str(%s)" % i)
elif ty == SYMBOL:
log_c.write(" Sy(a%s);\n" % i)
exe_c.write("in.get_symbol(%s)" % i)
elif ty == UINT:
log_c.write(" U(a%s);\n" % i)
exe_c.write("in.get_uint(%s)" % i)
elif ty == UINT64:
log_c.write(" U(a%s);\n" % i)
exe_c.write("in.get_uint64(%s)" % i)
elif ty == INT:
log_c.write(" I(a%s);\n" % i)
exe_c.write("in.get_int(%s)" % i)
elif ty == INT64:
log_c.write(" I(a%s);\n" % i)
exe_c.write("in.get_int64(%s)" % i)
elif ty == DOUBLE:
log_c.write(" D(a%s);\n" % i)
exe_c.write("in.get_double(%s)" % i)
elif ty == FLOAT:
log_c.write(" D(a%s);\n" % i)
exe_c.write("in.get_float(%s)" % i)
elif ty == BOOL:
log_c.write(" I(a%s);\n" % i)
exe_c.write("in.get_bool(%s)" % i)
elif ty == VOID_PTR:
log_c.write(" P(0);\n")
exe_c.write("in.get_obj_addr(%s)" % i)
elif ty == LBOOL:
log_c.write(" I(static_cast<signed>(a%s));\n" % i)
exe_c.write("static_cast<%s>(in.get_int(%s))" % (type2str(ty), i))
elif ty == PRINT_MODE or ty == ERROR_CODE:
log_c.write(" U(static_cast<unsigned>(a%s));\n" % i)
exe_c.write("static_cast<%s>(in.get_uint(%s))" % (type2str(ty), i))
else:
error("unsupported parameter for %s, %s" % (name, p))
elif kind == INOUT:
error("unsupported parameter for %s, %s" % (name, p))
elif kind == OUT:
if is_obj(ty):
log_c.write(" P(0);\n")
exe_c.write("reinterpret_cast<%s>(in.get_obj_addr(%s))" % (param2str(p), i))
elif ty == STRING:
log_c.write(" S(\"\");\n")
exe_c.write("in.get_str_addr(%s)" % i)
elif ty == UINT:
log_c.write(" U(0);\n")
exe_c.write("in.get_uint_addr(%s)" % i)
elif ty == UINT64:
log_c.write(" U(0);\n")
exe_c.write("in.get_uint64_addr(%s)" % i)
elif ty == INT:
log_c.write(" I(0);\n")
exe_c.write("in.get_int_addr(%s)" % i)
elif ty == INT64:
log_c.write(" I(0);\n")
exe_c.write("in.get_int64_addr(%s)" % i)
elif ty == BOOL:
log_c.write(" I(0);\n")
exe_c.write("in.get_bool_addr(%s)" % i)
elif ty == VOID_PTR:
log_c.write(" P(0);\n")
exe_c.write("in.get_obj_addr(%s)" % i)
else:
error("unsupported parameter for %s, %s" % (name, p))
elif kind == IN_ARRAY or kind == INOUT_ARRAY:
sz = param_array_capacity_pos(p)
log_c.write(" for (unsigned i = 0; i < a%s; ++i) { " % sz)
if is_obj(ty):
log_c.write("P(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Ap(a%s);\n" % sz)
exe_c.write("reinterpret_cast<%s*>(in.get_obj_array(%s))" % (type2str(ty), i))
elif ty == SYMBOL:
log_c.write("Sy(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Asy(a%s);\n" % sz)
exe_c.write("in.get_symbol_array(%s)" % i)
elif ty == UINT:
log_c.write("U(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)
exe_c.write("in.get_uint_array(%s)" % i)
elif ty == INT:
log_c.write("I(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Ai(a%s);\n" % sz)
exe_c.write("in.get_int_array(%s)" % i)
elif ty == BOOL:
log_c.write("U(a%s[i]);" % i)
log_c.write(" }\n")
log_c.write(" Au(a%s);\n" % sz)
exe_c.write("in.get_bool_array(%s)" % i)
else:
error ("unsupported parameter for %s, %s, %s" % (ty, name, p))
elif kind == OUT_ARRAY:
sz = param_array_capacity_pos(p)
sz_p = params[sz]
sz_p_k = param_kind(sz_p)
tstr = type2str(ty)
if sz_p_k == OUT or sz_p_k == INOUT:
sz_e = ("(*a%s)" % sz)
else:
sz_e = ("a%s" % sz)
log_c.write(" for (unsigned i = 0; i < %s; ++i) { " % sz_e)
if is_obj(ty):
log_c.write("P(0);")
log_c.write(" }\n")
log_c.write(" Ap(%s);\n" % sz_e)
exe_c.write("reinterpret_cast<%s*>(in.get_obj_array(%s))" % (tstr, i))
elif ty == UINT:
log_c.write("U(0);")
log_c.write(" }\n")
log_c.write(" Au(%s);\n" % sz_e)
exe_c.write("in.get_uint_array(%s)" % i)
else:
error ("unsupported parameter for %s, %s" % (name, p))
elif kind == OUT_MANAGED_ARRAY:
sz = param_array_size_pos(p)
sz_p = params[sz]
sz_p_k = param_kind(sz_p)
tstr = type2str(ty)
if sz_p_k == OUT or sz_p_k == INOUT:
sz_e = ("(*a%s)" % sz)
else:
sz_e = ("a%s" % sz)
log_c.write(" for (unsigned i = 0; i < %s; ++i) { " % sz_e)
log_c.write("P(0);")
log_c.write(" }\n")
log_c.write(" Ap(%s);\n" % sz_e)
exe_c.write("reinterpret_cast<%s**>(in.get_obj_array(%s))" % (tstr, i))
elif kind == FN_PTR:
log_c.write("// P(a%s);\n" % i)
exe_c.write("reinterpret_cast<%s>(in.get_obj(%s))" % (param2str(p), i))
else:
error ("unsupported parameter for %s, %s" % (name, p))
i = i + 1
log_c.write(" C(%s);\n" % next_id)
exe_c.write(");\n")
if is_obj(result):
exe_c.write(" in.store_result(result);\n")
if name == 'Z3_mk_context' or name == 'Z3_mk_context_rc':
exe_c.write(" Z3_set_error_handler(result, Z3_replayer_error_handler);")
log_c.write('}\n')
exe_c.write('}\n')
mk_log_macro(log_h, name, params)
if log_result(result, params):
mk_log_result_macro(log_h, name, result, params)
next_id = next_id + 1
def mk_bindings(exe_c):
exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n")
for key, val in API2Id.items():
exe_c.write(" in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val))
exe_c.write("}\n")
def ml_method_name(name):
return name[3:]
def is_out_param(p):
if param_kind(p) == OUT or param_kind(p) == INOUT or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_MANAGED_ARRAY:
return True
else:
return False
def outparams(params):
op = []
for param in params:
if is_out_param(param):
op.append(param)
return op
def is_in_param(p):
if param_kind(p) == IN or param_kind(p) == INOUT or param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY:
return True
else:
return False
def inparams(params):
ip = []
for param in params:
if is_in_param(param):
ip.append(param)
return ip
def is_array_param(p):
if param_kind(p) == IN_ARRAY or param_kind(p) == INOUT_ARRAY or param_kind(p) == OUT_ARRAY:
return True
else:
return False
def arrayparams(params):
op = []
for param in params:
if is_array_param(param):
op.append(param)
return op
def ml_plus_type(ts):
if ts == 'Z3_context':
return 'Z3_context_plus'
elif ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern':
return 'Z3_ast_plus'
elif ts == 'Z3_symbol':
return 'Z3_symbol_plus'
elif ts == 'Z3_constructor':
return 'Z3_constructor_plus'
elif ts == 'Z3_constructor_list':
return 'Z3_constructor_list_plus'
elif ts == 'Z3_rcf_num':
return 'Z3_rcf_num_plus'
elif ts == 'Z3_params':
return 'Z3_params_plus'
elif ts == 'Z3_param_descrs':
return 'Z3_param_descrs_plus'
elif ts == 'Z3_model':
return 'Z3_model_plus'
elif ts == 'Z3_func_interp':
return 'Z3_func_interp_plus'
elif ts == 'Z3_func_entry':
return 'Z3_func_entry_plus'
elif ts == 'Z3_goal':
return 'Z3_goal_plus'
elif ts == 'Z3_tactic':
return 'Z3_tactic_plus'
elif ts == 'Z3_simplifier':
return 'Z3_simplifier_plus'
elif ts == 'Z3_probe':
return 'Z3_probe_plus'
elif ts == 'Z3_apply_result':
return 'Z3_apply_result_plus'
elif ts == 'Z3_solver':
return 'Z3_solver_plus'
elif ts == 'Z3_stats':
return 'Z3_stats_plus'
elif ts == 'Z3_ast_vector':
return 'Z3_ast_vector_plus'
elif ts == 'Z3_ast_map':
return 'Z3_ast_map_plus'
elif ts == 'Z3_fixedpoint':
return 'Z3_fixedpoint_plus'
elif ts == 'Z3_optimize':
return 'Z3_optimize_plus'
else:
return ts
def ml_minus_type(ts):
if ts == 'Z3_ast' or ts == 'Z3_sort' or ts == 'Z3_func_decl' or ts == 'Z3_app' or ts == 'Z3_pattern':
return 'Z3_ast'
if ts == 'Z3_ast_plus' or ts == 'Z3_sort_plus' or ts == 'Z3_func_decl_plus' or ts == 'Z3_app_plus' or ts == 'Z3_pattern_plus':
return 'Z3_ast'
elif ts == 'Z3_constructor_plus':
return 'Z3_constructor'
elif ts == 'Z3_constructor_list_plus':
return 'Z3_constructor_list'
elif ts == 'Z3_rcf_num_plus':
return 'Z3_rcf_num'
elif ts == 'Z3_params_plus':
return 'Z3_params'
elif ts == 'Z3_param_descrs_plus':
return 'Z3_param_descrs'
elif ts == 'Z3_model_plus':
return 'Z3_model'
elif ts == 'Z3_func_interp_plus':
return 'Z3_func_interp'
elif ts == 'Z3_func_entry_plus':
return 'Z3_func_entry'
elif ts == 'Z3_goal_plus':
return 'Z3_goal'
elif ts == 'Z3_tactic_plus':
return 'Z3_tactic'
elif ts == 'Z3_simplifier_plus':
return 'Z3_simplifier'
elif ts == 'Z3_probe_plus':
return 'Z3_probe'
elif ts == 'Z3_apply_result_plus':
return 'Z3_apply_result'
elif ts == 'Z3_solver_plus':
return 'Z3_solver'
elif ts == 'Z3_stats_plus':
return 'Z3_stats'
elif ts == 'Z3_ast_vector_plus':
return 'Z3_ast_vector'
elif ts == 'Z3_ast_map_plus':
return 'Z3_ast_map'
elif ts == 'Z3_fixedpoint_plus':
return 'Z3_fixedpoint'
elif ts == 'Z3_optimize_plus':
return 'Z3_optimize'
else:
return ts
def ml_plus_type_raw(ts):
if ml_has_plus_type(ts):
return ml_plus_type(ts) + '_raw';
else:
return ts
def ml_plus_ops_type(ts):
if ml_has_plus_type(ts):
return ml_plus_type(ts) + '_custom_ops'
else:
return 'default_custom_ops'
def ml_has_plus_type(ts):
return ts != ml_plus_type(ts)
def ml_unwrap(t, ts, s):
if t == STRING:
return '(' + ts + ') String_val(' + s + ')'
elif t == BOOL or (type2str(t) == 'bool'):
return '(' + ts + ') Bool_val(' + s + ')'
elif t == INT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return '(' + ts + ') Int_val(' + s + ')'
elif t == UINT:
return '(' + ts + ') Unsigned_int_val(' + s + ')'
elif t == INT64:
return '(' + ts + ') Int64_val(' + s + ')'
elif t == UINT64:
return '(' + ts + ') Int64_val(' + s + ')'
elif t == DOUBLE:
return '(' + ts + ') Double_val(' + s + ')'
elif ml_has_plus_type(ts):
pts = ml_plus_type(ts)
return '(' + ts + ') ' + ml_plus_type_raw(ts) + '((' + pts + '*) Data_custom_val(' + s + '))'
else:
return '* ((' + ts + '*) Data_custom_val(' + s + '))'
def ml_set_wrap(t, d, n):
if t == VOID:
return d + ' = Val_unit;'
elif t == BOOL or (type2str(t) == 'bool'):
return d + ' = Val_bool(' + n + ');'
elif t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == LBOOL:
return d + ' = Val_int(' + n + ');'
elif t == INT64 or t == UINT64:
return d + ' = caml_copy_int64(' + n + ');'
elif t == DOUBLE:
return d + '= caml_copy_double(' + n + ');'
elif t == STRING:
return d + ' = caml_copy_string((const char*) ' + n + ');'
else:
pts = ml_plus_type(type2str(t))
return '*(' + pts + '*)Data_custom_val(' + d + ') = ' + n + ';'
def ml_alloc_and_store(t, lhs, rhs):
if t == VOID or t == BOOL or t == INT or t == UINT or t == PRINT_MODE or t == ERROR_CODE or t == INT64 or t == UINT64 or t == DOUBLE or t == STRING or t == LBOOL or (type2str(t) == 'bool'):
return ml_set_wrap(t, lhs, rhs)
else:
pts = ml_plus_type(type2str(t))
pops = ml_plus_ops_type(type2str(t))
alloc_str = '%s = caml_alloc_custom(&%s, sizeof(%s), 0, 1); ' % (lhs, pops, pts)
return alloc_str + ml_set_wrap(t, lhs, rhs)
z3_long_funs = frozenset([
'Z3_solver_check',
'Z3_solver_check_assumptions',
'Z3_simplify',
'Z3_simplify_ex',
])
z3_ml_overrides = frozenset([
'Z3_mk_config'])
z3_ml_callbacks = frozenset([
'Z3_solver_propagate_init',
'Z3_solver_propagate_fixed',
'Z3_solver_propagate_final',
'Z3_solver_propagate_eq',
'Z3_solver_propagate_diseq',
'Z3_solver_propagate_created',
'Z3_solver_propagate_decide',
'Z3_solver_propagate_on_binding',
'Z3_solver_register_on_clause'
])
def mk_ml(ml_src_dir, ml_output_dir):
global Type2Str
ml_nativef = os.path.join(ml_output_dir, 'z3native.ml')
ml_native = open(ml_nativef, 'w')
ml_native.write('(* Automatically generated file *)\n\n')
ml_pref = open(os.path.join(ml_src_dir, 'z3native.ml.pre'), 'r')
for s in ml_pref:
ml_native.write(s);
ml_pref.close()
ml_native.write('\n')
for name, result, params in _dotnet_decls:
if name in z3_ml_callbacks:
continue
ml_native.write('external %s : ' % ml_method_name(name))
ip = inparams(params)
op = outparams(params)
if len(ip) == 0:
ml_native.write(' unit -> ')
for p in ip:
ml_native.write('%s -> ' % param2ml(p))
if len(op) > 0:
ml_native.write('(')
first = True
if result != VOID or len(op) == 0:
ml_native.write('%s' % type2ml(result))
first = False
for p in op:
if first:
first = False
else:
ml_native.write(' * ')
ml_native.write('%s' % param2ml(p))
if len(op) > 0:
ml_native.write(')')
if len(ip) > 5:
ml_native.write(' = "n_%s_bytecode" "n_%s"\n' % (ml_method_name(name), ml_method_name(name)))
else:
ml_native.write(' = "n_%s"\n' % ml_method_name(name))
ml_native.write('\n')
for type_id in Type2Str:
type_name = Type2Str[type_id]
if ml_has_plus_type(type_name) and not type_name in ['Z3_context', 'Z3_sort', 'Z3_func_decl', 'Z3_app', 'Z3_pattern']:
ml_name = type2ml(type_id)
ml_native.write('external context_of_%s : %s -> context = "n_context_of_%s"\n' % (ml_name, ml_name, ml_name))
ml_native.write('external is_null_%s : %s -> bool = "n_is_null_%s"\n' % (ml_name, ml_name, ml_name))
ml_native.write('external mk_null_%s : context -> %s = "n_mk_null_%s"\n\n' % (ml_name, ml_name, ml_name))
ml_native.write('(**/**)\n')
ml_native.close()
if is_verbose():
print ('Generated "%s"' % ml_nativef)
mk_z3native_stubs_c(ml_src_dir, ml_output_dir)
def mk_z3native_stubs_c(ml_src_dir, ml_output_dir): ml_wrapperf = os.path.join(ml_output_dir, 'z3native_stubs.c')
ml_wrapper = open(ml_wrapperf, 'w')
ml_wrapper.write('// Automatically generated file\n\n')
ml_pref = open(os.path.join(ml_src_dir, 'z3native_stubs.c.pre'), 'r')
for s in ml_pref:
ml_wrapper.write(s);
ml_pref.close()
for name, result, params in _dotnet_decls:
if name in z3_ml_overrides:
continue
if name in z3_ml_callbacks:
continue
ip = inparams(params)
op = outparams(params)
ap = arrayparams(params)
ret_size = len(op)
if result != VOID:
ret_size = ret_size + 1
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s(' % ml_method_name(name))
first = True
i = 0
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_wrapper.write(', ')
ml_wrapper.write('value a%d' % i)
i = i + 1
ml_wrapper.write(') {\n')
ml_wrapper.write(' CAMLparam%d(' % len(ip))
i = 0
first = True
for p in params:
if is_in_param(p):
if first:
first = False
else:
ml_wrapper.write(', ')
ml_wrapper.write('a%d' % i)
i = i + 1
ml_wrapper.write(');\n')
i = 0
if len(op) + len(ap) == 0:
ml_wrapper.write(' CAMLlocal1(result);\n')
else:
c = 0
needs_tmp_value = False
for p in params:
if is_out_param(p) or is_array_param(p):
c = c + 1
needs_tmp_value = needs_tmp_value or param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY
if needs_tmp_value:
c = c + 1
if len(ap) > 0:
c = c + 1
ml_wrapper.write(' CAMLlocal%s(result, z3rv_val' % (c+2))
for p in params:
if is_out_param(p) or is_array_param(p):
ml_wrapper.write(', _a%s_val' % i)
i = i + 1
if needs_tmp_value:
ml_wrapper.write(', tmp_val')
if len(ap) != 0:
ml_wrapper.write(', _iter');
ml_wrapper.write(');\n')
if len(ap) > 0:
ml_wrapper.write(' unsigned _i;\n')
have_context = (len(params) > 0) and (param_type(params[0]) == CONTEXT)
if have_context and name not in Unwrapped and name not in Unchecked:
ml_wrapper.write(' Z3_error_code ec;\n')
if result != VOID:
ts = type2str(result)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' %s z3rv_m;\n' % ts)
ml_wrapper.write(' %s z3rv;\n' % pts)
else:
ml_wrapper.write(' %s z3rv;\n' % ts)
i = 0
for param in params:
if param_type(param) == CONTEXT and i == 0:
ml_wrapper.write(' Z3_context_plus ctx_p;\n')
ml_wrapper.write(' Z3_context _a0;\n')
else:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i))
elif k == OUT_MANAGED_ARRAY:
ml_wrapper.write(' %s * _a%s;\n' % (type2str(param_type(param)), i))
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' %s * _a%s;\n' % (ts, i))
elif k == IN:
t = param_type(param)
ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i))
elif k == OUT or k == INOUT:
t = param_type(param)
ml_wrapper.write(' %s _a%s;\n' % (type2str(t), i))
ts = type2str(t)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' %s _a%dp;\n' % (pts, i))
i = i + 1
ml_wrapper.write('\n')
i = 0
for param in params:
if param_type(param) == CONTEXT and i == 0:
ml_wrapper.write(' ctx_p = *(Z3_context_plus*) Data_custom_val(a' + str(i) + ');\n')
ml_wrapper.write(' _a0 = ctx_p->ctx;\n')
else:
k = param_kind(param)
if k == OUT_ARRAY:
ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * (_a%s));\n' % (
i,
type2str(param_type(param)),
type2str(param_type(param)),
param_array_capacity_pos(param)))
elif k == OUT_MANAGED_ARRAY:
ml_wrapper.write(' _a%s = 0;\n' % i)
elif k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' _a%s = (%s*) malloc(sizeof(%s) * _a%s);\n' % (i, ts, ts, param_array_capacity_pos(param)))
elif k == IN:
t = param_type(param)
ml_wrapper.write(' _a%s = %s;\n' % (i, ml_unwrap(t, type2str(t), 'a' + str(i))))
i = i + 1
i = 0
for param in params:
k = param_kind(param)
if k == IN_ARRAY or k == INOUT_ARRAY:
t = param_type(param)
ts = type2str(t)
ml_wrapper.write(' _iter = a' + str(i) + ';\n')
ml_wrapper.write(' for (_i = 0; _i < _a%s; ++_i) {\n' % param_array_capacity_pos(param))
ml_wrapper.write(' assert(_iter != Val_emptylist);\n')
ml_wrapper.write(' _a%s[_i] = %s;\n' % (i, ml_unwrap(t, ts, 'Field(_iter, 0)')))
ml_wrapper.write(' _iter = Field(_iter, 1);\n')
ml_wrapper.write(' }\n')
ml_wrapper.write(' assert(_iter == Val_emptylist);\n\n')
i = i + 1
release_caml_gc= name in z3_long_funs
if release_caml_gc:
ml_wrapper.write('\n caml_release_runtime_system();\n')
ml_wrapper.write('\n /* invoke Z3 function */\n ')
if result != VOID:
ts = type2str(result)
if ml_has_plus_type(ts):
ml_wrapper.write('z3rv_m = ')
else:
ml_wrapper.write('z3rv = ')
ml_wrapper.write('%s(' % name)
i = 0
first = True
for param in params:
if first:
first = False
else:
ml_wrapper.write(', ')
k = param_kind(param)
if k == OUT or k == INOUT or k == OUT_MANAGED_ARRAY:
ml_wrapper.write('&_a%s' % i)
else:
ml_wrapper.write('_a%i' % i)
i = i + 1
ml_wrapper.write(');\n')
if name in NULLWrapped:
ml_wrapper.write(' if (z3rv_m == NULL) {\n')
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), "Object allocation failed");\n')
ml_wrapper.write(' }\n')
if release_caml_gc:
ml_wrapper.write('\n caml_acquire_runtime_system();\n')
if have_context and name not in Unwrapped and name not in Unchecked:
ml_wrapper.write(' ec = Z3_get_error_code(ctx_p->ctx);\n')
ml_wrapper.write(' if (ec != Z3_OK) {\n')
ml_wrapper.write(' const char * msg = Z3_get_error_msg(ctx_p->ctx, ec);\n')
ml_wrapper.write(' caml_raise_with_string(*caml_named_value("Z3EXCEPTION"), msg);\n')
ml_wrapper.write(' }\n')
if result != VOID:
ts = type2str(result)
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
if name in NULLWrapped:
ml_wrapper.write(' z3rv = %s_mk(z3rv_m);\n' % pts)
else:
ml_wrapper.write(' z3rv = %s_mk(ctx_p, (%s) z3rv_m);\n' % (pts, ml_minus_type(ts)))
if len(op) > 0:
ml_wrapper.write('\n /* construct return tuple */\n')
ml_wrapper.write(' result = caml_alloc(%s, 0);\n' % ret_size)
i = 0
for p in params:
pt = param_type(p)
ts = type2str(pt)
if param_kind(p) == OUT_ARRAY or param_kind(p) == INOUT_ARRAY:
ml_wrapper.write('\n _a%s_val = Val_emptylist;\n' % i)
ml_wrapper.write(' for (_i = _a%s; _i > 0; _i--) {\n' % param_array_capacity_pos(p))
pts = ml_plus_type(ts)
pops = ml_plus_ops_type(ts)
if ml_has_plus_type(ts):
ml_wrapper.write(' %s _a%dp = %s_mk(ctx_p, (%s) _a%d[_i - 1]);\n' % (pts, i, pts, ml_minus_type(ts), i))
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%dp' % i))
else:
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, 'tmp_val', '_a%d[_i - 1]' % i))
ml_wrapper.write(' _iter = caml_alloc(2,0);\n')
ml_wrapper.write(' Store_field(_iter, 0, tmp_val);\n')
ml_wrapper.write(' Store_field(_iter, 1, _a%s_val);\n' % i)
ml_wrapper.write(' _a%s_val = _iter;\n' % i)
ml_wrapper.write(' }\n\n')
elif param_kind(p) == OUT_MANAGED_ARRAY:
wrp = ml_set_wrap(pt, '_a%d_val' % i, '_a%d' % i)
wrp = wrp.replace('*)', '**)')
wrp = wrp.replace('_plus', '')
ml_wrapper.write(' %s\n' % wrp)
elif is_out_param(p):
if ml_has_plus_type(ts):
pts = ml_plus_type(ts)
ml_wrapper.write(' _a%dp = %s_mk(ctx_p, (%s) _a%d);\n' % (i, pts, ml_minus_type(ts), i))
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%dp' % i))
else:
ml_wrapper.write(' %s\n' % ml_alloc_and_store(pt, '_a%d_val' % i, '_a%d' % i))
i = i + 1
i = j = 0
if result != VOID:
ml_wrapper.write(' %s' % ml_alloc_and_store(result, 'z3rv_val', 'z3rv'))
ml_wrapper.write(' Store_field(result, 0, z3rv_val);\n')
j = j + 1
for p in params:
if is_out_param(p):
ml_wrapper.write(' Store_field(result, %s, _a%s_val);\n' % (j, i))
j = j + 1
i = i + 1
else:
ml_wrapper.write('\n /* construct simple return value */\n')
ml_wrapper.write(' %s' % ml_alloc_and_store(result, "result", "z3rv"))
ml_wrapper.write('\n /* cleanup and return */\n')
i = 0
for p in params:
k = param_kind(p)
if k == OUT_ARRAY or k == IN_ARRAY or k == INOUT_ARRAY:
ml_wrapper.write(' free(_a%s);\n' % i)
i = i + 1
ml_wrapper.write(' CAMLreturn(result);\n')
ml_wrapper.write('}\n\n')
if len(ip) > 5:
ml_wrapper.write('CAMLprim DLL_PUBLIC value n_%s_bytecode(value * argv, int argn) {\n' % ml_method_name(name))
ml_wrapper.write(' return n_%s(' % ml_method_name(name))
i = 0
while i < len(ip):
if i == 0:
ml_wrapper.write('argv[0]')
else:
ml_wrapper.write(', argv[%s]' % i)
i = i + 1
ml_wrapper.write(');\n}\n')
ml_wrapper.write('\n\n')
ml_wrapper.write('#ifdef __cplusplus\n')
ml_wrapper.write('}\n')
ml_wrapper.write('#endif\n')
if is_verbose():
print ('Generated "%s"' % ml_wrapperf)
def def_APIs(api_files):
pat1 = re.compile(" *def_API.*")
pat2 = re.compile(" *extra_API.*")
for api_file in api_files:
api = open(api_file, 'r')
for line in api:
line = line.strip('\r\n\t ')
try:
m = pat1.match(line)
if m:
eval(line)
m = pat2.match(line)
if m:
eval(line)
except Exception as e:
error('ERROR: While processing: %s: %s\n' % (e, line))
def write_log_h_preamble(log_h):
log_h.write('// Automatically generated file\n')
log_h.write('#include\"api/z3.h\"\n')
log_h.write('#ifdef __GNUC__\n')
log_h.write('#define _Z3_UNUSED __attribute__((unused))\n')
log_h.write('#else\n')
log_h.write('#define _Z3_UNUSED\n')
log_h.write('#endif\n')
log_h.write('#include "util/mutex.h"\n')
log_h.write('extern atomic<bool> g_z3_log_enabled;\n')
log_h.write('void ctx_enable_logging();\n')
log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx() { ATOMIC_EXCHANGE(m_prev, g_z3_log_enabled, false); } ~z3_log_ctx() { if (m_prev) [[unlikely]] g_z3_log_enabled = true; } bool enabled() const { return m_prev; } };\n')
log_h.write('void SetR(const void * obj);\nvoid SetO(void * obj, unsigned pos);\nvoid SetAO(void * obj, unsigned pos, unsigned idx);\n')
log_h.write('#define RETURN_Z3(Z3RES) do { auto tmp_ret = Z3RES; if (_LOG_CTX.enabled()) [[unlikely]] { SetR(tmp_ret); } return tmp_ret; } while (0)\n')
def write_log_c_preamble(log_c):
log_c.write('// Automatically generated file\n')
log_c.write('#include\"api/z3.h\"\n')
log_c.write('#include\"api/api_log_macros.h\"\n')
log_c.write('#include\"api/z3_logger.h\"\n')
def write_exe_c_preamble(exe_c):
exe_c.write('// Automatically generated file\n')
exe_c.write('#include\"api/z3.h\"\n')
exe_c.write('#include\"api/z3_replayer.h\"\n')
exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n')
def write_core_py_post(core_py):
core_py.write("""
# Clean up
del _lib
del _lib_name
del _lib_names
del _default_dirs
del _all_dirs
del _ext
del _sover
""")
def write_core_py_preamble(core_py, z3py_soversion=None):
core_py.write(
"""
# Automatically generated file
import atexit
import sys, os
import contextlib
import ctypes
if sys.version_info >= (3, 9):
import importlib.resources as importlib_resources
else:
import importlib_resources
from .z3types import *
from .z3consts import *
_file_manager = contextlib.ExitStack()
atexit.register(_file_manager.close)
""")
core_py.write(f"_sover = {z3py_soversion!r}\n")
core_py.write(
"""
_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
_lib_name = 'libz3.%s.%s' % (_ext, _sover) if sys.platform.startswith('linux') and _sover else 'libz3.%s' % _ext
# On Linux with a soversion, also try the unversioned name as a fallback (e.g. build directories)
_lib_names = ['libz3.%s.%s' % (_ext, _sover), 'libz3.%s' % _ext] if sys.platform.startswith('linux') and _sover else ['libz3.%s' % _ext]
_lib = None
_z3_lib_resource = importlib_resources.files('z3').joinpath('lib')
_z3_lib_resource_path = _file_manager.enter_context(
importlib_resources.as_file(_z3_lib_resource)
)
_default_dirs = ['.',
os.path.dirname(os.path.abspath(__file__)),
_z3_lib_resource_path,
os.path.join(sys.prefix, 'lib'),
None]
_all_dirs = []
# search the default dirs first
_all_dirs.extend(_default_dirs)
if sys.version < '3':
import __builtin__
if hasattr(__builtin__, "Z3_LIB_DIRS"):
_all_dirs = __builtin__.Z3_LIB_DIRS
else:
import builtins
if hasattr(builtins, "Z3_LIB_DIRS"):
_all_dirs = builtins.Z3_LIB_DIRS
for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'):
if v in os.environ:
lp = os.environ[v];
lds = lp.split(';') if sys.platform in ('win32') else lp.split(':')
_all_dirs.extend(lds)
_failures = []
for _name in _lib_names:
for d in _all_dirs:
try:
d = os.path.realpath(d)
if os.path.isdir(d):
d = os.path.join(d, _name)
if os.path.isfile(d):
_lib = ctypes.CDLL(d)
break
except Exception as e:
_failures += [e]
pass
if _lib is not None:
break
if _lib is None:
# If all else failed, ask the system to find it.
for _name in _lib_names:
try:
_lib = ctypes.CDLL(_name)
break
except Exception as e:
_failures += [e]
pass
if _lib is None:
print("Could not find %s; consider adding the directory containing it to" % ' or '.join(_lib_names))
print(" - your system's PATH environment variable,")
print(" - the Z3_LIBRARY_PATH environment variable, or ")
print(" - to the custom Z3_LIB_DIRS Python-builtin before importing the z3 module, e.g. via")
if sys.version < '3':
print(" import __builtin__")
print(" __builtin__.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing %s" % _lib_name)
else:
print(" import builtins")
print(" builtins.Z3_LIB_DIRS = [ '/path/to/z3/lib/dir' ] # directory containing %s" % _lib_name)
print(_failures)
raise Z3Exception("%s not found." % _lib_name)
if sys.version < '3':
def _str_to_bytes(s):
return s
def _to_pystr(s):
return s
else:
def _str_to_bytes(s):
if isinstance(s, str):
enc = sys.getdefaultencoding()
return s.encode(enc if enc != None else 'latin-1')
else:
return s
def _to_pystr(s):
if s != None:
enc = sys.getdefaultencoding()
return s.decode(enc if enc != None else 'latin-1')
else:
return ""
_error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
_lib.Z3_set_error_handler.restype = None
_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
Z3_on_clause_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.POINTER(ctypes.c_uint), ctypes.c_void_p)
Z3_push_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
Z3_pop_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint)
Z3_fresh_eh = ctypes.CFUNCTYPE(ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_fixed_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_final_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p)
Z3_eq_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_created_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
Z3_decide_eh = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_uint, ctypes.c_int)
Z3_on_binding_eh = ctypes.CFUNCTYPE(ctypes.c_bool, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p, ctypes.c_void_p)
_lib.Z3_solver_register_on_clause.restype = None
_lib.Z3_solver_propagate_init.restype = None
_lib.Z3_solver_propagate_final.restype = None
_lib.Z3_solver_propagate_fixed.restype = None
_lib.Z3_solver_propagate_eq.restype = None
_lib.Z3_solver_propagate_diseq.restype = None
_lib.Z3_solver_propagate_decide.restype = None
on_model_eh_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p)
_lib.Z3_optimize_register_model_eh.restype = None
_lib.Z3_optimize_register_model_eh.argtypes = [ContextObj, OptimizeObj, ModelObj, ctypes.c_void_p, on_model_eh_type]
"""
)
log_h = None
log_c = None
exe_c = None
core_py = None
def generate_files(api_files,
api_output_dir=None,
z3py_output_dir=None,
z3py_soversion=None,
dotnet_output_dir=None,
java_input_dir=None,
java_output_dir=None,
java_package_name=None,
ml_output_dir=None,
ml_src_dir=None):
global log_h, log_c, exe_c, core_py
assert isinstance(api_files, list)
def mk_file_or_temp(output_dir, file_name, mode='w'):
if output_dir != None:
if not (os.path.exists(output_dir) and os.path.isdir(output_dir)):
raise ValueError(f"Output directory '{output_dir}' does not exist or is not a directory")
return open(os.path.join(output_dir, file_name), mode)
else:
print("Faking emission of '{}'".format(file_name))
import tempfile
return tempfile.TemporaryFile(mode=mode)
apiTypes = APITypes()
with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h:
with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c:
with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c:
with mk_file_or_temp(z3py_output_dir, os.path.join('z3', 'z3core.py')) as core_py:
write_log_h_preamble(log_h)
write_log_c_preamble(log_c)
write_exe_c_preamble(exe_c)
write_core_py_preamble(core_py, z3py_soversion)
apiTypes.def_Types(api_files)
def_APIs(api_files)
mk_bindings(exe_c)
mk_py_wrappers()
write_core_py_post(core_py)
if is_verbose():
print("Generated '{}'".format(log_h.name))
print("Generated '{}'".format(log_c.name))
print("Generated '{}'".format(exe_c.name))
print("Generated '{}'".format(core_py.name))
if dotnet_output_dir:
with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file:
mk_dotnet(dotnet_file)
mk_dotnet_wrappers(dotnet_file)
if is_verbose():
print("Generated '{}'".format(dotnet_file.name))
if java_output_dir:
mk_java(java_input_dir, java_output_dir, java_package_name)
if ml_output_dir:
assert not ml_src_dir is None
mk_ml(ml_src_dir, ml_output_dir)
def main(args):
logging.basicConfig(level=logging.INFO)
parser = argparse.ArgumentParser(description=__doc__)
parser.add_argument("api_files",
nargs="+",
help="API header files to generate files from")
parser.add_argument("--api_output_dir",
default=None,
help="Directory to emit files for api module. If not specified no files are emitted.")
parser.add_argument("--z3py-output-dir",
dest="z3py_output_dir",
default=None,
help="Directory to emit z3py files. If not specified no files are emitted.")
parser.add_argument("--z3py-soversion",
dest="z3py_soversion",
default=None,
help="SOVERSION for loading libz3 on supported platforms.")
parser.add_argument("--dotnet-output-dir",
dest="dotnet_output_dir",
default=None,
help="Directory to emit dotnet files. If not specified no files are emitted.")
parser.add_argument("--java-input-dir",
dest="java_input_dir",
default=None,
help="Directory where Java sources reside.")
parser.add_argument("--java-output-dir",
dest="java_output_dir",
default=None,
help="Directory to emit Java files. If not specified no files are emitted.")
parser.add_argument("--java-package-name",
dest="java_package_name",
default=None,
help="Name to give the Java package (e.g. ``com.microsoft.z3``).")
parser.add_argument("--ml-src-dir",
dest="ml_src_dir",
default=None,
help="Directory containing OCaml source files. If not specified no files are emitted")
parser.add_argument("--ml-output-dir",
dest="ml_output_dir",
default=None,
help="Directory to emit OCaml files. If not specified no files are emitted.")
pargs = parser.parse_args(args)
if pargs.java_output_dir:
if pargs.java_package_name == None:
logging.error('--java-package-name must be specified')
return 1
if pargs.java_input_dir is None:
logging.error('--java-input-dir must be specified')
return 1
if pargs.ml_output_dir:
if pargs.ml_src_dir is None:
logging.error('--ml-src-dir must be specified')
return 1
for api_file in pargs.api_files:
if not os.path.exists(api_file):
logging.error('"{}" does not exist'.format(api_file))
return 1
generate_files(api_files=pargs.api_files,
api_output_dir=pargs.api_output_dir,
z3py_output_dir=pargs.z3py_output_dir,
z3py_soversion=pargs.z3py_soversion,
dotnet_output_dir=pargs.dotnet_output_dir,
java_input_dir=pargs.java_input_dir,
java_output_dir=pargs.java_output_dir,
java_package_name=pargs.java_package_name,
ml_output_dir=pargs.ml_output_dir,
ml_src_dir=pargs.ml_src_dir)
return 0
if __name__ == '__main__':
sys.exit(main(sys.argv[1:]))