Re: domain propagation

Piero S wrote:
> Dear all,
> 
> I need to enforce a constraint so that the domain of some of its variables
> are not reduced during (domain) propagation. So far I've been using the
> get_bounds/3 predicate to achieve this, as you can see in the following
> example.
> 
> %+++ Example
>    [eclipse 1] lib(ic).
>    [eclipse 2] X #:: 0..1, get_bounds(X,B,T),
>               (Y #:: 0..3, X + Y #< 4, indomain(Y),
>                get_bounds(X,B1,T1), B1#=B, T1#=T).
> 
>    Y = 0
>    X = X{[0, 1]}
>    B1 = 0
>    B = 0
>    T1 = 1
>    T = 1
>    Yes (0.00s cpu, solution 1, maybe more) ? ;
> 
>    [eclipse 3]: X #:: 0..3, get_bounds(X,B,T), (Y #:: 0..1, X #= Y,
>    get_bounds(X,B1,T1), B1 #= B, T1 #= T).
> 
>    No (0.00s cpu)
> %+++


You can get this behaviour by triggering failure as soon as the variable
gets constrained, e.g.

?- X #:: 0 .. 1,
    suspend(fail, 2, X->constrained),
    Y #:: 0 .. 3, X + Y #< 4, indomain(Y).


But a more general warning here: your approach might not achieve
what you want. I guess what you want is a forall-quantification like

forall X in 0..1:  Y #:: 0 .. 3, X + Y #< 4

But the fact that propagation does not eliminate a value from X's domain
does _not_ (in general) prove that this domain value is a valid solution!
Example:

?- [X, Y, Z] :: 0 .. 9, Z #=< Y, Y #\= 1, X #= Y + 1, indomain(Z).
X = X{1 .. 9}
Y = Y{[0, 2 .. 8]}
Z = 0
There is 1 delayed goal.

Even though 2 is still in the domain of X, it is not a solution!
The delayed goal is an indication of this (within a program, you can
use subcall/2 to check for delayed goals).
In general, you need to label all variables to be sure that there
are no delayed goals left, and the values really are solutions.


-- 
  Joachim Schimpf              /             phone: +44 20 7594 8187
  IC-Parc                     /      mailto:J.Schimpf@imperial.ac.uk
  Imperial College London    /    http://www.icparc.ic.ac.uk/eclipse