[Fwd: Re: not exactly a bug with FD constraints]

From: Joachim Schimpf <j.schimpf_at_icparc.ic.ac.uk> Date: Wed 16 Jun 2004 03:33:19 PM GMT Message-ID: <40D0683F.403@icparc.ic.ac.uk> · This archive was generated by hypermail 2.1.8 : Wed 16 Nov 2005 06:08:24 PM GMT GMT

Alexander Pretschner wrote:
> Hi there,
> 
> it's not exactly a bug, and the behavior is understandable yet--for my 
> purposes--undesirable: "X#=Y and X#\=Y" is satisfiable.
> 
> Eclipse 57#43 under Linux reacts as follows:
> 
> 
> [eclipse 1]: lib(fd).
> [eclipse 2]: X#>10, Y#>20, X#\=Y, X#=Y.
> 
> X = X{[21..10000000]}
> Y = X{[21..10000000]}
> 
> 
> Delayed goals:
>         X{[21..10000000]} #\= X
> Yes (0.00s cpu)

You can add a ~= constraint, which will detect this situation:

[eclipse 2]: X#>10, Y#>20, X#\=Y, X~=Y, X#=Y.

No (0.00s cpu)

-- 
  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