Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00029 [ContractVerification(true)]
00030 public class ApplyResult : Z3Object
00031 {
00035 public uint NumSubgoals
00036 {
00037 get { return Native.Z3_apply_result_get_num_subgoals(Context.nCtx, NativeObject); }
00038 }
00039
00043 public Goal[] Subgoals
00044 {
00045 get
00046 {
00047 Contract.Ensures(Contract.Result<Goal[]>() != null);
00048 Contract.Ensures(Contract.Result<Goal[]>().Length == this.NumSubgoals);
00049
00050 uint n = NumSubgoals;
00051 Goal[] res = new Goal[n];
00052 for (uint i = 0; i < n; i++)
00053 res[i] = new Goal(Context, Native.Z3_apply_result_get_subgoal(Context.nCtx, NativeObject, i));
00054 return res;
00055 }
00056 }
00057
00063 public Model ConvertModel(uint i, Model m)
00064 {
00065 Contract.Requires(m != null);
00066 Contract.Ensures(Contract.Result<Model>() != null);
00067
00068 return new Model(Context, Native.Z3_apply_result_convert_model(Context.nCtx, NativeObject, i, m.NativeObject));
00069 }
00070
00074 public override string ToString()
00075 {
00076 return Native.Z3_apply_result_to_string(Context.nCtx, NativeObject);
00077 }
00078
00079 #region Internal
00080 internal ApplyResult(Context ctx, IntPtr obj)
00081 : base(ctx, obj)
00082 {
00083 Contract.Requires(ctx != null);
00084 }
00085
00086 internal class DecRefQueue : IDecRefQueue
00087 {
00088 public override void IncRef(Context ctx, IntPtr obj)
00089 {
00090 Native.Z3_apply_result_inc_ref(ctx.nCtx, obj);
00091 }
00092
00093 public override void DecRef(Context ctx, IntPtr obj)
00094 {
00095 Native.Z3_apply_result_dec_ref(ctx.nCtx, obj);
00096 }
00097 };
00098
00099 internal override void IncRef(IntPtr o)
00100 {
00101 Context.ApplyResult_DRQ.IncAndClear(Context, o);
00102 base.IncRef(o);
00103 }
00104
00105 internal override void DecRef(IntPtr o)
00106 {
00107 Context.ApplyResult_DRQ.Add(o);
00108 base.DecRef(o);
00109 }
00110 #endregion
00111 }
00112 }