Z3Tactic
public class Z3Tactic : Z3RefCountedObject
Basic building block for creating custom solvers for specific problem domains.
-
The context this
Z3Tactic
belongsDeclaration
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 andnext
to every subgoal produced byself
.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 ofother
applied to the given goal.Declaration
Swift
public func orElse(_ other: Z3Tactic) -> Z3Tactic
-
Return a tactic that applies
self
to a given goal and thenother
to every subgoal produced byself
. The subgoals are processed in parallel.Declaration
Swift
public func parallelAndThen(_ other: Z3Tactic) -> Z3Tactic
-
Return a tactic that applies
self
to a given goal formilliseconds
. Ifself
does not terminate inmilliseconds
, then it fails.Declaration
Swift
public func tryFor(milliseconds: UInt32) -> Z3Tactic
-
Return a tactic that applies
self
to a given goal is the probeprobe
evaluates to true. Ifprobe
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 probeprobe
evaluates to true, andother
ifprobe
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 iterationsmax
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
togoal
, optionally using a set of parametersparams
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