Why does MiniZinc sometimes not use regular constraint defined by a solver?

Question

According to the docs, "global constraints ... can be specialized for the particular solver". Indeed, for nurse rostering problem the FlatZinc model does use solver defined regular predicate (e.g. chuffed_regular, ortools_regular).

For an unclear reason MiniZinc does not use such solver provided predicate for the following model:

include "globals.mzn";

int: cnt;
int: tableMaxRowSize;
array[1..cnt] of 0..tableMaxRowSize: tableRowSizes;
array[1..cnt, 1..tableMaxRowSize] of 0..cnt: theTable;

enum Value = {
    NONE,
    A,
    B
};
array[1..cnt] of var Value: values;
array[1..cnt, 1..tableMaxRowSize] of var Value: paths;


constraint forall (i in 1..cnt) (
    tableRowSizes[i] = 0
    \/
    forall (j in 1..tableRowSizes[i]) (
        paths[i, j] = values[theTable[i, j]]
    )
);

enum ValueAlphabet = {NULL} ++ toValueAlphabet(Value);
int: Q = 4; set of 1..Q: states = 1..Q;
array[states, ValueAlphabet] of int: transitionTable = [|
    1, 1, 1, 1, |
    1, 2, 3, 0, |
    1, 3, 0, 4, |
    1, 4, 0, 0, |
|];

constraint forall (i in 1..cnt) (
    regular(
        [toValueAlphabet(paths[i, j]) | j in 1..tableRowSizes[i]] ++ [NULL],
        Q,
        ValueAlphabet,
        transitionTable,
        2,
        {1}
    )
);

solve maximize sum (t in values) (t != NONE);

output [format(t) ++ "\n" | t in values];

Compiling the model above with the data below (minizinc --solver org.chuffed.chuffed -s model.mzn data.dzn -c)

cnt = 3;
tableMaxRowSize = 3;
tableRowSizes = [0,0,3];
theTable = [|0,0,0,|0,0,0,|1,2,3|];

yields a fzn-file with no mentions of chuffed_regular predicate:

array [1..16] of int: X_INTRODUCED_30_ = [1,1,1,1,1,2,3,0,1,3,0,4,1,4,0,0];
var 1..3: X_INTRODUCED_0_;
var 1..3: X_INTRODUCED_1_;
var 1..3: X_INTRODUCED_2_;
var 0..3: X_INTRODUCED_12_:: is_defined_var;
var bool: X_INTRODUCED_13_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_14_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_15_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_16_ ::var_is_introduced :: is_defined_var;
var bool: X_INTRODUCED_17_ ::var_is_introduced :: is_defined_var;
var 0..1: X_INTRODUCED_18_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_41_ ::var_is_introduced :: is_defined_var;
var 6..8: X_INTRODUCED_42_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_43_ ::var_is_introduced :: is_defined_var;
var 2..16: X_INTRODUCED_45_ ::var_is_introduced :: is_defined_var;
var 1..4: X_INTRODUCED_46_ ::var_is_introduced :: is_defined_var;
var 2..16: X_INTRODUCED_47_ ::var_is_introduced :: is_defined_var;
var 1..13: X_INTRODUCED_50_ ::var_is_introduced :: is_defined_var;
var 1..1: X_INTRODUCED_29_ ::var_is_introduced  = 1;
var 1..1: X_INTRODUCED_48_ ::var_is_introduced  = 1;
array [1..3] of var int: values:: output_array([1..3]) = [X_INTRODUCED_0_,X_INTRODUCED_1_,X_INTRODUCED_2_];
constraint array_int_element(X_INTRODUCED_42_,X_INTRODUCED_30_,X_INTRODUCED_41_);
constraint array_int_element(X_INTRODUCED_45_,X_INTRODUCED_30_,X_INTRODUCED_43_);
constraint array_int_element(X_INTRODUCED_47_,X_INTRODUCED_30_,X_INTRODUCED_46_);
constraint array_int_element(X_INTRODUCED_50_,X_INTRODUCED_30_,1);
constraint int_lin_eq([1,1,1,-1],[X_INTRODUCED_14_,X_INTRODUCED_16_,X_INTRODUCED_18_,X_INTRODUCED_12_],0):: defines_var(X_INTRODUCED_12_);
constraint int_ne_reif(X_INTRODUCED_0_,1,X_INTRODUCED_13_):: defines_var(X_INTRODUCED_13_);
constraint bool2int(X_INTRODUCED_13_,X_INTRODUCED_14_):: defines_var(X_INTRODUCED_14_);
constraint int_ne_reif(X_INTRODUCED_1_,1,X_INTRODUCED_15_):: defines_var(X_INTRODUCED_15_);
constraint bool2int(X_INTRODUCED_15_,X_INTRODUCED_16_):: defines_var(X_INTRODUCED_16_);
constraint int_ne_reif(X_INTRODUCED_2_,1,X_INTRODUCED_17_):: defines_var(X_INTRODUCED_17_);
constraint bool2int(X_INTRODUCED_17_,X_INTRODUCED_18_):: defines_var(X_INTRODUCED_18_);
constraint int_lin_eq([1,-1],[X_INTRODUCED_0_,X_INTRODUCED_42_],-5):: defines_var(X_INTRODUCED_42_):: domain;
constraint int_lin_eq([1,4,-1],[X_INTRODUCED_1_,X_INTRODUCED_41_,X_INTRODUCED_45_],3):: defines_var(X_INTRODUCED_45_):: domain;
constraint int_lin_eq([1,4,-1],[X_INTRODUCED_2_,X_INTRODUCED_43_,X_INTRODUCED_47_],3):: defines_var(X_INTRODUCED_47_):: domain;
constraint int_lin_eq([4,-1],[X_INTRODUCED_46_,X_INTRODUCED_50_],3):: defines_var(X_INTRODUCED_50_):: domain;
solve  maximize X_INTRODUCED_12_;

The above model is a simplified version of the actual model, which both Chuffed and OR-Tools fail to solve within reasonable time limit. Also I am sure that the reason for the poor solver performance is related to the regular constraint, because in the actual model I eliminated all the other constraints and the solving performance did not improve. On the other hand, removing transitions from the dfa transition table did improve the performance of the solvers.

Is such selective usage of the solver provided regular constraint an expected behavior of MiniZinc compiler? Can I somehow ask the compiler to use the solver provided regular constraint (e.g. with the help of an annotation)?

Answer 1

Predicate regular is called with set of ValueAlphabet as third parameter. But it expects an int.

I modified the include statement to

include "regular.mzn";

This resulted in the following error message:

MiniZinc: type error: no function or predicate with this signature found: `regular(array[int] of var ValueAlphabet,int,set of ValueAlphabet,array[int,ValueAlphabet] of int,int,set of int)'
Cannot use the following functions or predicates with the same identifier:
predicate regular(array[int] of var int: x,int: Q,int: S,array[int,int] of int: d,int: q0,set of int: F);
    (argument 3 expects type int, but type set of ValueAlphabet given)

I am not sure about the following line in your model:

enum ValueAlphabet = {NULL} ++ toValueAlphabet(Value);

What is toValueAlphabet supposed to do? I could not find it in the documentation.