Module LinearExpr.L

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

val zero : t

An empty linear expression.

val var : 'a Var.t -> t

A single variable.

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

A single term.

val (+) : t -> t -> t

Concatenatation of two linear expressions.

val (-) : t -> t -> t

Concatenatation of the left expression with the negation of the right expression.

val scale : int -> t -> t

Multiplication of a linear expression by a constant.

val of_int : int -> t

A constant linear expression.

val not : Var.t_bool -> Var.t_bool

Complement a boolean literal. Same as Var.not.