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 belongs

    Declaration

    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 by rhs.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs 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 by rhs.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs 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 by rhs.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs 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 by rhs.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs share the same context.

    Declaration

    Swift

    static func >= (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe

  • Return a probe that evaluates to “true” when lhs and rhs evaluate to true.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs share the same context.

    Declaration

    Swift

    static func == (lhs: Z3Probe, rhs: Z3Probe) -> Z3Probe

  • Return a probe that evaluates to “true” when lhs or rhs evaluate to true.

    Remark

    For probes, “true” is any value different from 0.0.

    Precondition

    lhs and rhs 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