diff --git a/scripts/update_api.py b/scripts/update_api.py index 09c4fbe1c..2ffd95e3d 100644 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -108,6 +108,7 @@ INOUT = 2 IN_ARRAY = 3 OUT_ARRAY = 4 INOUT_ARRAY = 5 +OUT_MANAGED_ARRAY = 6 # Primitive Types VOID = 0 @@ -224,6 +225,10 @@ def _out_array2(cap, sz, ty): 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] @@ -254,11 +259,11 @@ def param2dotnet(p): return "out IntPtr" else: return "[In, Out] ref %s" % type2dotnet(param_type(p)) - if k == IN_ARRAY: + elif k == IN_ARRAY: return "[In] %s[]" % type2dotnet(param_type(p)) - if k == INOUT_ARRAY: + elif k == INOUT_ARRAY: return "[In, Out] %s[]" % type2dotnet(param_type(p)) - if k == OUT_ARRAY: + elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY: return "[Out] out %s[]" % type2dotnet(param_type(p)) else: return type2dotnet(param_type(p)) @@ -268,7 +273,7 @@ def param2java(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) >= FIRST_OBJ_ID: + 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" @@ -466,7 +471,7 @@ def mk_dotnet_wrappers(): dotnet.write('out '); else: dotnet.write('ref ') - elif param_kind(param) == OUT_ARRAY: + elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY: dotnet.write('out '); dotnet.write('a%d' % i) i = i + 1 @@ -678,9 +683,11 @@ def mk_java(): if param_type(param) == INT or param_type(param) == UINT: 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)) + 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 # invoke procedure java_wrapper.write(' ') @@ -699,6 +706,8 @@ def mk_java(): 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: @@ -734,6 +743,8 @@ def mk_java(): 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)) i = i + 1 # return if result == STRING: @@ -934,6 +945,9 @@ def def_API(name, result, params): elif ty == INT64: log_c.write(" I(0);\n") exe_c.write("in.get_int64_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: @@ -978,6 +992,20 @@ def def_API(name, result, params): 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)) else: error ("unsupported parameter for %s, %s" % (name, p)) i = i + 1 diff --git a/src/api/api_interp.cpp b/src/api/api_interp.cpp index 3e9ddc8a3..dbf68da38 100644 --- a/src/api/api_interp.cpp +++ b/src/api/api_interp.cpp @@ -520,7 +520,7 @@ extern "C" { } - int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast cnsts[], unsigned parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast theory[]){ + int Z3_read_interpolation_problem(Z3_context ctx, unsigned *_num, Z3_ast *cnsts[], unsigned *parents[], const char *filename, Z3_string_ptr error, unsigned *ret_num_theory, Z3_ast *theory[]){ hash_map file_params; get_file_params(filename, file_params); @@ -549,11 +549,11 @@ extern "C" { if (ret_num_theory) *ret_num_theory = num_theory; if (theory) - theory = &read_theory[0]; + *theory = &read_theory[0]; if (!parents){ *_num = num; - cnsts = &read_cnsts[0]; + *cnsts = &read_cnsts[0]; return true; } @@ -623,8 +623,8 @@ extern "C" { } *_num = num; - cnsts = &read_cnsts[0]; - parents = &read_parents[0]; + *cnsts = &read_cnsts[0]; + *parents = &read_parents[0]; return true; fail: diff --git a/src/api/dotnet/InterpolationContext.cs b/src/api/dotnet/InterpolationContext.cs index fbedadffe..8ba5fe773 100644 --- a/src/api/dotnet/InterpolationContext.cs +++ b/src/api/dotnet/InterpolationContext.cs @@ -129,27 +129,21 @@ namespace Microsoft.Z3 /// For more information on interpolation please refer /// too the function Z3_read_interpolation_problem in the C/C++ API, which is /// well documented. - public int ReadInterpolationProblem(string filename, out Expr[] cnsts, ref uint[] parents, out string error, out Expr[] theory) + public int ReadInterpolationProblem(string filename, out Expr[] cnsts, out uint[] parents, out string error, out Expr[] theory) { uint num = 0, num_theory = 0; - IntPtr n_cnsts = new IntPtr(); - IntPtr n_theory = new IntPtr(); + IntPtr[] n_cnsts; + IntPtr[] n_theory; IntPtr n_err_str; - int r = Native.Z3_read_interpolation_problem(nCtx, ref num, ref n_cnsts, out parents, filename, out n_err_str, ref num_theory, ref n_theory); + int r = Native.Z3_read_interpolation_problem(nCtx, ref num, out n_cnsts, out parents, filename, out n_err_str, ref num_theory, out n_theory); error = Marshal.PtrToStringAnsi(n_err_str); cnsts = new Expr[num]; parents = new uint[num]; theory = new Expr[num_theory]; for (int i = 0; i < num; i++) - { - IntPtr ce = new IntPtr(n_cnsts.ToInt64() + (IntPtr.Size * i)); - cnsts[i] = Expr.Create(this, ce); - } + cnsts[i] = Expr.Create(this, n_cnsts[i]); for (int i = 0; i < num_theory; i++) - { - IntPtr te = new IntPtr(n_theory.ToInt64() + (IntPtr.Size * i)); - theory[i] = Expr.Create(this, te); - } + theory[i] = Expr.Create(this, n_theory[i]); return r; } diff --git a/src/api/z3_interp.h b/src/api/z3_interp.h index 88ba83e2d..729851988 100644 --- a/src/api/z3_interp.h +++ b/src/api/z3_interp.h @@ -206,18 +206,18 @@ extern "C" { where each value is represented using the common symbols between the formulas in the subtree and the remainder of the formulas. - def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out(AST), _out_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out(AST))) + def_API('Z3_read_interpolation_problem', INT, (_in(CONTEXT), _out(UINT), _out_managed_array(1, AST), _out_managed_array(1, UINT), _in(STRING), _out(STRING), _out(UINT), _out_managed_array(6, AST))) */ int Z3_API Z3_read_interpolation_problem(__in Z3_context ctx, __out unsigned *num, - __out Z3_ast *cnsts, - __out unsigned parents[], + __out Z3_ast *cnsts[], + __out unsigned *parents[], __in Z3_string filename, __out_opt Z3_string_ptr error, __out unsigned *num_theory, - __out Z3_ast theory[]); + __out Z3_ast *theory[]);