Optimization with maximize/minimize objectives
Context methods (receiver omitted for clarity)
NewOptimize creates a new optimization context.
Optimize represents a Z3 optimization context for solving optimization problems. Unlike Solver which only checks satisfiability, Optimize can find optimal solutions with respect to objective functions.
Assert adds a constraint to the optimizer.
AssertAndTrack adds a constraint with a tracking literal for unsat core extraction.
AssertSoft adds a soft constraint with a weight. Soft constraints are used for MaxSMT problems. Returns a handle to the objective.
Assertions returns the assertions in the optimizer.
Check checks the satisfiability of the constraints and optimizes objectives.
FromFile parses an SMT-LIB2 file with optimization objectives and constraints.
FromString parses an SMT-LIB2 string with optimization objectives and constraints.
GetHelp returns help information for the optimizer.
GetLower retrieves a lower bound for the objective at the given index.
GetLowerAsVector retrieves a lower bound as a vector (inf, value, eps). The objective value is unbounded if inf is non-zero, otherwise it's represented as value + eps * EPSILON.
GetUpper retrieves an upper bound for the objective at the given index.
GetUpperAsVector retrieves an upper bound as a vector (inf, value, eps). The objective value is unbounded if inf is non-zero, otherwise it's represented as value + eps * EPSILON.
Maximize adds a maximization objective. Returns a handle to the objective that can be used to retrieve bounds.
Minimize adds a minimization objective. Returns a handle to the objective that can be used to retrieve bounds.
Model returns the model if the constraints are satisfiable.
Objectives returns the objectives in the optimizer.
Pop removes a backtracking point.
Push creates a backtracking point.
ReasonUnknown returns the reason why the result is unknown.
SetParams sets parameters for the optimizer.
String returns the string representation of the optimize context.
Translate creates a copy of the optimize context in the target context. This is useful when working with multiple Z3 contexts.
UnsatCore returns the unsat core if the constraints are unsatisfiable.