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

Assert 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

Check consistency and produce optimal values.

val get_model : optimize -> Model.model option

Retrieve model from satisfiable context

val get_lower : handle -> Expr.expr

Retrieve lower bound in current model for handle

val get_upper : handle -> 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

val from_file : optimize -> string -> unit

Parse an SMT-LIB2 file with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

val from_string : optimize -> string -> unit

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the optimization context.

val get_assertions : optimize -> Expr.expr list

Return the set of asserted formulas on the optimization context.

val get_objectives : optimize -> Expr.expr list

Return objectives on the optimization context. If the objective function is a max-sat objective it is returned as a Pseudo-Boolean (minimization) sum of the form (+ (if f1 w1 0) (if f2 w2 0) ...). If the objective function is entered as a maximization objective, then return the corresponding minimization objective. In this way the resulting objective function is always returned as a minimization objective.