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. For a new variable x, lb <= x <= ub.

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 any : [< `Bool | `Int ] t -> [ `Bool | `Int ] t

Ignore any type information. Allows, for example, to stored differently typed variables in a data structure. The explicit to_bool/to_int casts, with dynamic checks, can be applied to recover the types.

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.