Z3
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
;
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
DecRefQueue() : base() { }
77
public
DecRefQueue(uint move_limit) : base(move_limit) { }
78
internal
override
void
IncRef(
Context
ctx, IntPtr obj)
79
{
80
Native.Z3_probe_inc_ref(ctx.nCtx, obj);
81
}
82
83
internal
override
void
DecRef(
Context
ctx, IntPtr obj)
84
{
85
Native.Z3_probe_dec_ref(ctx.nCtx, obj);
86
}
87
};
88
89
internal
override
void
IncRef(IntPtr o)
90
{
91
Context
.
Probe_DRQ
.IncAndClear(
Context
, o);
92
base.IncRef(o);
93
}
94
95
internal
override
void
DecRef(IntPtr o)
96
{
97
Context
.
Probe_DRQ
.Add(o);
98
base.DecRef(o);
99
}
100
#endregion
101
}
102
}
System
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
System.Diagnostics
Microsoft
System.Diagnostics.Contracts.ContractVerification
Definition:
DummyContracts.cs:38
System.Diagnostics.Contracts
Definition:
DummyContracts.cs:21
Microsoft.Z3.Probe.Apply
double Apply(Goal g)
Execute the probe over the goal.
Definition:
Probe.cs:41
Microsoft.Z3.IDecRefQueue
DecRefQueue interface
Definition:
IDecRefQueue.cs:32
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:4933
Microsoft.Z3.Z3Object
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition:
Z3Object.cs:33
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:31
Generated on Sat Nov 12 2016 22:01:04 for Z3 by
1.8.12