mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-02 12:21:21 +00:00
Code Activity

revert some changes to how 'out' parameters are annotated on API calls. Retain the 'out' annotation for so-called managed out parameters. The data-type examples in managed API fail with the out parameter annotation as no memory is allocated on instances of out parameters, other than the interpolation APIs that are new

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-10-16 22:40:52 -07:00
parent 7767a23626
commit fe4a8b44a5
5 changed files with 12 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

8
scripts/update_api.py
View file

@ -263,8 +263,10 @@ def param2dotnet(p):
return "[In] %s[]" % type2dotnet(param_type(p)) return "[In] %s[]" % type2dotnet(param_type(p))
elif k == INOUT_ARRAY: elif k == INOUT_ARRAY:
return "[In, Out] %s[]" % type2dotnet(param_type(p)) return "[In, Out] %s[]" % type2dotnet(param_type(p))
elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY: elif k == OUT_ARRAY:
return "[Out] out %s[]" % type2dotnet(param_type(p)) return "[Out] %s[]" % type2dotnet(param_type(p))
elif k == OUT_MANAGED_ARRAY:
return "[Out] out %s[]" % type2dotnet(param_type(p))
else: else:
return type2dotnet(param_type(p)) return type2dotnet(param_type(p))
@ -476,7 +478,7 @@ def mk_dotnet_wrappers():
dotnet.write('out '); dotnet.write('out ');
else: else:
dotnet.write('ref ') dotnet.write('ref ')
elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY: elif param_kind(param) == OUT_MANAGED_ARRAY:
dotnet.write('out '); dotnet.write('out ');
dotnet.write('a%d' % i) dotnet.write('a%d' % i)
i = i + 1 i = i + 1

6
src/api/dotnet/Constructor.cs
View file

@ -50,7 +50,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero; IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero; IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n]; IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
return new FuncDecl(Context, constructor); return new FuncDecl(Context, constructor);
} }
} }
@ -66,7 +66,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero; IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero; IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n]; IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
return new FuncDecl(Context, tester); return new FuncDecl(Context, tester);
} }
} }
@ -82,7 +82,7 @@ namespace Microsoft.Z3
IntPtr constructor = IntPtr.Zero; IntPtr constructor = IntPtr.Zero;
IntPtr tester = IntPtr.Zero; IntPtr tester = IntPtr.Zero;
IntPtr[] accessors = new IntPtr[n]; IntPtr[] accessors = new IntPtr[n];
Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors); Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
FuncDecl[] t = new FuncDecl[n]; FuncDecl[] t = new FuncDecl[n];
for (uint i = 0; i < n; i++) for (uint i = 0; i < n; i++)
t[i] = new FuncDecl(Context, accessors[i]); t[i] = new FuncDecl(Context, accessors[i]);

2
src/api/dotnet/Context.cs
View file

@ -424,7 +424,7 @@ namespace Microsoft.Z3
n_constr[i] = cla[i].NativeObject; n_constr[i] = cla[i].NativeObject;
} }
IntPtr[] n_res = new IntPtr[n]; IntPtr[] n_res = new IntPtr[n];
Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr); Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
DatatypeSort[] res = new DatatypeSort[n]; DatatypeSort[] res = new DatatypeSort[n];
for (uint i = 0; i < n; i++) for (uint i = 0; i < n; i++)
res[i] = new DatatypeSort(this, n_res[i]); res[i] = new DatatypeSort(this, n_res[i]);

2
src/api/dotnet/EnumSort.cs
View file

@ -88,7 +88,7 @@ namespace Microsoft.Z3
IntPtr[] n_constdecls = new IntPtr[n]; IntPtr[] n_constdecls = new IntPtr[n];
IntPtr[] n_testers = new IntPtr[n]; IntPtr[] n_testers = new IntPtr[n];
NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n, NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers); Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
} }
#endregion #endregion
}; };

4
src/api/dotnet/TupleSort.cs
View file

@ -74,10 +74,10 @@ namespace Microsoft.Z3
Contract.Requires(name != null); Contract.Requires(name != null);
IntPtr t = IntPtr.Zero; IntPtr t = IntPtr.Zero;
IntPtr[] f; IntPtr[] f = new IntPtr[numFields];
NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields, NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts), Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
ref t, out f); ref t, f);
} }
#endregion #endregion
}; };