sig
  type optimize
  type handle
  val mk_opt : Z3.context -> Z3.Optimize.optimize
  val get_help : Z3.Optimize.optimize -> string
  val set_parameters : Z3.Optimize.optimize -> Z3.Params.params -> unit
  val get_param_descrs :
    Z3.Optimize.optimize -> Z3.Params.ParamDescrs.param_descrs
  val add : Z3.Optimize.optimize -> Z3.Expr.expr list -> unit
  val add_soft :
    Z3.Optimize.optimize ->
    Z3.Expr.expr -> string -> Z3.Symbol.symbol -> Z3.Optimize.handle
  val maximize : Z3.Optimize.optimize -> Z3.Expr.expr -> Z3.Optimize.handle
  val minimize : Z3.Optimize.optimize -> Z3.Expr.expr -> Z3.Optimize.handle
  val check : Z3.Optimize.optimize -> Z3.Solver.status
  val get_model : Z3.Optimize.optimize -> Z3.Model.model option
  val get_lower : Z3.Optimize.handle -> Z3.Expr.expr
  val get_upper : Z3.Optimize.handle -> Z3.Expr.expr
  val push : Z3.Optimize.optimize -> unit
  val pop : Z3.Optimize.optimize -> unit
  val get_reason_unknown : Z3.Optimize.optimize -> string
  val to_string : Z3.Optimize.optimize -> string
  val get_statistics : Z3.Optimize.optimize -> Z3.Statistics.statistics
  val from_file : Z3.Optimize.optimize -> string -> unit
  val from_string : Z3.Optimize.optimize -> string -> unit
  val get_assertions : Z3.Optimize.optimize -> Z3.Expr.expr list
  val get_objectives : Z3.Optimize.optimize -> Z3.Expr.expr list
end