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.
More...
Data Structures | |
class | DecRefQueue |
Public Member Functions | |
double | Apply (Goal g) |
Execute the probe over the goal. | |
Properties | |
double | this[Goal g] [get] |
Apply the probe to a goal. |
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.
Execute the probe over the goal.
Definition at line 41 of file Probe.cs.
{
Contract.Requires(g != null);
Context.CheckContextMatch(g);
return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
}