Library Predicates

Constraints

Vars :: Lo..Hi

Logically: Constrain a variable (or all variables in a list) to take only integer or real values in a given range. The type of the bounds determines the type of the variable (real or integer). Also allowed are the (untyped) symbolic bound values inf, +inf and -inf. For instance

X :: 0..1 % boolean
X :: -1..5 % integer between -1 and 5
X :: 1..inf % strictly positive integer
X :: 0.0..10.0 % real between 0.0 and 10.0
X :: 1.5..3.7 % real between 1.5 and 3.7
X :: 0.0..inf % positive real
X :: 0.0..5 % TYPE ERROR

Operationally, the range and type information is immediately stored into the variable's attribute.

reals(Vars)

The domain of the variables is the real numbers. This is the default, so the declaration is optional. real(X) is equivalent to X :: -inf..inf. Mathematical Programming style nonnegative variables are best declared as X :: 0.0..inf.

Note that the notion of real numbers is used here in the pure mathematical sense, where real numbers subsume the integers. A variable of type real can therefore be instantated to either a floating point or an integer number.

integers(Vars)

Constrain the variables to integer values. Note that this declaration is implicit when specifiying an integer range, e.g. in Y :: 0..99.

lwb(?Var, +Bound)

Constrain the variable to be greater or equal to the specified lower bound. A bound update on a variable may fail (when the update empties the domain), succeed (possibly updating the variable's bounds), or instantiate the variable (in case the domain get restricted to a singleton value). Note that if the variable's type is integer, its bounds will always be adjusted to integral values.

Important hint: If the bound is indeed modified, this predicate will invoke schedule_suspensions/2 for the corresponding suspension list. This will only schedule the delayed suspensions for execution, but not actually execute them. The caller therefore has to invoke wake/0 (the woken goal scheduler) at an appropriate point in the subsequent execution.

upb(?Var, +Bound)

As above, but constrains the variable to be less or equal to the specified upper bound.

Examples

Every new constraint on a variable is immediately reflected in the range:

[eclipse 2]: X::0.0..9.5, lwb(X,4.5).
X = X{4.5 .. 9.5}
yes.
[eclipse 3]: X::0.0..9.5, lwb(X,4.5), integers([X]).
X = X{5 .. 9}
yes.
[eclipse 4]: X::0.0..9.5, lwb(X,4.5), integers([X]), upb(X,5.9).
X = 5
yes.
[eclipse 5]: X::0.0..9.5, lwb(X,4.5), upb(X,4.3).
no (more) solution.

Retrieving Domain Information

var_range(?Var, -Lo, -Hi)

Retrieve the current range of a variable (or number). Lo and Hi return the minimum and maximum (respectively) of the variable's range in floating point format (regardless of the variable's type). If Var has not been declared before, it will be turned into an unrestricted real variable. If Var is a number, that number will be returned as both Lo and Hi.

var_type(?Var, -Type)

Retrieve the type ('real' or 'integer') of a variable (or number).

Auxliliary Predicates

range_msg(?Var1, ?Var2, ?Var3)

The most specific generalisation of two ranges is computed and returned as Var3. Var3 will range over the smallest interval enclosing the input ranges, and have the more general type of the input types.

print_range(?Var, -Range)

Returns the variable's range in a form that would be acceptable to ::/2, ie. as a Lo..Hi structure, encoding the variable's type in the type of the bounds.

set_range_bounds(?Var, +Lo, +Hi)

Imposes lower and upper bounds on the variable (a combination of lwb/2, upb/2 and wake/0). This is the set_bounds-handler (see below).

Handlers

The library installs the following handlers (cf. ECLiPSeUser Manual) in order to implement the semantics of ranged variables:

unify

Unification between two variables amounts to intersecting their ranges and taking the more restrictive type as the result type. If the intersection is empty, the unification fails. Unifying a variable with a number involves a check whether the number is within the variable's range and of the proper type, otherwise failure occurs.

test_unify

like unify.

compare_instances

A range variable is an instance of another when its range is subsumed by the other range.

copy_term

Range and type are copied, delayed goals are not.

suspensions, delayed_goals_number

Considers the goals in the two attached suspension lists.

get_bounds

get the variable's bounds, the handler is var_range/3.

set_bounds

set the variable's bounds, the handler is set_range_bounds/3.

print

Ranges are printed using print_range/2.

Due to the handlers, Unification and instance test take the ranges into account:

[eclipse 6]: X::0.0..5.5, Y::3..8, X=Y.
X = X{3 .. 5}
Y = X{3 .. 5}
yes.
[eclipse 8]: X::0.0..5.5, Y::3..8, instance(X,Y).
no (more) solution.
[eclipse 9]: X::0.0..5.5, Y::3..5, instance(Y,X).
Y = Y{3 .. 5}
X = X{0.0 .. 5.5}
yes.