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.

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

Referenced by Tactic.__call__().