Make sure search annotation array arguments are 1d and 1-based

Fixes #768
MiniZinc · Jan 25, 2024 · 183877b · 183877b
1 parent f300070
commit 183877b
Show file tree

Hide file tree

Showing 6 changed files with 60 additions and 0 deletions.
diff --git a/changes.rst b/changes.rst
@@ -21,6 +21,8 @@ Bug fixes:
 -  Fix crash involving ``var`` comprehensions with set types by rejecting
    unsupported type (:bugref:`779`).
 -  Fix internal error during evaluation of ``par opt set`` expressions.
+-  Fix invalid FlatZinc produced when search annotations are passed non-1-based
+   arrays (:bugref:`768`).
 
 Changes:
 ^^^^^^^^

diff --git a/include/minizinc/ast.hh b/include/minizinc/ast.hh
@@ -2301,6 +2301,13 @@ public:
     Id* flatzinc_builtin;                    // NOLINT(readability-identifier-naming)
     Id* mzn_evaluate_once;                   // NOLINT(readability-identifier-naming)
     Id* promise_commutative;                 // NOLINT(readability-identifier-naming)
+    ASTString seq_search;                    // NOLINT(readability-identifier-naming)
+    ASTString int_search;                    // NOLINT(readability-identifier-naming)
+    ASTString bool_search;                   // NOLINT(readability-identifier-naming)
+    ASTString float_search;                  // NOLINT(readability-identifier-naming)
+    ASTString set_search;                    // NOLINT(readability-identifier-naming)
+    ASTString warm_start;                    // NOLINT(readability-identifier-naming)
+    ASTString warm_start_array;              // NOLINT(readability-identifier-naming)
   } ann;
 
   /// Command line options

diff --git a/lib/ast.cpp b/lib/ast.cpp
@@ -2361,6 +2361,13 @@ Constants::Constants() {
   ann.mzn_evaluate_once->type(Type::ann());
   ann.promise_commutative = addId("promise_commutative");
   ann.promise_commutative->type(Type::ann());
+  ann.seq_search = addString("seq_search");
+  ann.int_search = addString("int_search");
+  ann.bool_search = addString("bool_search");
+  ann.float_search = addString("float_search");
+  ann.set_search = addString("set_search");
+  ann.warm_start = addString("warm_start");
+  ann.warm_start_array = addString("warm_start_array");
 
   cli.cmdlineData_short_str = addString("-D");
   cli.cmdlineData_str = addString("--cmdline-data");

diff --git a/lib/typecheck.cpp b/lib/typecheck.cpp
@@ -2762,6 +2762,33 @@ class Typer {
       fi = _model->matchFn(_env, call, true, true);
     }
 
+    if (fi != nullptr && fi->e() == nullptr && fi->paramCount() >= 1 &&
+        fi->param(0)->type().dim() != 0 &&
+        (fi->id() == _env.constants.ann.seq_search || fi->id() == _env.constants.ann.int_search ||
+         fi->id() == _env.constants.ann.bool_search ||
+         fi->id() == _env.constants.ann.float_search || fi->id() == _env.constants.ann.set_search ||
+         fi->id() == _env.constants.ann.warm_start ||
+         fi->id() == _env.constants.ann.warm_start_array)) {
+      // Need to make sure first argument is 1d and 1-based
+      GCLock lock;
+      auto* array = call->arg(0);
+      auto* array1d =
+          Call::a(Expression::loc(array).introduce(), _env.constants.ids.array1d, {array});
+      array1d->decl(_model->matchFn(_env, array1d, true, true));
+      Expression::type(array1d, Expression::type(array));
+      call->arg(0, array1d);
+      if ((fi->id() == _env.constants.ann.warm_start ||
+           fi->id() == _env.constants.ann.warm_start_array) &&
+          fi->paramCount() == 2 && fi->param(1)->type().dim() != 0) {
+        auto* array = call->arg(1);
+        auto* array1d =
+            Call::a(Expression::loc(array).introduce(), _env.constants.ids.array1d, {array});
+        array1d->decl(_model->matchFn(_env, array1d, true, true));
+        Expression::type(array1d, Expression::type(array));
+        call->arg(1, array1d);
+      }
+    }
+
     if ((fi->e() != nullptr) && Expression::isa<Call>(fi->e())) {
       Call* next_call = Expression::cast<Call>(fi->e());
       if ((next_call->decl() != nullptr) && next_call->argCount() == fi->paramCount() &&

diff --git a/tests/spec/unit/regression/github_768.fzn b/tests/spec/unit/regression/github_768.fzn
@@ -0,0 +1,3 @@
+var 1..2: X_INTRODUCED_1_;
+array [1..1] of var int: X_INTRODUCED_0_:: output_array([1..1]) = [X_INTRODUCED_1_];
+solve :: seq_search([int_search([X_INTRODUCED_1_],input_order,indomain_min,complete),warm_start([X_INTRODUCED_1_],[1])]) satisfy;
diff --git a/tests/spec/unit/regression/github_768.mzn b/tests/spec/unit/regression/github_768.mzn
@@ -0,0 +1,14 @@
+/***
+!Test
+expected: !FlatZinc 'github_768.fzn'
+solvers: [gecode]
+type: compile
+***/
+
+% Regression test for bug where the search annotation ended up with an array1d call
+
+array [0..0] of var 1..2: x;
+ann: s = int_search(x, input_order, indomain_min, complete);
+ann: t = warm_start(x, [0: 1]);
+ann: u = seq_search([3: s, t]);
+solve :: u satisfy;