Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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]
53  {
54  get
55  {
56  Contract.Requires(g != null);
57 
58  return Apply(g);
59  }
60  }
61 
62  #region Internal
63  internal Probe(Context ctx, IntPtr obj)
64  : base(ctx, obj)
65  {
66  Contract.Requires(ctx != null);
67  }
68  internal Probe(Context ctx, string name)
69  : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
70  {
71  Contract.Requires(ctx != null);
72  }
73 
74  internal class DecRefQueue : IDecRefQueue
75  {
76  public override void IncRef(Context ctx, IntPtr obj)
77  {
78  Native.Z3_probe_inc_ref(ctx.nCtx, obj);
79  }
80 
81  public override void DecRef(Context ctx, IntPtr obj)
82  {
83  Native.Z3_probe_dec_ref(ctx.nCtx, obj);
84  }
85  };
86 
87  internal override void IncRef(IntPtr o)
88  {
89  Context.Probe_DRQ.IncAndClear(Context, o);
90  base.IncRef(o);
91  }
92 
93  internal override void DecRef(IntPtr o)
94  {
95  Context.Probe_DRQ.Add(o);
96  base.DecRef(o);
97  }
98  #endregion
99  }
100 }
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
static double Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2)
Definition: Native.cs:4785
double Apply(Goal g)
Execute the probe over the goal.
Definition: Probe.cs:41
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
Z3_probe Z3_API Z3_mk_probe(__in Z3_context c, __in Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31