From edeeded4eaa0aaf6b98f32113b4a0531ed2bc8d8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 11 Sep 2022 18:59:00 -0700 Subject: [PATCH] remove DecRefQueue, use Z3_enable_concurrent_dec_ref (#6332) 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). --- src/api/dotnet/AST.cs | 35 +++----- src/api/dotnet/ASTMap.cs | 25 ++---- src/api/dotnet/ASTVector.cs | 24 ++---- src/api/dotnet/ApplyResult.cs | 25 ++---- src/api/dotnet/Context.cs | 146 +++------------------------------- src/api/dotnet/Fixedpoint.cs | 25 ++---- src/api/dotnet/FuncInterp.cs | 50 +++--------- src/api/dotnet/Goal.cs | 27 ++----- src/api/dotnet/Model.cs | 27 ++----- src/api/dotnet/Optimize.cs | 25 ++---- src/api/dotnet/ParamDescrs.cs | 27 ++----- src/api/dotnet/Params.cs | 27 ++----- src/api/dotnet/Probe.cs | 25 ++---- src/api/dotnet/Solver.cs | 25 ++---- src/api/dotnet/Statistics.cs | 27 ++----- src/api/dotnet/Tactic.cs | 28 ++----- src/api/dotnet/Z3Object.cs | 6 -- 17 files changed, 114 insertions(+), 460 deletions(-) diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index 0afff2c42..48a7175eb 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -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) diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 0dde04411..ad3c47106 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -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 } diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index fcfa6bd65..777d7d56c 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -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 } diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs index 342bf3216..728fde3d5 100644 --- a/src/api/dotnet/ApplyResult.cs +++ b/src/api/dotnet/ApplyResult.cs @@ -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 } diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index af982b2d4..5aabcbc39 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -75,6 +75,7 @@ namespace Microsoft.Z3 foreach (KeyValuePair 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); - - /// - /// AST DRQ - /// - public IDecRefQueue AST_DRQ { get { return m_AST_DRQ; } } - - /// - /// ASTMap DRQ - /// - public IDecRefQueue ASTMap_DRQ { get { return m_ASTMap_DRQ; } } - - /// - /// ASTVector DRQ - /// - public IDecRefQueue ASTVector_DRQ { get { return m_ASTVector_DRQ; } } - - /// - /// ApplyResult DRQ - /// - public IDecRefQueue ApplyResult_DRQ { get { return m_ApplyResult_DRQ; } } - - /// - /// FuncEntry DRQ - /// - public IDecRefQueue FuncEntry_DRQ { get { return m_FuncEntry_DRQ; } } - - /// - /// FuncInterp DRQ - /// - public IDecRefQueue FuncInterp_DRQ { get { return m_FuncInterp_DRQ; } } - - /// - /// Goal DRQ - /// - public IDecRefQueue Goal_DRQ { get { return m_Goal_DRQ; } } - - /// - /// Model DRQ - /// - public IDecRefQueue Model_DRQ { get { return m_Model_DRQ; } } - - /// - /// Params DRQ - /// - public IDecRefQueue Params_DRQ { get { return m_Params_DRQ; } } - - /// - /// ParamDescrs DRQ - /// - public IDecRefQueue ParamDescrs_DRQ { get { return m_ParamDescrs_DRQ; } } - - /// - /// Probe DRQ - /// - public IDecRefQueue Probe_DRQ { get { return m_Probe_DRQ; } } - - /// - /// Solver DRQ - /// - public IDecRefQueue Solver_DRQ { get { return m_Solver_DRQ; } } - - /// - /// Statistics DRQ - /// - public IDecRefQueue Statistics_DRQ { get { return m_Statistics_DRQ; } } - - /// - /// Tactic DRQ - /// - public IDecRefQueue Tactic_DRQ { get { return m_Tactic_DRQ; } } - - /// - /// FixedPoint DRQ - /// - public IDecRefQueue Fixedpoint_DRQ { get { return m_Fixedpoint_DRQ; } } - - /// - /// Optimize DRQ - /// - public IDecRefQueue Optimize_DRQ { get { return m_Fixedpoint_DRQ; } } - - internal long refCount = 0; - /// /// Finalizer. /// @@ -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,13 +4882,16 @@ namespace Microsoft.Z3 m_realSort = null; m_stringSort = null; m_charSort = null; - if (refCount == 0 && m_ctx != IntPtr.Zero) + if (m_ctx != IntPtr.Zero) { - m_n_err_handler = null; IntPtr ctx = m_ctx; - m_ctx = IntPtr.Zero; - if (!is_external) - Native.Z3_del_context(ctx); + lock (this) + { + m_n_err_handler = null; + m_ctx = IntPtr.Zero; + } + if (!is_external) + Native.Z3_del_context(ctx); } else GC.ReRegisterForFinalize(this); diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 15560d829..2edae1e2a 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -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 } diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs index 6924049d3..fec6eab95 100644 --- a/src/api/dotnet/FuncInterp.cs +++ b/src/api/dotnet/FuncInterp.cs @@ -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 } diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index c096c0755..8183c7a79 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -252,33 +252,20 @@ namespace Microsoft.Z3 : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (byte)(models ? 1 : 0), (byte)(unsatCores ? 1 : 0), (byte)(proofs ? 1 : 0))) { 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 diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index c35c0a727..343b2beee 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -302,33 +302,20 @@ namespace Microsoft.Z3 : 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_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 } diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index ecd5e8e82..0694faabe 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -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 } diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs index fbfb9cd16..1975037e3 100644 --- a/src/api/dotnet/ParamDescrs.cs +++ b/src/api/dotnet/ParamDescrs.cs @@ -91,33 +91,20 @@ namespace Microsoft.Z3 : 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_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 } diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index e5926934a..64dd34968 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -147,33 +147,20 @@ namespace Microsoft.Z3 : base(ctx, Native.Z3_mk_params(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_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 } diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs index 5cdee79a2..e0457c2fe 100644 --- a/src/api/dotnet/Probe.cs +++ b/src/api/dotnet/Probe.cs @@ -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 } diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 52f2ad993..00b5117ea 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -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) diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index f6d72e0c7..1811951a2 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -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 } diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs index 96b6da170..d87b8bc48 100644 --- a/src/api/dotnet/Tactic.cs +++ b/src/api/dotnet/Tactic.cs @@ -107,34 +107,18 @@ namespace Microsoft.Z3 Debug.Assert(ctx != null); } - /// - /// DecRefQueue - /// - 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 } diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs index 432885b66..1affa9d17 100644 --- a/src/api/dotnet/Z3Object.cs +++ b/src/api/dotnet/Z3Object.cs @@ -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;