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.
41 {
42 Debug.Assert(g != null);
43
44 Context.CheckContextMatch(g);
45 return Native.Z3_probe_apply(Context.nCtx, NativeObject, g.NativeObject);
46 }
◆ this[Goal g]
Apply the probe to a goal.
Definition at line 51 of file Probe.cs.
52 {
53 get
54 {
55 Debug.Assert(g != null);
56
58 }
59 }
double Apply(Goal g)
Execute the probe over the goal.