module Probe: sig
.. end
Probes
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.
type
probe
val apply : probe -> Goal.goal -> float
Execute the probe over the goal.
Returns A probe always produce a float value.
"Boolean" probes return 0.0 for false, and a value different from 0.0 for true.
val get_num_probes : context -> int
The number of supported Probes.
val get_probe_names : context -> string list
The names of all supported Probes.
val get_probe_description : context -> string -> string
Returns a string containing a description of the probe with the given name.
val mk_probe : context -> string -> probe
Creates a new Probe.
val const : context -> float -> probe
Create a probe that always evaluates to a float value.
val lt : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when the value returned by the first argument
is less than the value returned by second argument
val gt : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when the value returned by the first argument
is greater than the value returned by second argument
val le : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when the value returned by the first argument
is less than or equal the value returned by second argument
val ge : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when the value returned by the first argument
is greater than or equal the value returned by second argument
val eq : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when the value returned by the first argument
is equal the value returned by second argument
val and_ : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when both of two probes evaluate to "true".
val or_ : context -> probe -> probe -> probe
Create a probe that evaluates to "true" when either of two probes evaluates to "true".
val not_ : context -> probe -> probe
Create a probe that evaluates to "true" when another probe does not evaluate to "true".