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.
More...
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 34 of file Probe.cs.
§ Apply()
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.
Definition at line 41 of file Probe.cs.
43 Contract.Requires(g != null);
45 Context.CheckContextMatch(g);
46 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
§ this[Goal g]
Apply the probe to a goal.
Definition at line 53 of file Probe.cs.