Make is a functor that creates an optimizer instance from a given mappings module.
module _ : Mappings_intf.Sval create : unit -> tcreate () creates a new optimization solver.
val push : t -> unitpush solver pushes a new context level onto the solver solver.
val pop : t -> unitpop solver pops a context level from the solver solver.
val protect : t -> (unit -> 'a) -> 'aprotect 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.
model solver retrieves the model from the solver solver, if one exists.
maximize solver expr maximizes the expression expr in the solver solver. Returns the optimal value if found.
minimize solver expr minimizes the expression expr in the solver solver. Returns the optimal value if found.
val get_statistics : t -> Statistics.tget_statistics solver retrieves statistics from the solver solver.