incomplete constraint propagation

The ECLiPSe banner with the version number and configuration
(unless visible in the script):

	ECLiPSe Constraint Logic Programming System [kernel]
	Copyright Imperial College London and ICL
	Certain libraries copyright Parc Technologies Ltd
	GMP library copyright Free Software Foundation
	Version 5.1.1, Thu Feb 22 01:08 2001

Machine type:

	sun4u sparc SUNW,Ultra-5_10

Operating system name and version number:

	SunOS 5.8 Generic_108528-05

If graphics is involved, ProTcl and Tcl/Tk release number,
X version number, X server type and window manager:

	no graphics involved

Your .eclipserc and ECLIPSE... environment variables, if used:

	not used

A script which causes the bug to appear, enhanced by comments where
necessary (start from the ECLiPSe banner unless the option -e is used):

	The problem is that my program is completely constrained, but Eclipse
	fails to follow through all the constraints.  Here is my program, based on
	a logic puzzle from Dell Logic Puzzles, October 1999, page 8, called
	"Boo!".  I first represent the logic puzzle in my own "Constraint Lingo",
	from which I then generate Eclipse clauses, retaining Constraint Lingo as
	comments for documentation purposes.  I have a paper on Constraint Lingo
	if you are interested; I also can generate smodels clauses, and smodels
	succeeds in finding the unique solution.

	--- program starts here

	:- use_module(library(fd)) .

	try :- 

	% CLASS place: 1 .. 4
		Place = [Place1, Place2, Place3, Place4],
		Place :: 1..4,
		alldifferent(Place),
	% CLASS child: bernadette juan keisha sam
		Child = [Bernadette, Juan, Keisha, Sam],
		Child :: 1..4,
		alldifferent(Child),
	% Break symmetry
		Bernadette = 1,
		Juan = 2,
		Keisha = 3,
		Sam = 4,
	% CLASS costume: crayon lion robot scarecrow
		Costume = [Crayon, Lion, Robot, Scarecrow],
		Costume :: 1..4,
		alldifferent(Costume),
	% 	CONFLICT sam robot
		Robot #\= Sam,
	% 	REQUIRED sam 4
		Sam #= Place4,
	% 	OFFSET 1 place: scarecrow lion
		( ( Scarecrow #= Place1 #/\ Lion #= Place2 ) #\/
		(Scarecrow #= Place2 #/\ Lion #= Place3) #\/
		(Scarecrow #= Place3 #/\ Lion #= Place4) ),
	% 	CONFLICT bernadette 2
		Bernadette #\= Place2,
	% 	OFFSET 2 place: crayon keisha
		((Crayon #= Place1 #/\ Keisha #= Place3) #\/
		(Crayon #= Place2 #/\ Keisha #= Place4)),
	% print result
		write(stdout, '\nPlace1 = '), write(stdout, Place1) ,
		write(stdout, '\nPlace2 = '), write(stdout, Place2) ,
		write(stdout, '\nPlace3 = '), write(stdout, Place3) ,
		write(stdout, '\nPlace4 = '), write(stdout, Place4) ,
		write(stdout, '\nBernadette = '), write(stdout, Bernadette) ,
		write(stdout, '\nJuan = '), write(stdout, Juan) ,
		write(stdout, '\nKeisha = '), write(stdout, Keisha) ,
		write(stdout, '\nSam = '), write(stdout, Sam) ,
		write(stdout, '\nCrayon = '), write(stdout, Crayon) ,
		write(stdout, '\nLion = '), write(stdout, Lion) ,
		write(stdout, '\nRobot = '), write(stdout, Robot) ,
		write(stdout, '\nScarecrow = '), write(stdout, Scarecrow) .

	--- program ends here
	
	once try/1 is compiled, I run it by the query "try ." .
	
	Output:
		Place1 = 1
		Place2 = 2
		Place3 = 3
		Place4 = 4
		Bernadette = 1
		Juan = 2
		Keisha = 3
		Sam = 4
		Crayon = 1
		Lion = _622{[2..4]}
		Robot = _635{[2, 3]}
		Scarecrow = _648{[2, 4]}

	This output is correct so far as it goes, but it should go farther.  For
	example, Scarecrow cannot be 4, because the clause for 
	"OFFSET 1 place: scarecrow lion" explicitly restricts it to 1, 2, or 3.
	Even if I explicitly add a term "Scarecrow #\= 4", Eclipse propagates
	constraints no further.  But of the three disjuncts in

		( ( Scarecrow #= Place1 #/\ Lion #= Place2 ) #\/
		(Scarecrow #= Place2 #/\ Lion #= Place3) #\/
		(Scarecrow #= Place3 #/\ Lion #= Place4) ),
	
	the first is disallowed because Place1=1 and Scarecrow={[2,4]}, and
	the second is disallowed because it would prevent Robot from getting a
	valid value.  After all, Robot is distinct from Scarecrow (putatively
	Place2=2), Lion (putatively Place3=3), and Crayon (known to be Place1=1),
	but Robot is known to be in {[2,3]}.  Therefore, only the third disjunct
	holds, so Scarecrow=Place3=3, Lion=Place4=4, forcing Robot=Place2=2, fully
	constraining all the variables.

	If it is any consolation, Gnu Prolog also fails in exactly the same way.

Raphael Finkel