Module Z3.Probe

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-tactic) 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".