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