mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

remove DecRefQueue, use Z3_enable_concurrent_dec_ref (#6332)

Browse source 
The notion of reference counted contexts never worked.
The reference count to a context only ends up being 0 if the GC kicks in and disposes the various z3 objects. A call to Dispose on Context should free up all resources associated with that context. In exchange none of the resources are allowed any other operation than DecRef. The invocations of DecRef are protected by a lock and test on the context that the native pointer associated with the context is non-zero. Dispose sets the native pointer to zero.

Z3_enable_concurrent_dec_ref ensures that:

- calls to decref are thread safe. Other threads can operate on the context without interference.

The Z3_context ensures that
- z3objects allocated, but not disposed during the lifetime of Z3_context are freed when Z3_context is deleted (it triggers a debug warning, but this is now benign).
This commit is contained in:
Nikolaj Bjorner 2022-09-11 18:59:00 -07:00 committed by GitHub
parent 3c8c80bbac
commit edeeded4ea
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
17 changed files with 114 additions and 460 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

35
src/api/dotnet/AST.cs
View file

@ -208,37 +208,22 @@ namespace Microsoft.Z3
internal AST(Context ctx) : base(ctx) { Debug.Assert(ctx != null); }
internal AST(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
// Console.WriteLine("AST IncRef()");
if (Context == null || o == IntPtr.Zero)
return;
Context.AST_DRQ.IncAndClear(Context, o);
base.IncRef(o);
if (Context != null && o != IntPtr.Zero)
Native.Z3_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
// Console.WriteLine("AST DecRef()");
if (Context == null || o == IntPtr.Zero)
return;
Context.AST_DRQ.Add(o);
base.DecRef(o);
if (Context != null && o != IntPtr.Zero)
{
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_dec_ref(Context.nCtx, o);
}
}
}
internal static AST Create(Context ctx, IntPtr obj)

25
src/api/dotnet/ASTMap.cs
View file

@ -125,31 +125,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_ast_map_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_ast_map_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.ASTMap_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_ast_map_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.ASTMap_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_ast_map_dec_ref(Context.nCtx, o);
}
}
#endregion
}

24
src/api/dotnet/ASTVector.cs
View file

@ -233,31 +233,19 @@ namespace Microsoft.Z3
internal ASTVector(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
internal ASTVector(Context ctx) : base(ctx, Native.Z3_mk_ast_vector(ctx.nCtx)) { Debug.Assert(ctx != null); }
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_ast_vector_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.ASTVector_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_ast_vector_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.ASTVector_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_ast_vector_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/ApplyResult.cs
View file

@ -67,31 +67,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.ApplyResult_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_apply_result_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.ApplyResult_DRQ.Add(o);
base.DecRef(o);
lock(Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_apply_result_dec_ref(Context.nCtx, o);
}
}
#endregion
}

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

@ -75,6 +75,7 @@ namespace Microsoft.Z3
foreach (KeyValuePair<string, string> kv in settings)
Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
m_ctx = Native.Z3_mk_context_rc(cfg);
Native.Z3_enable_concurrent_dec_ref(m_ctx);
Native.Z3_del_config(cfg);
InitContext();
}
@ -4852,123 +4853,9 @@ namespace Microsoft.Z3
private void ObjectInvariant()
{
Debug.Assert(m_AST_DRQ != null);
Debug.Assert(m_ASTMap_DRQ != null);
Debug.Assert(m_ASTVector_DRQ != null);
Debug.Assert(m_ApplyResult_DRQ != null);
Debug.Assert(m_FuncEntry_DRQ != null);
Debug.Assert(m_FuncInterp_DRQ != null);
Debug.Assert(m_Goal_DRQ != null);
Debug.Assert(m_Model_DRQ != null);
Debug.Assert(m_Params_DRQ != null);
Debug.Assert(m_ParamDescrs_DRQ != null);
Debug.Assert(m_Probe_DRQ != null);
Debug.Assert(m_Solver_DRQ != null);
Debug.Assert(m_Statistics_DRQ != null);
Debug.Assert(m_Tactic_DRQ != null);
Debug.Assert(m_Fixedpoint_DRQ != null);
Debug.Assert(m_Optimize_DRQ != null);
// none
}
readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue();
readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(10);
readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(10);
readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.DecRefQueue(10);
readonly private FuncInterp.Entry.DecRefQueue m_FuncEntry_DRQ = new FuncInterp.Entry.DecRefQueue(10);
readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(10);
readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(10);
readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(10);
readonly private Params.DecRefQueue m_Params_DRQ = new Params.DecRefQueue(10);
readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(10);
readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(10);
readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(10);
readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(10);
readonly private Tactic.DecRefQueue m_Tactic_DRQ = new Tactic.DecRefQueue(10);
readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10);
readonly private Optimize.DecRefQueue m_Optimize_DRQ = new Optimize.DecRefQueue(10);
/// <summary>
/// AST DRQ
/// </summary>
public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } }
/// <summary>
/// ASTMap DRQ
/// </summary>
public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } }
/// <summary>
/// ASTVector DRQ
/// </summary>
public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } }
/// <summary>
/// ApplyResult DRQ
/// </summary>
public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } }
/// <summary>
/// FuncEntry DRQ
/// </summary>
public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } }
/// <summary>
/// FuncInterp DRQ
/// </summary>
public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } }
/// <summary>
/// Goal DRQ
/// </summary>
public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } }
/// <summary>
/// Model DRQ
/// </summary>
public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } }
/// <summary>
/// Params DRQ
/// </summary>
public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } }
/// <summary>
/// ParamDescrs DRQ
/// </summary>
public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } }
/// <summary>
/// Probe DRQ
/// </summary>
public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } }
/// <summary>
/// Solver DRQ
/// </summary>
public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } }
/// <summary>
/// Statistics DRQ
/// </summary>
public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } }
/// <summary>
/// Tactic DRQ
/// </summary>
public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } }
/// <summary>
/// FixedPoint DRQ
/// </summary>
public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } }
/// <summary>
/// Optimize DRQ
/// </summary>
public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } }
internal long refCount = 0;
/// <summary>
/// Finalizer.
/// </summary>
@ -4984,22 +4871,6 @@ namespace Microsoft.Z3
public void Dispose()
{
// Console.WriteLine("Context Dispose from " + System.Threading.Thread.CurrentThread.ManagedThreadId);
AST_DRQ.Clear(this);
ASTMap_DRQ.Clear(this);
ASTVector_DRQ.Clear(this);
ApplyResult_DRQ.Clear(this);
FuncEntry_DRQ.Clear(this);
FuncInterp_DRQ.Clear(this);
Goal_DRQ.Clear(this);
Model_DRQ.Clear(this);
Params_DRQ.Clear(this);
ParamDescrs_DRQ.Clear(this);
Probe_DRQ.Clear(this);
Solver_DRQ.Clear(this);
Statistics_DRQ.Clear(this);
Tactic_DRQ.Clear(this);
Fixedpoint_DRQ.Clear(this);
Optimize_DRQ.Clear(this);
if (m_boolSort != null) m_boolSort.Dispose();
if (m_intSort != null) m_intSort.Dispose();
@ -5011,11 +4882,14 @@ namespace Microsoft.Z3
m_realSort = null;
m_stringSort = null;
m_charSort = null;
if (refCount == 0 && m_ctx != IntPtr.Zero)
if (m_ctx != IntPtr.Zero)
{
IntPtr ctx = m_ctx;
lock (this)
{
m_n_err_handler = null;
IntPtr ctx = m_ctx;
m_ctx = IntPtr.Zero;
}
if (!is_external)
Native.Z3_del_context(ctx);
}

25
src/api/dotnet/Fixedpoint.cs
View file

@ -318,31 +318,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_fixedpoint_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Fixedpoint_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_fixedpoint_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Fixedpoint_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_fixedpoint_dec_ref(Context.nCtx, o);
}
}
#endregion
}

50
src/api/dotnet/FuncInterp.cs
View file

@ -85,31 +85,18 @@ namespace Microsoft.Z3
#region Internal
internal Entry(Context ctx, IntPtr obj) : base(ctx, obj) { Debug.Assert(ctx != null); }
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_func_entry_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_func_entry_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.FuncEntry_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_func_entry_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.FuncEntry_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_func_entry_dec_ref(Context.nCtx, o);
}
}
#endregion
};
@ -190,31 +177,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_func_interp_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_func_interp_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.FuncInterp_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_func_interp_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.FuncInterp_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_func_interp_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/Goal.cs
View file

@ -254,31 +254,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_goal_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_goal_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Goal_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_goal_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Goal_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_goal_dec_ref(Context.nCtx, o);
}
}
#endregion

25
src/api/dotnet/Model.cs
View file

@ -304,31 +304,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_model_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_model_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Model_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_model_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Model_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_model_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/Optimize.cs
View file

@ -440,31 +440,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_optimize_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_optimize_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Optimize_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_optimize_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Optimize_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_optimize_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/ParamDescrs.cs
View file

@ -93,31 +93,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_param_descrs_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.ParamDescrs_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_param_descrs_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.ParamDescrs_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_param_descrs_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/Params.cs
View file

@ -149,31 +149,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_params_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_params_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Params_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_params_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Params_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_params_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/Probe.cs
View file

@ -70,31 +70,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_probe_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_probe_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Probe_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_probe_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Probe_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_probe_dec_ref(Context.nCtx, o);
}
}
#endregion
}

25
src/api/dotnet/Solver.cs
View file

@ -538,31 +538,18 @@ namespace Microsoft.Z3
this.BacktrackLevel = uint.MaxValue;
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_solver_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_solver_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Solver_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_solver_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Solver_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_solver_dec_ref(Context.nCtx, o);
}
}
private Status lboolToStatus(Z3_lbool r)

27
src/api/dotnet/Statistics.cs
View file

@ -19,8 +19,6 @@ Notes:
using System;
using System.Diagnostics;
namespace Microsoft.Z3
{
@ -189,31 +187,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_stats_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_stats_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Statistics_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_stats_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Statistics_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_stats_dec_ref(Context.nCtx, o);
}
}
#endregion
}

28
src/api/dotnet/Tactic.cs
View file

@ -107,34 +107,18 @@ namespace Microsoft.Z3
Debug.Assert(ctx != null);
}
/// <summary>
/// DecRefQueue
/// </summary>
internal class DecRefQueue : IDecRefQueue
{
public DecRefQueue() : base() { }
public DecRefQueue(uint move_limit) : base(move_limit) { }
internal override void IncRef(Context ctx, IntPtr obj)
{
Native.Z3_tactic_inc_ref(ctx.nCtx, obj);
}
internal override void DecRef(Context ctx, IntPtr obj)
{
Native.Z3_tactic_dec_ref(ctx.nCtx, obj);
}
};
internal override void IncRef(IntPtr o)
{
Context.Tactic_DRQ.IncAndClear(Context, o);
base.IncRef(o);
Native.Z3_tactic_inc_ref(Context.nCtx, o);
}
internal override void DecRef(IntPtr o)
{
Context.Tactic_DRQ.Add(o);
base.DecRef(o);
lock (Context)
{
if (Context.nCtx != IntPtr.Zero)
Native.Z3_tactic_dec_ref(Context.nCtx, o);
}
}
#endregion
}

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

@ -52,8 +52,6 @@ namespace Microsoft.Z3
if (m_ctx != null)
{
if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
GC.ReRegisterForFinalize(m_ctx);
m_ctx = null;
}
@ -76,16 +74,12 @@ namespace Microsoft.Z3
internal Z3Object(Context ctx)
{
Debug.Assert(ctx != null);
Interlocked.Increment(ref ctx.refCount);
m_ctx = ctx;
}
internal Z3Object(Context ctx, IntPtr obj)
{
Debug.Assert(ctx != null);
Interlocked.Increment(ref ctx.refCount);
m_ctx = ctx;
IncRef(obj);
m_n_obj = obj;