package smtml

  1. Overview
  2. Docs
package smtml
Legend:
Page
Library
Module
Module type
Parameter
Class
Class type
Source

Module Mappings.OptimizerSource

Sourceval make : unit -> optimizer

make () creates a new optimizer.

Sourceval push : optimizer -> unit

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

Sourceval pop : optimizer -> unit

pop optimizer pops a context level from the optimizer optimizer.

Sourceval add : optimizer -> term list -> unit

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

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

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

Sourceval model : optimizer -> model option

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

Sourceval maximize : optimizer -> term -> handle

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

Sourceval minimize : optimizer -> term -> handle

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

Sourceval interrupt : unit -> unit

interrupt () interrupts the current optimizer operation.

Sourceval get_statistics : optimizer -> Statistics.t

get_statistics optimizer retrieves statistics from the optimizer optimizer.

Sourceval pp_statistics : optimizer Fmt.t

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