Z3
 
Loading...
Searching...
No Matches
Probe.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Probe.cs
7
8Abstract:
9
10 Z3 Managed API: Probes
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-21
15
16Notes:
17
18--*/
19
20using System.Diagnostics;
21using System;
22using System.Runtime.InteropServices;
23
24namespace Microsoft.Z3
25{
33 public class Probe : Z3Object
34 {
40 public double Apply(Goal g)
41 {
42 Debug.Assert(g != null);
43
44 Context.CheckContextMatch(g);
45 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
46 }
47
51 public double this[Goal g]
52 {
53 get
54 {
55 Debug.Assert(g != null);
56
57 return Apply(g);
58 }
59 }
60
61 #region Internal
62 internal Probe(Context ctx, IntPtr obj)
63 : base(ctx, obj)
64 {
65 Debug.Assert(ctx != null);
66 }
67 internal Probe(Context ctx, string name)
68 : base(ctx, Native.Z3_mk_probe(ctx.nCtx, name))
69 {
70 Debug.Assert(ctx != null);
71 }
72
73 internal override void IncRef(IntPtr o)
74 {
75 Native.Z3_probe_inc_ref(Context.nCtx, o);
76 }
77
78 internal override void DecRef(IntPtr o)
79 {
80 lock (Context)
81 {
82 if (Context.nCtx != IntPtr.Zero)
83 Native.Z3_probe_dec_ref(Context.nCtx, o);
84 }
85 }
86 #endregion
87 }
88}
The main interaction with Z3 happens via the Context.
Definition Context.cs:34
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition Goal.cs:32
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition Probe.cs:34
double Apply(Goal g)
Execute the probe over the goal.
Definition Probe.cs:40
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition Z3Object.cs:33
Context Context
Access Context object.
Definition Z3Object.cs:111
Z3_probe Z3_API Z3_mk_probe(Z3_context c, Z3_string name)
Return a probe associated with the given name. The complete list of probes may be obtained using the ...