CLP(FD) and monotonicity

Hi all,

as many of you are already aware, the evaluation step that implicitly
takes place when posting arithmetic constraints with CLP(FD) can lead to
declarative problems with the current expression syntax. For example,
simply exchanging the order of goals can yield different results:

   ?- X #= 3, X = 1+2.
   false.

   ?- X = 1+2, X #= 3.
   X = 1+2.

The reason for this is that when a variable is encountered in a CLP(FD)
expression, it is implicitly constrained to a finite domain variable
although declaratively, it stands for other CLP(FD) expressions as well.
This syntax is convenient for users and used by most CLP(FD) systems.

As of the most recent commits, SWI's library(clpfd) now also supports a
syntax that lets you explicitly denote finite domain variables in
expressions: Use ?(X) to state that X is a finite domain variable or
integer, and not any other arithmetic expression. For example:

   ?- ?(X) #= 3.
   X = 3.

This syntax may seem a bit awkward at first and is easier to use with:

   :- op(5, xf, ?).

Example:

   ?- X? #> 3.
   X in 4..sup.

With this ?/1 syntax for variables, the situation above cannot arise:

   ?- X? #= 3, X = 1+2.
   false.

   ?- X = 1+2, X? #= 3.
   %@ ERROR: Type error: `integer' expected, found `1+2'

Note that type errors can be replaced by silent failure and still
preserve declarative equivalence, but instantiation errors can not.

The usual syntax for CLP(FD) variables is of course still supported.
However, if you want declarative purity, set clpfd_monotonic to true:

   :- set_prolog_flag(clpfd_monotonic, true).

When this flag is enabled, you get instantiation errors when bare
variables appear in CLP(FD) expressions. For example:

   ?- X #= 3.
   ERROR: Arguments are not sufficiently instantiated

This error is justified when the clpfd_monotonic flag is set to true
because too little information is known about X: the constraint holds
for any CLP(FD) expression X that evaluates to 3, and there is no way to
describe that with residual goals when we want to obtain X = 3 at the
same time. So, again use ?/1 to explicitly denote a single FD variable:

   ?- X? #= 3.
   X = 3.

When clpfd_monotonic is set to true, the ?/1 syntax is also used in
residual goals, for example:

   ?- X? + Y? #> 5.
   X? + Y? #= _G8957?,
   _G8957 in 6..sup.

Since the ?/1 syntax is now supported in user programs independently of
the clpfd_monotonic flag, I will likely enable this syntax for residual
goals in both cases (i.e., whether or not clpfd_monotonic is true) in
the future to obtain declarative purity in residual programs. Please let
me know if you currently rely on a particular representation of
variables in CLP(FD)'s residual goals, I will take it into account.

Finally, to see why it is called "clpfd_monotonic", consider that adding
additional constraints can currently yield new solutions, rendering
CLP(FD) programs potentially non-monotonic:

   ?- X #= 3, X = 1+2.
   false.

   ?- X = 1+2, X #= 3, X = 1+2.
   X = 1+2.

Of course, this also cannot arise when clpfd_monotonic is set to true:

   ?- X #= 3, X = 1+2.
   %@ ERROR: Arguments are not sufficiently instantiated

Enjoy!

All the best,
Markus