From 75f2f53731d4300f3748b3d21b60b6d7e8aca614 Mon Sep 17 00:00:00 2001 From: Guido Tack Date: Fri, 22 Nov 2024 10:34:52 +1100 Subject: [PATCH] Remove is_defined_var annotation if no constraint is left defining a variable. Fixes #863. --- changes.rst | 2 +- lib/flatten.cpp | 34 ++++++++++++++----- .../unit/compilation/float_inf_range_dom.fzn | 14 ++++---- tests/spec/unit/compilation/test_bug_863b.fzn | 4 +++ tests/spec/unit/compilation/test_bug_863b.mzn | 11 ++++++ tests/spec/unit/regression/bug_629.fzn | 2 +- 6 files changed, 50 insertions(+), 17 deletions(-) create mode 100644 tests/spec/unit/compilation/test_bug_863b.fzn create mode 100644 tests/spec/unit/compilation/test_bug_863b.mzn diff --git a/changes.rst b/changes.rst index 284b81852..4e455bb05 100644 --- a/changes.rst +++ b/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. diff --git a/lib/flatten.cpp b/lib/flatten.cpp index fa5689db4..deb913d25 100644 --- a/lib/flatten.cpp +++ b/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 globals; @@ -5441,7 +5439,11 @@ void oldflatzinc(Env& e) { // Record indices of VarDeclIs with Id RHS for sorting & unification std::vector 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,6 +5465,13 @@ 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()) { Expression* new_ce = cleanup_constraint(e.envi(), globals, ci->e(), keepDefinesVar); if (new_ce != nullptr) { @@ -5470,9 +5479,15 @@ void oldflatzinc(Env& e) { if (keepDefinesVar) { if (Call* defines_var = Expression::ann(new_ce).getCall(env.constants.ann.defines_var)) { if (Id* ident = Expression::dynamicCast(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( - (*m)[definition_map[cur].first]->cast()->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( + (*m)[definition_map[cur].first]->cast()->e())) { // Variable is defined by a call, push all arguments unsigned int count_cur = 0; for (unsigned int i = 0; i < c->argCount(); i++) { diff --git a/tests/spec/unit/compilation/float_inf_range_dom.fzn b/tests/spec/unit/compilation/float_inf_range_dom.fzn index e0a0ec84b..dcbda5b39 100644 --- a/tests/spec/unit/compilation/float_inf_range_dom.fzn +++ b/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; diff --git a/tests/spec/unit/compilation/test_bug_863b.fzn b/tests/spec/unit/compilation/test_bug_863b.fzn new file mode 100644 index 000000000..5cb809770 --- /dev/null +++ b/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; diff --git a/tests/spec/unit/compilation/test_bug_863b.mzn b/tests/spec/unit/compilation/test_bug_863b.mzn new file mode 100644 index 000000000..3caef02db --- /dev/null +++ b/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; diff --git a/tests/spec/unit/regression/bug_629.fzn b/tests/spec/unit/regression/bug_629.fzn index e96a286c6..80ce529d5 100644 --- a/tests/spec/unit/regression/bug_629.fzn +++ b/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);