Z3
src/api/dotnet/ApplyResult.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     ApplyResult.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Result object for tactic applications
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
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 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines