Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Probe.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Probe.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Probes
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Runtime.InteropServices;
22 using System.Diagnostics.Contracts;
23 
24 namespace Microsoft.Z3
25 {
33  [ContractVerification(true)]
34  public class Probe : Z3Object
35  {
41  public double Apply(Goal g)
42  {
43  Contract.Requires(g != null);
44 
45  Context.CheckContextMatch(g);
46  return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
47  }
48 
52  public double this[Goal g] { get {
53  Contract.Requires(g != null);
54 
55  return Apply(g); } }
56 
57  #region Internal
58  internal Probe(Context ctx, IntPtr obj)
59  : base(ctx, obj)
60  {
61  Contract.Requires(ctx != null);
62  }
63  internal Probe(Context ctx, string name)
64  : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
65  {
66  Contract.Requires(ctx != null);
67  }
68 
69  internal class DecRefQueue : Z3.DecRefQueue
70  {
71  public override void IncRef(Context ctx, IntPtr obj)
72  {
73  Native.Z3_probe_inc_ref(ctx.nCtx, obj);
74  }
75 
76  public override void DecRef(Context ctx, IntPtr obj)
77  {
78  Native.Z3_probe_dec_ref(ctx.nCtx, obj);
79  }
80  };
81 
82  internal override void IncRef(IntPtr o)
83  {
84  Context.Probe_DRQ.IncAndClear(Context, o);
85  base.IncRef(o);
86  }
87 
88  internal override void DecRef(IntPtr o)
89  {
90  Context.Probe_DRQ.Add(o);
91  base.DecRef(o);
92  }
93  #endregion
94  }
95 }