package alt-ergo-lib

  1. Overview
  2. Docs

Module Objective.Function

type index
type t = private {
  1. e : Expr.t;
    (*

    Term that represents the objective function.

    *)
  2. is_max : bool;
    (*

    Determine if we want to maximize or minimize this objective function.

    *)
  3. index : index;
    (*

    Unique identifier from the input. This field is used as a priority index.

    *)
}

Type of an objective function.

val mk : is_max:bool -> Expr.t -> t
val pp : t Fmt.t

pp ppf o prints the objective function o on the formatter ppf using the SMT-LIB format.

val reinit_cnt : unit -> unit

Reinitializes the internal counter used to produce unique indexes.