Remove is_defined_var annotation if no constraint is left defining a …

…variable. Fixes #863.

changes.rst

@@ -29,7 +29,7 @@ Bug fixes:
 -  Fix compilation of empty arrays with empty domains (:bugref:`860`).
 -  Fix evaluation of ``dom_array`` on par arrays (:bugref:`851`).
 -  Fix flattening of array slices inside tuples and records (:bugref:`859`).
--  Fix defines_var annotation for cyclic definitions (:bugref:`863`).
+-  Fix defines_var annotation for cyclic and missing definitions (:bugref:`863`).
 -  Fix assertion failures when using arrays as argument to bin packing constraints
    (:bugref:`865`).
 -  Fix operator precedences for ``intersect`` and unary plus/minus.

lib/flatten.cpp

@@ -5429,8 +5429,6 @@ void oldflatzinc(Env& e) {
 
   EnvI& env = e.envi();
 
-  unsigned int msize = m->size();
-
   // Predicate declarations of solver builtins
   std::unordered_set<Item*> globals;
 
@@ -5441,7 +5439,11 @@ void oldflatzinc(Env& e) {
 
   // Record indices of VarDeclIs with Id RHS for sorting & unification
   std::vector<int> declsWithIds;
-  for (int i = 0; i < msize; i++) {
+
+  // Important: items are being added to m while iterating over it.
+  // The loop therefore needs to check the size in each iteration to make
+  // sure it also handles the new items.
+  for (int i = 0; i < m->size(); i++) {
     if ((*m)[i]->removed()) {
       continue;
     }
@@ -5463,16 +5465,29 @@ void oldflatzinc(Env& e) {
           e.envi().flatAddItem(new ConstraintI(Location().introduce(), new_ce));
         }
       }
+      if (Expression::ann(vd).contains(e.envi().constants.ann.is_defined_var)) {
+        if (definition_map.find(vd) == definition_map.end()) {
+          // We haven't seen this variable before
+          definition_map.insert({vd, {-1, DFS_UNKNOWN}});
+          definitions.push_back(vd);
+        }
+      }
     } else if (auto* ci = (*m)[i]->dynamicCast<ConstraintI>()) {
       Expression* new_ce = cleanup_constraint(e.envi(), globals, ci->e(), keepDefinesVar);
       if (new_ce != nullptr) {
         ci->e(new_ce);
         if (keepDefinesVar) {
           if (Call* defines_var = Expression::ann(new_ce).getCall(env.constants.ann.defines_var)) {
             if (Id* ident = Expression::dynamicCast<Id>(defines_var->arg(0))) {
-              if (definition_map.find(ident->decl()) != definition_map.end()) {
-                // This is the second definition, remove it
-                Expression::ann(new_ce).removeCall(env.constants.ann.defines_var);
+              auto it = definition_map.find(ident->decl());
+              if (it != definition_map.end()) {
+                if (it->second.first == -1) {
+                  // We've only seen the decl before, but not yet the defining constraint
+                  it->second.first = i;
+                } else {
+                  // This is the second definition, remove it
+                  Expression::ann(new_ce).removeCall(env.constants.ann.defines_var);
+                }
               } else {
                 definition_map.insert({ident->decl(), {i, DFS_UNKNOWN}});
                 definitions.push_back(ident->decl());
@@ -5552,8 +5567,11 @@ void oldflatzinc(Env& e) {
           } else {
             // now visited and on stack
             definition_map[cur].second = DFS_SEEN;
-            if (Call* c = Expression::dynamicCast<Call>(
-                    (*m)[definition_map[cur].first]->cast<ConstraintI>()->e())) {
+            if (definition_map[cur].first == -1) {
+              // No associated call, remove annotation
+              Expression::ann(cur).remove(Constants::constants().ann.is_defined_var);
+            } else if (Call* c = Expression::dynamicCast<Call>(
+                           (*m)[definition_map[cur].first]->cast<ConstraintI>()->e())) {
               // Variable is defined by a call, push all arguments
               unsigned int count_cur = 0;
               for (unsigned int i = 0; i < c->argCount(); i++) {

tests/spec/unit/compilation/float_inf_range_dom.fzn

@@ -1,12 +1,12 @@
 var float: x:: output_var;
-var bool: X_INTRODUCED_1_ ::var_is_introduced :: is_defined_var;
 var bool: X_INTRODUCED_2_ ::var_is_introduced :: is_defined_var;
 var bool: X_INTRODUCED_3_ ::var_is_introduced :: is_defined_var;
-var bool: X_INTRODUCED_5_ ::var_is_introduced :: is_defined_var;
+var bool: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var;
+var bool: X_INTRODUCED_6_ ::var_is_introduced :: is_defined_var;
 constraint float_le(1.0,x);
-constraint bool_clause([X_INTRODUCED_3_,X_INTRODUCED_5_],[]);
-constraint float_le_reif(1.0,x,X_INTRODUCED_1_):: defines_var(X_INTRODUCED_1_);
-constraint float_le_reif(x,2.0,X_INTRODUCED_2_):: defines_var(X_INTRODUCED_2_);
-constraint array_bool_and([X_INTRODUCED_1_,X_INTRODUCED_2_],X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
-constraint float_le_reif(3.0,x,X_INTRODUCED_5_):: defines_var(X_INTRODUCED_5_);
+constraint bool_clause([X_INTRODUCED_4_,X_INTRODUCED_6_],[]);
+constraint float_le_reif(1.0,x,X_INTRODUCED_2_):: defines_var(X_INTRODUCED_2_);
+constraint float_le_reif(x,2.0,X_INTRODUCED_3_):: defines_var(X_INTRODUCED_3_);
+constraint array_bool_and([X_INTRODUCED_2_,X_INTRODUCED_3_],X_INTRODUCED_4_):: defines_var(X_INTRODUCED_4_);
+constraint float_le_reif(3.0,x,X_INTRODUCED_6_):: defines_var(X_INTRODUCED_6_);
 solve  satisfy;

tests/spec/unit/compilation/test_bug_863b.fzn

@@ -0,0 +1,4 @@
+var 1..2: X_INTRODUCED_0_;
+var 1..2: X_INTRODUCED_1_;
+array [1..2] of var int: arr:: output_array([1..2]) = [X_INTRODUCED_0_,X_INTRODUCED_1_];
+solve  satisfy;

tests/spec/unit/compilation/test_bug_863b.mzn

@@ -0,0 +1,11 @@
+/***
+!Test
+type: compile
+solvers: [chuffed]
+expected: !FlatZinc test_bug_863b.fzn
+***/
+
+array[1..2] of var 1..2: arr;
+var 1..2: index;
+constraint arr[index] = arr[2];
+constraint index == 2;

tests/spec/unit/regression/bug_629.fzn

@@ -1,7 +1,7 @@
 array [1..2] of int: X_INTRODUCED_3_ = [1,1];
 array [1..2] of int: X_INTRODUCED_7_ = [-1,1];
 array [1..2] of int: X_INTRODUCED_9_ = [-1,-1];
-var 0..1: X_INTRODUCED_4_ ::var_is_introduced :: is_defined_var;
+var 0..1: X_INTRODUCED_4_ ::var_is_introduced ;
 var 0..1: X_INTRODUCED_5_ ::var_is_introduced ;
 var 0..1: X_INTRODUCED_6_ ::var_is_introduced :: output_var;
 constraint int_lin_le(X_INTRODUCED_7_,[X_INTRODUCED_4_,X_INTRODUCED_6_],0);