Module Optimizer.Make

Make is a functor that creates an optimizer instance from a given mappings module.

Parameters

module _ : Mappings_intf.S

Signature

type t

The type of optimization solvers.

val create : unit -> t

create () creates a new optimization solver.

val push : t -> unit

push solver pushes a new context level onto the solver solver.

val pop : t -> unit

pop solver pops a context level from the solver solver.

val add : t -> Expr.t list -> unit

add solver exprs adds the expressions exprs to the solver solver.

val protect : t -> (unit -> 'a) -> 'a

protect solver f executes the function f within a protected context, ensuring that the solver state is restored after execution.

val check : t -> [ `Sat | `Unsat | `Unknown ]

check solver checks the satisfiability of the solver solver. Returns `Sat, `Unsat, or `Unknown.

val model : t -> Model.t option

model solver retrieves the model from the solver solver, if one exists.

val maximize : t -> Expr.t -> Value.t option

maximize solver expr maximizes the expression expr in the solver solver. Returns the optimal value if found.

val minimize : t -> Expr.t -> Value.t option

minimize solver expr minimizes the expression expr in the solver solver. Returns the optimal value if found.

val get_statistics : t -> Statistics.t

get_statistics solver retrieves statistics from the solver solver.