Module Sat.LinearExpr

Linear expressions are used in linear constraints and to specify objectives.

type t

A linear expression. An integer offset is maintainted in addition to a list of coefficients and variables. This allows both to normalize boolean literals into positive form and to represent constants (see of_int).

val zero : t

An empty linear expression.

val sum : t list -> t

A sum of linear expressions.

val sum_vars : 'a Var.t list -> t

A sum of variables: all coefficients are 1s.

val weighted_sum : (int * 'a Var.t) list -> t

A weighted sum of variables.

val scale : int -> t -> t

Multiply all coefficients by an integer.

val of_int : int -> t

A constant expression.

val var : 'a Var.t -> t

A single variable.

val term : (int * 'a Var.t) -> t

A single term. See also (*).

val neg : t -> t

Negate all coefficients (and the offset).

val to_string : t -> string

Return a string representing the linear expression.

val pp : Stdlib.Format.formatter -> t -> unit

Pretty-printer for linear expressions.

module L : sig ... end

Operators for building linear expressions. They are also available directly in the Sat module.