Z3Probe
public class Z3Probe : Z3RefCountedObject
A class describing a probe in Z3. 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 context this
Z3ParserContext
belongsDeclaration
Swift
public let context: Z3Context
-
Execute the probe over the goal. The probe always produce a double value. “Boolean” probes return 0.0 for false, and a value different from 0.0 for true.
Declaration
Swift
public func apply(over goal: Z3Goal) -> Double
-
Return a tactic that fails if this probe evaluates to false.
Declaration
Swift
public func tacticForFailure() -> Z3Tactic
-
Return a probe that evaluates to “true” when the value returned by
lhs
is less than the value returned byrhs
.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func < (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when the value returned by
lhs
is less than or equal to the value returned byrhs
.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func <= (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when the value returned by
lhs
is greater than the value returned byrhs
.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func > (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when the value returned by
lhs
is greater than or equal to the value returned byrhs
.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func >= (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when
lhs
andrhs
evaluate to true.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func == (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when
lhs
orrhs
evaluate to true.Remark
For probes, “true” is any value different from 0.0.Precondition
lhs
andrhs
share the same context.Declaration
Swift
static func || (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe
-
Return a probe that evaluates to “true” when
probe
does not evaluate to true.Remark
For probes, “true” is any value different from 0.0.Declaration
Swift
prefix static func ! (probe: Z3Probe) -> Z3Probe