Module Z3_mappings.Optimizer

make () creates a new optimizer.

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

pop optimizer pops a context level from the optimizer optimizer.

add optimizer exprs adds the expressions exprs to the optimizer optimizer.

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.

interrupt optimizer interrupts the current optimizer operation.

get_statistics optimizer retrieves statistics from the optimizer optimizer.