A RetroSearch Logo

Home - News ( United States | United Kingdom | Italy | Germany ) - Football scores

Search Query:

Showing content from https://z3prover.github.io/api/html/class_microsoft_1_1_z3_1_1_probe.html below:

Z3: Probe Class Reference


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

);

45  return

Native.Z3_probe_apply(

Context

.nCtx, NativeObject, g.NativeObject);

Context Context

Access Context object

◆ this[Goal g]

Apply the probe to a goal.

Definition at line 51 of file Probe.cs.

55

Debug.Assert(g !=

null

);

double Apply(Goal g)

Execute the probe over the goal.


RetroSearch is an open source project built by @garambo | Open a GitHub Issue

Search and Browse the WWW like it's 1997 | Search results from DuckDuckGo

HTML: 3.2 | Encoding: UTF-8 | Version: 0.7.4