20using System.Diagnostics;
36 get {
return Native.Z3_apply_result_get_num_subgoals(
Context.nCtx, NativeObject); }
49 for (uint i = 0; i < n; i++)
50 res[i] =
new Goal(
Context, Native.Z3_apply_result_get_subgoal(
Context.nCtx, NativeObject, i));
60 return Native.Z3_apply_result_to_string(
Context.nCtx, NativeObject);
67 Debug.Assert(ctx !=
null);
70 internal class DecRefQueue : IDecRefQueue
72 public DecRefQueue() : base() { }
73 public DecRefQueue(uint move_limit) : base(move_limit) { }
74 internal override void IncRef(Context ctx, IntPtr obj)
76 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
79 internal override void DecRef(Context ctx, IntPtr obj)
81 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
85 internal override void IncRef(IntPtr o)
91 internal override void DecRef(IntPtr o)
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
uint NumSubgoals
The number of Subgoals.
override string ToString()
A string representation of the ApplyResult.
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
The main interaction with Z3 happens via the Context.
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Internal base class for interfacing with native Z3 objects. Should not be used externally.