Module Sat.Var

Representation of integer variables and boolean literals.

type 'a t

A variable or boolean literal. Note that each variable and boolean literal is associated with a specific model. It is an error to mix variables or literals from different models.

type t_bool = [ `Bool ] t

A boolean literal.

type t_int = [ `Int ] t

An integer variable.

val new_int : model -> lb:int -> ub:int -> string -> t_int

Add a new bounded integer variable to a model.

val new_int_from_domain : model -> Domain.t -> string -> t_int

Restrict the new bounded integer variable to a domain.

val new_bool : model -> string -> t_bool

Add a new boolean variable to a model.

val not : t_bool -> t_bool

Complement a boolean literal.

val new_constant : model -> int -> t_int

Create a new integer variable constrained to a given value.

val to_index : 'a t -> int

Expose the underlying index of a variable.

val to_bool : 'a t -> [ `Bool ] t

Assert that a variable is a boolean variable. Raises Invalid_argument for a variable x that does not satisfy 0 <= x <= 1.

val to_int : 'a t -> [ `Int ] t

Convert a variable to an integer variable. Raises Invalid_argument on complemented boolean literals.

val to_string : 'a t -> string

Return a string representing the variable or boolean literal.

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

Pretty-printer for variables and boolean literals.