-
The context this
Z3Optimize
belongsDeclaration
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 soft constraint to the optimization context.
Seealso
assert
Seealso
assertAndTrack
Declaration
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
-
Retrieve a string that describes the last status returned by
check(_:)
.Use this method when
check(_:)
returnsStatus.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 assumptionsa
.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 ofgetLower()
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
-
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
-
Backtrack one level.
Precondition
The number of calls to pop cannot exceed calls to push.Seealso
push()
Declaration
Swift
public func pop()