diff --git a/src/api/dotnet/AST.cs b/src/api/dotnet/AST.cs index d3b31a325..552fd6def 100644 --- a/src/api/dotnet/AST.cs +++ b/src/api/dotnet/AST.cs @@ -213,6 +213,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/ASTMap.cs b/src/api/dotnet/ASTMap.cs index 9de3b8358..fa8070908 100644 --- a/src/api/dotnet/ASTMap.cs +++ b/src/api/dotnet/ASTMap.cs @@ -128,6 +128,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_ast_map_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/ASTVector.cs b/src/api/dotnet/ASTVector.cs index bbba3de90..be5172f97 100644 --- a/src/api/dotnet/ASTVector.cs +++ b/src/api/dotnet/ASTVector.cs @@ -105,6 +105,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_ast_vector_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/ApplyResult.cs b/src/api/dotnet/ApplyResult.cs index d64dccb4b..4ff8851af 100644 --- a/src/api/dotnet/ApplyResult.cs +++ b/src/api/dotnet/ApplyResult.cs @@ -85,6 +85,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_apply_result_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs index 65ec87bc6..94baea35a 100644 --- a/src/api/dotnet/Context.cs +++ b/src/api/dotnet/Context.cs @@ -4396,20 +4396,20 @@ namespace Microsoft.Z3 } readonly private AST.DecRefQueue m_AST_DRQ = new AST.DecRefQueue(); - readonly private ASTMap.DecRefQueue m_ASTMap_DRQ = new ASTMap.DecRefQueue(); - readonly private ASTVector.DecRefQueue m_ASTVector_DRQ = new ASTVector.DecRefQueue(); - readonly private ApplyResult.DecRefQueue m_ApplyResult_DRQ = new ApplyResult.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(); readonly private FuncInterp.DecRefQueue m_FuncInterp_DRQ = new FuncInterp.DecRefQueue(); - readonly private Goal.DecRefQueue m_Goal_DRQ = new Goal.DecRefQueue(); - readonly private Model.DecRefQueue m_Model_DRQ = new Model.DecRefQueue(); + 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(); readonly private ParamDescrs.DecRefQueue m_ParamDescrs_DRQ = new ParamDescrs.DecRefQueue(); readonly private Probe.DecRefQueue m_Probe_DRQ = new Probe.DecRefQueue(); - readonly private Solver.DecRefQueue m_Solver_DRQ = new Solver.DecRefQueue(); - readonly private Statistics.DecRefQueue m_Statistics_DRQ = new Statistics.DecRefQueue(); + 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(); - readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(); + readonly private Fixedpoint.DecRefQueue m_Fixedpoint_DRQ = new Fixedpoint.DecRefQueue(10); internal AST.DecRefQueue AST_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_AST_DRQ; } } internal ASTMap.DecRefQueue ASTMap_DRQ { get { Contract.Ensures(Contract.Result() != null); return m_ASTMap_DRQ; } } diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs index 3f40b220b..37ae1b110 100644 --- a/src/api/dotnet/Fixedpoint.cs +++ b/src/api/dotnet/Fixedpoint.cs @@ -335,6 +335,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_fixedpoint_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/FuncInterp.cs b/src/api/dotnet/FuncInterp.cs index a6628af28..488abb780 100644 --- a/src/api/dotnet/FuncInterp.cs +++ b/src/api/dotnet/FuncInterp.cs @@ -91,6 +91,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_func_entry_inc_ref(ctx.nCtx, obj); @@ -197,6 +199,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_func_interp_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Goal.cs b/src/api/dotnet/Goal.cs index b108683c9..13c98f932 100644 --- a/src/api/dotnet/Goal.cs +++ b/src/api/dotnet/Goal.cs @@ -219,6 +219,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_goal_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/IDecRefQueue.cs b/src/api/dotnet/IDecRefQueue.cs index d741a8f05..a69e28ff2 100644 --- a/src/api/dotnet/IDecRefQueue.cs +++ b/src/api/dotnet/IDecRefQueue.cs @@ -40,7 +40,12 @@ namespace Microsoft.Z3 readonly internal protected Object m_lock = new Object(); readonly internal protected List m_queue = new List(); - internal const uint m_move_limit = 1024; + internal uint m_move_limit; + + public IDecRefQueue(uint move_limit = 1024) + { + m_move_limit = move_limit; + } public abstract void IncRef(Context ctx, IntPtr obj); public abstract void DecRef(Context ctx, IntPtr obj); diff --git a/src/api/dotnet/Model.cs b/src/api/dotnet/Model.cs index 5c0bc24f8..9cff1e667 100644 --- a/src/api/dotnet/Model.cs +++ b/src/api/dotnet/Model.cs @@ -291,6 +291,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_model_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/ParamDescrs.cs b/src/api/dotnet/ParamDescrs.cs index acfae1b85..a08e11859 100644 --- a/src/api/dotnet/ParamDescrs.cs +++ b/src/api/dotnet/ParamDescrs.cs @@ -87,6 +87,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_param_descrs_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Params.cs b/src/api/dotnet/Params.cs index 9a814b2ec..de2287af5 100644 --- a/src/api/dotnet/Params.cs +++ b/src/api/dotnet/Params.cs @@ -140,6 +140,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_params_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Probe.cs b/src/api/dotnet/Probe.cs index 1ae7ee064..e8907b294 100644 --- a/src/api/dotnet/Probe.cs +++ b/src/api/dotnet/Probe.cs @@ -73,6 +73,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_probe_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs index 9de515e86..2e12a5842 100644 --- a/src/api/dotnet/Solver.cs +++ b/src/api/dotnet/Solver.cs @@ -328,6 +328,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_solver_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Statistics.cs b/src/api/dotnet/Statistics.cs index 408995140..81240e2c0 100644 --- a/src/api/dotnet/Statistics.cs +++ b/src/api/dotnet/Statistics.cs @@ -189,6 +189,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_stats_inc_ref(ctx.nCtx, obj); diff --git a/src/api/dotnet/Tactic.cs b/src/api/dotnet/Tactic.cs index eb4ef085c..be79c2a43 100644 --- a/src/api/dotnet/Tactic.cs +++ b/src/api/dotnet/Tactic.cs @@ -114,6 +114,8 @@ namespace Microsoft.Z3 internal class DecRefQueue : IDecRefQueue { + public DecRefQueue() : base() { } + public DecRefQueue(uint move_limit) : base(move_limit) { } public override void IncRef(Context ctx, IntPtr obj) { Native.Z3_tactic_inc_ref(ctx.nCtx, obj);