Module M_with_make.Optimizer

val make : unit -> optimizer

make () creates a new optimizer.

val push : optimizer -> unit

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

val pop : optimizer -> unit

pop optimizer pops a context level from the optimizer optimizer.

val add : optimizer -> term list -> unit

add optimizer ts adds the terms ts to the optimizer optimizer.

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

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

val model : optimizer -> model option

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

val maximize : optimizer -> term -> handle

maximize optimizer t maximizes the term t in the optimizer optimizer.

val minimize : optimizer -> term -> handle

minimize optimizer t minimizes the term t in the optimizer optimizer.

val interrupt : unit -> unit

interrupt () interrupts the current optimizer operation.

val get_statistics : optimizer -> Statistics.t

get_statistics optimizer retrieves statistics from the optimizer optimizer.

val pp_statistics : optimizer Fmt.t

pp_statistics fmt optimizer pretty-prints the statistics of the optimizer optimizer using the formatter fmt.