Do not use memory addresses for determining in which order duplicate …

…variables are removed

changelog.in

@@ -68,6 +68,19 @@ Date: 2019-??-??
 [DESCRIPTION]
 Let's see.
 
+[ENTRY]
+Module: kernel
+What:   bug
+Rank:   major
+[DESCRIPTION]
+For the combination of some constraints (min, max, nvalues, and
+some constraints over Boolean variables) with shared variable
+selection branching (that is, AFC, Action, and CHB) the behavior
+of Gecode was indeterminstic. The indeterminism was based on
+using memory addresses for determining the order of variables in
+some propagators which in turn affected which propagator might
+record failure first and hence influenced the branching decisions.
+
 [ENTRY]
 Module: example
 What:   new

gecode/kernel/data/array.hpp

@@ -45,6 +45,24 @@
 
 namespace Gecode { namespace Kernel {
 
+  /// Occurence information for a view
+  template<class View>
+  class ViewOcc {
+  public:
+    /// The view
+    View x;
+    /// The original index in the array
+    int i;
+    /// Sorting order
+    bool operator <(const ViewOcc& y) const;
+  };
+
+  template<class View>
+  forceinline bool
+  ViewOcc<View>::operator <(const ViewOcc& y) const {
+    return x < y.x;
+  }
+
   /// Check whether \a p has duplicates among its \a n elements (changes \a p)
   GECODE_KERNEL_EXPORT
   bool duplicates(void** p, int n);
@@ -1399,12 +1417,32 @@ namespace Gecode {
   ViewArray<View>::unique(void) {
     if (n < 2)
       return;
-    Support::quicksort<View>(x,n);
-    int j = 0;
-    for (int i=1; i<n; i++)
-      if (x[j] != x[i])
-        x[++j] = x[i];
-    n = j+1;
+    Region r;
+    Kernel::ViewOcc<View>* o = r.alloc<Kernel::ViewOcc<View>>(n);
+    for (int i=0; i<n; i++) {
+      o[i].x = x[i]; o[i].i = i;
+    }
+    Support::quicksort<Kernel::ViewOcc<View>>(o,n);
+    // Assign bucket numbers
+    int* bkt = r.alloc<int>(n);
+    int b = 0;
+    bkt[o[0].i] = b;
+    for (int i=1; i<n; i++) {
+      if (o[i-1].x != o[i].x)
+        b++;
+      bkt[o[i].i] = b;
+    }
+    // Eliminate duplicate elements
+    Support::BitSet<Region> seen(r,static_cast<unsigned int>(b+1));
+    int j=0;
+    for (int i=0; i<n; i++)
+      if (!seen.get(bkt[i])) {
+        x[j++]=x[i]; seen.set(bkt[i]);
+      } else {
+        x[j]=x[i];
+      }
+    assert(j == b+1);
+    n = j;
   }
 
   template<class View>