mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

Resolved interpolation API issues.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2014-10-10 11:41:21 +01:00
parent 1c1351a064
commit 9b8406c717
4 changed files with 49 additions and 27 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

40
scripts/update_api.py
View file

@ -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

10
src/api/api_interp.cpp
View file

@ -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<std::string, std::string> 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:

18
src/api/dotnet/InterpolationContext.cs
View file

@ -129,27 +129,21 @@ namespace Microsoft.Z3
/// <remarks>For more information on interpolation please refer
/// too the function Z3_read_interpolation_problem in the C/C++ API, which is
/// well documented.</remarks>
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;
}

8
src/api/z3_interp.h
View file

@ -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[]);