Z3
Public Member Functions
Probe Class Reference
+ Inheritance diagram for Probe:

Public Member Functions

double apply (Goal g)
 
- Public Member Functions inherited from Z3Object
void dispose ()
 
- Public Member Functions inherited from IDisposable
void dispose ()
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize ()
 

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-tactics)

in the SMT 2.0 front-end.

Definition at line 28 of file Probe.java.

Member Function Documentation

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

Referenced by Tactic.__call__().

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