Z3
ApplyResult.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  ApplyResult.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Result object for tactic applications
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
22 
23 namespace Microsoft.Z3
24 {
29  [ContractVerification(true)]
30  public class ApplyResult : Z3Object
31  {
35  public uint NumSubgoals
36  {
37  get { return Native.Z3_apply_result_get_num_subgoals(Context.nCtx, NativeObject); }
38  }
39 
43  public Goal[] Subgoals
44  {
45  get
46  {
47  Contract.Ensures(Contract.Result<Goal[]>() != null);
48  Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
49 
50  uint n = NumSubgoals;
51  Goal[] res = new Goal[n];
52  for (uint i = 0; i < n; i++)
53  res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
54  return res;
55  }
56  }
57 
63  public Model ConvertModel(uint i, Model m)
64  {
65  Contract.Requires(m != null);
66  Contract.Ensures(Contract.Result<Model>() != null);
67 
68  return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject));
69  }
70 
74  public override string ToString()
75  {
76  return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
77  }
78 
79  #region Internal
80  internal ApplyResult(Context ctx, IntPtr obj)
81  : base(ctx, obj)
82  {
83  Contract.Requires(ctx != null);
84  }
85 
86  internal class DecRefQueue : IDecRefQueue
87  {
88  public DecRefQueue() : base() { }
89  public DecRefQueue(uint move_limit) : base(move_limit) { }
90  internal override void IncRef(Context ctx, IntPtr obj)
91  {
92  Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
93  }
94 
95  internal override void DecRef(Context ctx, IntPtr obj)
96  {
97  Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
98  }
99  };
100 
101  internal override void IncRef(IntPtr o)
102  {
103  Context.ApplyResult_DRQ.IncAndClear(Context, o);
104  base.IncRef(o);
105  }
106 
107  internal override void DecRef(IntPtr o)
108  {
109  Context.ApplyResult_DRQ.Add(o);
110  base.DecRef(o);
111  }
112  #endregion
113  }
114 }
override string ToString()
A string representation of the ApplyResult.
Definition: ApplyResult.cs:74
Model ConvertModel(uint i, Model m)
Convert a model for the subgoal i into a model for the original goal g, that the ApplyResult was obt...
Definition: ApplyResult.cs:63
IDecRefQueue ApplyResult_DRQ
ApplyResult DRQ
Definition: Context.cs:4898
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
DecRefQueue interface
Definition: IDecRefQueue.cs:32
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31