Z3 |

Public Member Functions
Probe Class Reference
Inheritance diagram for Probe:

## Public Member Functions
double | apply (Goal g)

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## 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 28 of file Probe.java.

## 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.

Exceptions

  Z3Exception |

Definition at line 36 of file Probe.java.

37 {
38 getContext().checkContextMatch(g);
39 return Native.probeApply(getContext().nCtx(), getNativeObject(),
40 g.getNativeObject());
41 }

Referenced by Tactic.__call__().