mirror of
https://github.com/Z3Prover/z3
synced 2025-06-02 12:21:21 +00:00
edeeded4ea
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).
85 lines
2 KiB
C#
85 lines
2 KiB
C#
/*++
|
|
Copyright (c) 2012 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
ApplyResult.cs
|
|
|
|
Abstract:
|
|
|
|
Z3 Managed API: Result object for tactic applications
|
|
|
|
Author:
|
|
|
|
Christoph Wintersteiger (cwinter) 2012-03-21
|
|
|
|
Notes:
|
|
|
|
--*/
|
|
|
|
using System.Diagnostics;
|
|
using System;
|
|
|
|
namespace Microsoft.Z3
|
|
{
|
|
/// <summary>
|
|
/// ApplyResult objects represent the result of an application of a
|
|
/// tactic to a goal. It contains the subgoals that were produced.
|
|
/// </summary>
|
|
public class ApplyResult : Z3Object
|
|
{
|
|
/// <summary>
|
|
/// The number of Subgoals.
|
|
/// </summary>
|
|
public uint NumSubgoals
|
|
{
|
|
get { return Native.Z3_apply_result_get_num_subgoals(Context.nCtx, NativeObject); }
|
|
}
|
|
|
|
/// <summary>
|
|
/// Retrieves the subgoals from the ApplyResult.
|
|
/// </summary>
|
|
public Goal[] Subgoals
|
|
{
|
|
get
|
|
{
|
|
|
|
uint n = NumSubgoals;
|
|
Goal[] res = new Goal[n];
|
|
for (uint i = 0; i < n; i++)
|
|
res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
|
|
return res;
|
|
}
|
|
}
|
|
|
|
/// <summary>
|
|
/// A string representation of the ApplyResult.
|
|
/// </summary>
|
|
public override string ToString()
|
|
{
|
|
return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
|
|
}
|
|
|
|
#region Internal
|
|
internal ApplyResult(Context ctx, IntPtr obj)
|
|
: base(ctx, obj)
|
|
{
|
|
Debug.Assert(ctx != null);
|
|
}
|
|
|
|
internal override void IncRef(IntPtr o)
|
|
{
|
|
Native.Z3_apply_result_inc_ref(Context.nCtx, o);
|
|
}
|
|
|
|
internal override void DecRef(IntPtr o)
|
|
{
|
|
lock(Context)
|
|
{
|
|
if (Context.nCtx != IntPtr.Zero)
|
|
Native.Z3_apply_result_dec_ref(Context.nCtx, o);
|
|
}
|
|
}
|
|
#endregion
|
|
}
|
|
}
|