val make : unit -> optimizemake () creates a new optimizer.
val push : optimize -> unitpush optimizer pushes a new context level onto the optimizer optimizer.
val pop : optimize -> unitpop optimizer pops a context level from the optimizer optimizer.
add optimizer exprs adds the expressions exprs to the optimizer optimizer.
val check : optimize -> [ `Sat | `Unsat | `Unknown ]check optimizer checks the satisfiability of the optimizer optimizer. Returns `Sat, `Unsat, or `Unknown.
model optimizer retrieves the model from the optimizer optimizer, if one exists.
maximize optimizer expr maximizes the expression expr in the optimizer optimizer.
minimize optimizer expr minimizes the expression expr in the optimizer optimizer.
val interrupt : optimize -> unitinterrupt optimizer interrupts the current optimizer operation.
val get_statistics : optimize -> Statistics.tget_statistics optimizer retrieves statistics from the optimizer optimizer.