Module Z3.Optimize

module Optimize: sig .. end
Optimization

type optimize 
type handle 
val mk_opt : context -> optimize
Create a Optimize context.
val get_help : optimize -> string
A string that describes all available optimize solver parameters.
val set_parameters : optimize -> Params.params -> unit
Sets the optimize solver parameters.
val get_param_descrs : optimize -> Params.ParamDescrs.param_descrs
Retrieves parameter descriptions for Optimize solver.
val add : optimize -> Expr.expr list -> unit
Assert a constraints into the optimize solver.
val add_soft : optimize ->
Expr.expr -> string -> Symbol.symbol -> handle
Asssert a soft constraint. Supply integer weight and string that identifies a group of soft constraints.
val maximize : optimize -> Expr.expr -> handle
Add maximization objective.
val minimize : optimize -> Expr.expr -> handle
Add minimization objective.
val check : optimize -> Solver.status
Checks whether the assertions in the context are satisfiable and solves objectives.
val get_model : optimize -> Model.model option
Retrieve model from satisfiable context
val get_lower : handle -> int -> Expr.expr
Retrieve lower bound in current model for handle
val get_upper : handle -> int -> Expr.expr
Retrieve upper bound in current model for handle
val push : optimize -> unit
Creates a backtracking point. Optimize.pop
val pop : optimize -> unit
Backtrack one backtracking point. Note that an exception is thrown if Pop is called without a corresponding Push Optimize.push
val get_reason_unknown : optimize -> string
Retrieve explanation why optimize engine returned status Unknown.
val to_string : optimize -> string
Retrieve SMT-LIB string representation of optimize object.
val get_statistics : optimize -> Statistics.statistics
Retrieve statistics information from the last call to check