Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
Probe Class Reference
+ Inheritance diagram for Probe:

Public Member Functions

double apply (Goal g) throws Z3Exception

Package Functions

 Probe (Context ctx, long obj) throws Z3Exception
 Probe (Context ctx, String name) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) 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.


Constructor & Destructor Documentation

Probe ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 44 of file Probe.java.

    {
        super(ctx, obj);
    }
Probe ( Context  ctx,
String  name 
) throws Z3Exception [inline, package]

Definition at line 49 of file Probe.java.

    {
        super(ctx, Native.mkProbe(ctx.nCtx(), name));
    }

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());
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 60 of file Probe.java.

    {
        getContext().probe_DRQ().add(o);
        super.decRef(o);
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 54 of file Probe.java.

    {
        getContext().probe_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines