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.
UnsatCore returns the unsat core if the constraints are unsatisfiable.