Z3Tactic

public class Z3Tactic : Z3RefCountedObject

Basic building block for creating custom solvers for specific problem domains.

  • The context this Z3Tactic belongs

    Declaration

    Swift

    public let context: Z3Context

  • Return a string containing a description of parameters accepted by this tactic.

    Declaration

    Swift

    public var help: String { get }

  • Return the parameter description set for this tactic object.

    Declaration

    Swift

    public func getParamDescrs() -> Z3ParamDescrs

  • Return a tactic that applies self to a given goal and next to every subgoal produced by self.

    Declaration

    Swift

    public func andThen(_ next: Z3Tactic) -> Z3Tactic

  • Return a tactic that first applies self to a given goal, if it fails then returns the result of other applied to the given goal.

    Declaration

    Swift

    public func orElse(_ other: Z3Tactic) -> Z3Tactic

  • Return a tactic that applies self to a given goal and then other to every subgoal produced by self. The subgoals are processed in parallel.

    Declaration

    Swift

    public func parallelAndThen(_ other: Z3Tactic) -> Z3Tactic

  • Return a tactic that applies self to a given goal for milliseconds. If self does not terminate in milliseconds, then it fails.

    Declaration

    Swift

    public func tryFor(milliseconds: UInt32) -> Z3Tactic

  • Return a tactic that applies self to a given goal is the probe probe evaluates to true. If probe evaluates to false, then the new tactic behaves like the skip tactic.

    Declaration

    Swift

    public func when(_ probe: Z3Probe) -> Z3Tactic

  • Return a tactic that applies self to a given goal if the probe probe evaluates to true, and other if probe evaluates to false.

    Declaration

    Swift

    public func conditional(ifProbe probe: Z3Probe, else other: Z3Tactic) -> Z3Tactic

  • Return a tactic that keeps applying self until the goal is not modified anymore or the maximum number of iterations max is reached.

    Declaration

    Swift

    public func repeating(max: UInt32) -> Z3Tactic

  • Return a tactic that applies self using the given set of parameters.

    Declaration

    Swift

    public func usingParams(_ params: Z3Params) -> Z3Tactic

  • Apply tactic self to goal, optionally using a set of parameters params if non-nil.

    Declaration

    Swift

    public func apply(to goal: Z3Goal, params: Z3Params? = nil) -> Z3ApplyResult

  • Return a tactic that applies the given tactics in parallel.

    Precondition

    tactics.count > 0

    Precondition

    All tactics belong to the same context.

    Declaration

    Swift

    public static func parallelOr(_ tactics: [Z3Tactic]) -> Z3Tactic