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 |
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.
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)); }
double apply | ( | Goal | g | ) | throws Z3Exception [inline] |
Execute the probe over the goal.
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); }