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 33 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 40 of file Probe.cs.
42 Debug.Assert(g !=
null);
44 Context.CheckContextMatch(g);
45 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
◆ this[Goal g]
Apply the probe to a goal.
Definition at line 52 of file Probe.cs.
55 Debug.Assert(g !=
null);