Z3
ApplyResult.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 ApplyResult.cs
7
8Abstract:
9
10 Z3 Managed API: Result object for tactic applications
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22
23namespace Microsoft.Z3
24{
29 public class ApplyResult : Z3Object
30 {
34 public uint NumSubgoals
35 {
36 get { return Native.Z3_apply_result_get_num_subgoals(Context.nCtx, NativeObject); }
37 }
38
42 public Goal[] Subgoals
43 {
44 get
45 {
46
47 uint n = NumSubgoals;
48 Goal[] res = new Goal[n];
49 for (uint i = 0; i < n; i++)
50 res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
51 return res;
52 }
53 }
54
58 public override string ToString()
59 {
60 return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
61 }
62
63 #region Internal
64 internal ApplyResult(Context ctx, IntPtr obj)
65 : base(ctx, obj)
66 {
67 Debug.Assert(ctx != null);
68 }
69
70 internal class DecRefQueue : IDecRefQueue
71 {
72 public DecRefQueue() : base() { }
73 public DecRefQueue(uint move_limit) : base(move_limit) { }
74 internal override void IncRef(Context ctx, IntPtr obj)
75 {
76 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
77 }
78
79 internal override void DecRef(Context ctx, IntPtr obj)
80 {
81 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
82 }
83 };
84
85 internal override void IncRef(IntPtr o)
86 {
87 Context.ApplyResult_DRQ.IncAndClear(Context, o);
88 base.IncRef(o);
89 }
90
91 internal override void DecRef(IntPtr o)
92 {
93 Context.ApplyResult_DRQ.Add(o);
94 base.DecRef(o);
95 }
96 #endregion
97 }
98}
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:35
override string ToString()
A string representation of the ApplyResult.
Definition: ApplyResult.cs:58
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
Definition: ApplyResult.cs:43
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4740
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33