Z3
src/api/dotnet/Probe.cs
Go to the documentation of this file.
00001 /*++
00002 Copyright (c) 2012 Microsoft Corporation
00003 
00004 Module Name:
00005 
00006     Probe.cs
00007 
00008 Abstract:
00009 
00010     Z3 Managed API: Probes
00011 
00012 Author:
00013 
00014     Christoph Wintersteiger (cwinter) 2012-03-21
00015 
00016 Notes:
00017     
00018 --*/
00019 
00020 using System;
00021 using System.Runtime.InteropServices;
00022 using System.Diagnostics.Contracts;
00023 
00024 namespace Microsoft.Z3
00025 {
00033     [ContractVerification(true)]
00034     public class Probe : Z3Object
00035     {
00041         public double Apply(Goal g)
00042         {
00043             Contract.Requires(g != null);
00044 
00045             Context.CheckContextMatch(g);
00046             return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
00047         }
00048 
00052         public double this[Goal g]
00053         {
00054             get
00055             {
00056                 Contract.Requires(g != null);
00057 
00058                 return Apply(g);
00059             }
00060         }
00061 
00062         #region Internal
00063         internal Probe(Context ctx, IntPtr obj)
00064             : base(ctx, obj)
00065         {
00066             Contract.Requires(ctx != null);
00067         }
00068         internal Probe(Context ctx, string name)
00069             : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
00070         {
00071             Contract.Requires(ctx != null);
00072         }
00073 
00074         internal class DecRefQueue : IDecRefQueue
00075         {
00076             public override void IncRef(Context ctx, IntPtr obj)
00077             {
00078                 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
00079             }
00080 
00081             public override void DecRef(Context ctx, IntPtr obj)
00082             {
00083                 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
00084             }
00085         };
00086 
00087         internal override void IncRef(IntPtr o)
00088         {
00089             Context.Probe_DRQ.IncAndClear(Context, o);
00090             base.IncRef(o);
00091         }
00092 
00093         internal override void DecRef(IntPtr o)
00094         {
00095             Context.Probe_DRQ.Add(o);
00096             base.DecRef(o);
00097         }
00098         #endregion
00099     }
00100 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines