Module Optimizer.MakeSource

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

Parameters

module _ : Mappings_intf.S

Signature

Sourcetype t

The type of optimization solvers.

Sourceval create : unit -> t

create () creates a new optimization solver.

Sourceval push : t -> unit

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

Sourceval pop : t -> unit

pop solver pops a context level from the solver solver.

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

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

Sourceval 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.

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

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

Sourceval model : t -> Model.t option

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

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

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

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

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

Sourceval get_statistics : t -> Statistics.t

get_statistics solver retrieves statistics from the solver solver.