Probe Class Reference

Inheritance diagram for Probe:

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

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize () throws Z3Exception

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 ) throws Z3Exception

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__().

    {
        getContext().checkContextMatch(g);
        return Native.probeApply(getContext().nCtx(), getNativeObject(),
                g.getNativeObject());
    }