Z3 |

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.Diagnostics;
21 using System;
22 using System.Runtime.InteropServices;
23
24 namespace 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 class DecRefQueue : IDecRefQueue
74 {
75 public DecRefQueue() : base() { }
76 public DecRefQueue(uint move_limit) : base(move_limit) { }
77 internal override void IncRef(Context ctx, IntPtr obj)
78 {
79 Native.Z3_probe_inc_ref(ctx.nCtx, obj);
80 }
81
82 internal override void DecRef(Context ctx, IntPtr obj)
83 {
84 Native.Z3_probe_dec_ref(ctx.nCtx, obj);
85 }
86 };
87
88 internal override void IncRef(IntPtr o)
89 {
90 Context.Probe_DRQ.IncAndClear(Context, o);
91 base.IncRef(o);
92 }
93
94 internal override void DecRef(IntPtr o)
95 {
96 Context.Probe_DRQ.Add(o);
97 base.DecRef(o);
98 }
99 #endregion
100 }
101}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Microsoft.Z3.Context.Probe_DRQ
IDecRefQueue Probe_DRQ
Probe DRQ
Definition: Context.cs:4775
Microsoft.Z3.Goal
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:32
Microsoft.Z3.Probe
Probes are used to inspect a goal (aka problem) and collect information that may be used to decide wh...
Definition: Probe.cs:34
Microsoft.Z3.Probe.Apply
double Apply(Goal g)
Execute the probe over the goal.
Definition: Probe.cs:40
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Microsoft.Z3
Definition: AlgebraicNum.cs:27
Z3_mk_probe
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 ...