Complete GCC solution-loss fix

Author: Mikael Zayenz Lagerkvist

changelog.in

@@ -82,8 +82,9 @@ Rank:   major
 Issue:  166
 Thanks: Mats Carlsson
 [DESCRIPTION]
-Fix domain-level global cardinality propagation losing solutions when search
-recomputation applies several branch choices before propagation.
+Fix domain-level global cardinality propagation losing solutions by counting
+assigned variables twice and retaining stale conflict marks when cardinality
+bounds shrink.
 
 [ENTRY]
 Module: flatzinc

gecode/int/gcc/dom-sup.hpp

@@ -1268,7 +1268,8 @@ namespace Gecode { namespace Int { namespace GCC {
               v->maxlow(k[i].max() - (inc_lbc));
               if (v->kmin() == v->kmax())
                 v->cap(LBC,k[i].max() - (inc_lbc));
-              v->card_conflict(rm);
+              int matched = inc_ubc - v->kcount();
+              v->card_conflict(std::min(rm, matched));
             }
           }
         }

test/flatzinc/issue166.cpp

@@ -35,25 +35,42 @@
 namespace Test { namespace FlatZinc {
 
   namespace {
-    /// Check that recomputation does not lose a solution
-    bool check(const std::string& output) {
+    /// Check that recomputation does not lose solutions
+    bool check(const std::string& output, int expected,
+               const std::string& representative) {
       const std::string separator = "----------\n";
       int solutions = 0;
       for (std::string::size_type p = 0;
            (p = output.find(separator,p)) != std::string::npos;
            p += separator.size())
         solutions++;
-      return (solutions == 11) &&
-        (output.find("A = 3;\nB = 1;\nC = 3;\nD = 1;\nE = 2;\nG = 3;\n")
-         != std::string::npos);
+      return (solutions == expected) &&
+        (output.find(representative) != std::string::npos);
     }
 
     /// Helper class to create and register test
     class Create {
     public:
       /// Perform creation and registration
       Create(void) {
-        (void) new FlatZincTest("Issue166",
+        (void) new FlatZincTest("Issue166::Original",
+"predicate gecode_global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);\n\
+var {1,3}: A :: output_var;\n\
+var 2..3: B :: output_var;\n\
+var 2..3: C :: output_var;\n\
+var 2..3: D :: output_var;\n\
+var 2..5: E :: output_var;\n\
+var 1..4: F :: output_var;\n\
+var 2..3: G :: output_var;\n\
+var 2..3: H :: output_var;\n\
+constraint gecode_global_cardinality([A,D,1,3,3,C,1,H,B],[1,2,3],[G,F,E]) :: domain;\n\
+solve :: int_search([A,B,C,D,E,F,G,H],anti_first_fail,indomain_min,complete) satisfy;\n",
+          "", true, {"-a"}, [] (const std::string& output) {
+            return check(output, 26,
+                         "A = 1;\nB = 2;\nC = 3;\nD = 3;\nE = 5;\n"
+                         "F = 1;\nG = 3;\nH = 3;\n");
+          });
+        (void) new FlatZincTest("Issue166::Minimized",
 "predicate gecode_global_cardinality(array [int] of var int: x, array [int] of int: cover, array [int] of var int: counts);\n\
 var 1..3: A :: output_var;\n\
 var 1..3: B :: output_var;\n\
@@ -63,7 +80,11 @@ var 2..3: E :: output_var;\n\
 var 2..3: G :: output_var;\n\
 constraint gecode_global_cardinality([3,A,D,G,E],[1,2,3],[1,B,C]) :: domain;\n\
 solve :: int_search([D,A,E,B],input_order,indomain_random,complete) satisfy;\n",
-          "", true, {"-a", "-r", "0", "-c-d", "8"}, check);
+          "", true, {"-a", "-r", "0", "-c-d", "8"},
+          [] (const std::string& output) {
+            return check(output, 11,
+                         "A = 3;\nB = 1;\nC = 3;\nD = 1;\nE = 2;\nG = 3;\n");
+          });
       }
     };