Z3 |

Data Structures | Public Member Functions | Properties
Probe Class Reference

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures `Context.NumProbes` and `Context.ProbeNames`. It may also be obtained using the command `(help-tactic)` in the SMT 2.0 front-end. More...

Inheritance diagram for Probe:

## Data Structures
class | DecRefQueue

## Public Member Functions
double | Apply (Goal g)
| Execute the probe over the goal. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
double | this[Goal g]`[get]`
| Apply the probe to a goal. More...

## Detailed Description

Probes are used to inspect a goal (aka problem) and collect information that may be used to decide which solver and/or preprocessing step will be used. The complete list of probes may be obtained using the procedures `Context.NumProbes` and `Context.ProbeNames`. It may also be obtained using the command `(help-tactic)` in the SMT 2.0 front-end.

Definition at line 33 of file Probe.cs.

## Member Function Documentation

## ◆ Apply()

double Apply | ( | Goal | g | ) |
| inline

Execute the probe over the goal.

Returns
  A probe always produce a double value. "Boolean" probes return 0.0 for false, and a value different from 0.0 for true.

Definition at line 40 of file Probe.cs.

41 {
42 Debug.Assert(g != null);
43
44 Context.CheckContextMatch(g);
45 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
46 }

## Property Documentation

## ◆ this[Goal g]

double this[Goal g]
| get

Apply the probe to a goal.

Definition at line 51 of file Probe.cs.

52 {
53 get
54 {
55 Debug.Assert(g != null);
56
57 return Apply(g);
58 }
59 }
Microsoft.Z3.Probe.Apply
double Apply(Goal g)
Execute the probe over the goal.
Definition: Probe.cs:40