Z3
Loading...
Searching...
No Matches
src
api
dotnet
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
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
}
Microsoft.Z3.Context
The main interaction with Z3 happens via the Context.
Definition
Context.cs:34
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.Z3Object.Context
Context Context
Access Context object.
Definition
Z3Object.cs:111
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 ...
Microsoft.Z3
Definition
AlgebraicNum.cs:27
Generated on Sat Dec 20 2025 19:33:21 for Z3 by
1.9.8