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

use static list to connect managed and unmanaged objects

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-06-28 14:09:22 -07:00
parent 820c782b5e
commit 556f0d7b5f
1 changed files with 22 additions and 28 deletions
Download patch file Download diff file Expand all files Collapse all files

48
src/api/dotnet/UserPropagator.cs
View file

@ -62,9 +62,12 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase); public delegate void DecideEh(ref Expr term, ref uint idx, ref int phase);
// access managed objects through a static array.
// thread safety is ignored for now.
static List<UserPropagator> propagators = new List<UserPropagator>();
int id;
Solver solver; Solver solver;
Context ctx; Context ctx;
GCHandle gch;
Z3_solver_callback callback = IntPtr.Zero; Z3_solver_callback callback = IntPtr.Zero;
FixedEh fixed_eh; FixedEh fixed_eh;
Action final_eh; Action final_eh;
@ -88,65 +91,56 @@ namespace Microsoft.Z3
static void _push(voidp ctx, Z3_solver_callback cb) { static void _push(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Push(), cb); prop.Callback(() => prop.Push(), cb);
} }
static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) { static void _pop(voidp ctx, Z3_solver_callback cb, uint num_scopes) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.Pop(num_scopes), cb); prop.Callback(() => prop.Pop(num_scopes), cb);
} }
static voidp _fresh(voidp _ctx, Z3_context new_context) { static voidp _fresh(voidp _ctx, Z3_context new_context) {
var gch = GCHandle.FromIntPtr(_ctx); var prop = propagators[_ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
var ctx = new Context(new_context); var ctx = new Context(new_context);
var prop1 = prop.Fresh(ctx); var prop1 = prop.Fresh(prop.ctx);
return GCHandle.ToIntPtr(prop1.gch); return new IntPtr(prop1.id);
} }
static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) { static void _fixed(voidp ctx, Z3_solver_callback cb, Z3_ast _term, Z3_ast _value) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
using var term = Expr.Create(prop.ctx, _term); using var term = Expr.Create(prop.ctx, _term);
using var value = Expr.Create(prop.ctx, _value); using var value = Expr.Create(prop.ctx, _value);
prop.Callback(() => prop.fixed_eh(term, value), cb); prop.Callback(() => prop.fixed_eh(term, value), cb);
} }
static void _final(voidp ctx, Z3_solver_callback cb) { static void _final(voidp ctx, Z3_solver_callback cb) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
prop.Callback(() => prop.final_eh(), cb); prop.Callback(() => prop.final_eh(), cb);
} }
static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { static void _eq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a); using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b); using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.eq_eh(s, t), cb); prop.Callback(() => prop.eq_eh(s, t), cb);
} }
static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) { static void _diseq(voidp ctx, Z3_solver_callback cb, Z3_ast a, Z3_ast b) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
using var s = Expr.Create(prop.ctx, a); using var s = Expr.Create(prop.ctx, a);
using var t = Expr.Create(prop.ctx, b); using var t = Expr.Create(prop.ctx, b);
prop.Callback(() => prop.diseq_eh(s, t), cb); prop.Callback(() => prop.diseq_eh(s, t), cb);
} }
static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) { static void _created(voidp ctx, Z3_solver_callback cb, Z3_ast a) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
using var t = Expr.Create(prop.ctx, a); using var t = Expr.Create(prop.ctx, a);
prop.Callback(() => prop.created_eh(t), cb); prop.Callback(() => prop.created_eh(t), cb);
} }
static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) { static void _decide(voidp ctx, Z3_solver_callback cb, ref Z3_ast a, ref uint idx, ref int phase) {
var gch = GCHandle.FromIntPtr(ctx); var prop = propagators[ctx.ToInt32()];
var prop = (UserPropagator)gch.Target;
var t = Expr.Create(prop.ctx, a); var t = Expr.Create(prop.ctx, a);
var u = t; var u = t;
prop.callback = cb; prop.callback = cb;
@ -161,11 +155,11 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public UserPropagator(Solver s) public UserPropagator(Solver s)
{ {
gch = GCHandle.Alloc(this, GCHandleType.Pinned); id = propagators.Count;
propagators.Add(this);
solver = s; solver = s;
ctx = solver.Context; ctx = solver.Context;
var cb = GCHandle.ToIntPtr(gch); Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, new IntPtr(id), _push, _pop, _fresh);
Native.Z3_solver_propagate_init(ctx.nCtx, solver.NativeObject, cb, _push, _pop, _fresh);
} }
/// <summary> /// <summary>
@ -173,7 +167,8 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
public UserPropagator(Context _ctx) public UserPropagator(Context _ctx)
{ {
gch = GCHandle.Alloc(this); id = propagators.Count;
propagators.Add(this);
solver = null; solver = null;
ctx = _ctx; ctx = _ctx;
} }
@ -183,8 +178,7 @@ namespace Microsoft.Z3
/// </summary> /// </summary>
~UserPropagator() ~UserPropagator()
{ {
if (gch != null) propagators[id] = null;
gch.Free();
if (solver == null) if (solver == null)
ctx.Dispose(); ctx.Dispose();
} }