Z3Optimize

public class Z3Optimize : Z3RefCountedObject

Object for managing optimization context.

  • The context this Z3Optimize belongs

    Declaration

    Swift

    public let context: Z3Context

  • Assert hard constraint to the optimization context.

    Seealso

    assertSoft

    Seealso

    assertAndTrack

    Declaration

    Swift

    public func assert(_ a: Z3Bool)

  • Assert hard constraints to the optimization context.

    Seealso

    assertSoft

    Seealso

    assertAndTrack

    Declaration

    Swift

    public func assert(_ constraints: [Z3Bool])

  • Assert tracked hard constraint to the optimization context.

    Seealso

    assert

    Seealso

    assertSoft

    Declaration

    Swift

    public func assertAndTrack(_ a: Z3Bool, _ t: Z3Bool)

  • Assert soft constraint to the optimization context.

    Seealso

    assert

    Seealso

    assertAndTrack

    Declaration

    Swift

    public func assertSoft(_ a: Z3Bool, weight: String, id: Z3Symbol? = nil) -> UInt32

    Parameters

    a

    formula
    weight

    a weight, penalty for violating soft constraint. Negative weights convert into rewards.
    id

    optional identifier to group soft constraints

  • Add a maximization constraint.

    Seealso

    minimize()

    Declaration

    Swift

    public func maximize<T>(_ a: Z3Ast<T>) -> UInt32 where T : BitVectorSort

  • Add a maximization constraint.

    Seealso

    minimize()

    Declaration

    Swift

    public func maximize<T>(_ a: Z3Ast<T>) -> UInt32 where T : ArithmeticSort

  • Add a maximization constraint.

    AST must be of bit vector, int, or real type.

    Seealso

    minimize()

    Seealso

    minimizeAny()

    Declaration

    Swift

    public func maximizeAny(_ a: AnyZ3Ast) -> UInt32

  • Add a minimization constraint.

    Seealso

    minimize()

    Seealso

    minimizeAny()

    Declaration

    Swift

    public func minimize<T>(_ a: Z3Ast<T>) -> UInt32 where T : BitVectorSort

  • Add a minimization constraint.

    Seealso

    maximize()

    Seealso

    maximizeAny()

    Declaration

    Swift

    public func minimize<T>(_ a: Z3Ast<T>) -> UInt32 where T : ArithmeticSort

  • Add a minimization constraint.

    AST must be of bit vector, int, or real type.

    Seealso

    maximize()

    Seealso

    maximizeAny()

    Declaration

    Swift

    public func minimizeAny(_ a: AnyZ3Ast) -> UInt32

  • Check consistency and produce optimal values.

    Seealso

    getReasonUnknown

    Seealso

    getModel

    Seealso

    getStatistics

    Seealso

    getUnsatCore

    Declaration

    Swift

    public func check(_ assumptions: [AnyZ3Ast] = []) -> Status

    Parameters

    assumptions

    the additional assumptions

  • Retrieve a string that describes the last status returned by check(_:).

    Use this method when check(_:) returns Status.unknown.

    Declaration

    Swift

    public func getReasonUnknown() -> String

  • Retrieve the model for the last check

    The error handler is invoked if a model is not available because the commands above were not invoked for the given optimization solver, or if the result was Status.unsatisfiable.

    Declaration

    Swift

    public func getModel() -> Z3Model

  • Retrieve the unsat core for the last check The unsat core is a subset of the assumptions a.

    Declaration

    Swift

    public func getUnsatCore() -> Z3AstVector

  • Set parameters on optimization context.

    Seealso

    getHelp

    Seealso

    getParamDescrs

    Declaration

    Swift

    public func setParams(_ params: Z3Params)

  • Return the parameter description set for this optimize object.

    Declaration

    Swift

    public func getParamDescrs() -> Z3ParamDescrs

  • Retrieve lower bound value or approximation for the i'th optimization objective.

    Seealso

    getUpper

    Seealso

    getUpperAsVector

    Seealso

    getLowerAsVector

    Declaration

    Swift

    public func getLower(_ idx: UInt32) -> AnyZ3Ast

    Parameters

    idx

    index of optimization objective

  • Retrieve upper bound value or approximation for the i'th optimization objective.

    Seealso

    getLower

    Seealso

    getUpperAsVector

    Seealso

    getLowerAsVector

    Declaration

    Swift

    public func getUpper(_ idx: UInt32) -> AnyZ3Ast

    Parameters

    idx

    index of optimization objective

  • Retrieve lower bound value or approximation for the i'th optimization objective. The returned vector is of length 3. It always contains numerals. The three numerals are coefficients a, b, c and encode the result of getLower() a * infinity + b + c * epsilon.

    Seealso

    getLower

    Seealso

    getUpper

    Seealso

    getUpperAsVector

    Declaration

    Swift

    public func getLowerAsVector(_ idx: UInt32) -> Z3AstVector

    Parameters

    idx

    index of optimization objective

  • Retrieve upper bound value or approximation for the i'th optimization objective.

    Seealso

    getLower

    Seealso

    getUpper

    Seealso

    getLowerAsVector

    Declaration

    Swift

    public func getUpperAsVector(_ idx: UInt32) -> Z3AstVector

    Parameters

    idx

    index of optimization objective

  • Print the current context as a string.

    Seealso

    fromFile

    Seealso

    fromString

    Declaration

    Swift

    public func toString() -> String

  • Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

    Seealso

    fromFile

    Seealso

    toString

    Declaration

    Swift

    public func fromString(_ str: String) throws

  • Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

    Seealso

    fromString

    Seealso

    toString

    Declaration

    Swift

    public func fromFile(_ str: String) throws

  • Return a string containing a description of parameters accepted by optimize.

    Seealso

    getParamDescrs

    Seealso

    setParams

    Declaration

    Swift

    public func getHelp() -> String

  • Retrieve statistics information from the last call to check(_:)

    Declaration

    Swift

    public func getStatistics() -> Z3Stats

  • Return the set of asserted formulas on the optimization context.

    Declaration

    Swift

    public func getAssertions() -> Z3AstVector

  • Return objectives on the optimization context.

    If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...) If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.

    Declaration

    Swift

    public func getObjectives() -> Z3AstVector

  • Create a backtracking point.

    The optimize solver contains a set of rules, added facts and assertions. The set of rules, facts and assertions are restored upon calling pop().

    Seealso

    pop()

    Declaration

    Swift

    public func push()

  • Backtrack one level.

    Precondition

    The number of calls to pop cannot exceed calls to push.

    Seealso

    push()

    Declaration

    Swift

    public func pop()