equivalent regular expression and DFA flatten differently in (at least) Gecode

[Pierre-Flener]

A student (Niclas Soika) in my course found the following bug. Try the model below (the example is mine) with Gecode: with only line 6 commented away (as below), we get the expected 1 constraint (gecode_regular), but with instead only the equivalent line 7 commented away, we get n constraints (gecode_int_element2d).

include "globals.mzn";
int: n; % length of X
enum Alphabet = {s,t};  enum State = {a,b,c,d,e};
array[State,Alphabet] of opt State: Transition = [| b,c | d,<> | e,<> | <>,b | c,e |];
array[1..n] of var Alphabet: X;
% constraint regular(X,Transition,a,{d,e});
constraint regular(X,"s s (t s)* | t s (t | s s)*");
solve satisfy;

This seems to be an oversight of the global enum surgery, leading for a provided DFA to fzn_regular_set, for which the bundled Gecode backend was not updated.

I post this here since this might not be limited to Gecode, so other backend designers may want to check their code.

[zayenz]

Looking into it, the difference is that the new enum-based version of regular rewrites into fzn_regular_set instead of fzn_regular. For some reason, we've never had that handled in Gecode, and that should be added since it doesn't seem to be anything that is problematic for supporting it.

In general, it would be good to have a list of all the base predicates in the FlatZinc library that one might want to override somewhere in https://docs.minizinc.dev/en/stable/fzn-spec.html, I had no idea that fzn_regular_set even existed.

[krzku]

It is a good idea to add fzn_regular_set to solver's library. I have added it to JaCoP but got the following error from minizinc compiler.

Error: type error: Type array[int,int] of int is not allowed in as a FlatZinc builtin argument, arrays must be one dimensional
/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc/std/fzn_regular_set.mzn.deprecated.mzn:5.3-28

It seems that definition fzn_regular_set.mzn.deprecated.mzn needs to be removed to make it working. When removed, JaCoP solves the problem correctly with one regular constraint ;)

[Pierre-Flener]

The same phenomenon happens for Gecode with cost_regular and a cost-DFA.

I guess there is no easy work-around (for my students) until the next version.

[guidotack]

Thanks for reporting this. @Pierre-Flener, if you can ask your students to modify the MiniZinc library, a workaround is to change the file regular.mzn to dispatch to the non-set version if possible (this should cover almost all cases). Here is the modified predicate:

predicate regular(
  array [$$X] of var $$Val: x,
  array [$$State, $$Val] of opt $$State: d,
  $$State: q0,
  set of $$State: F,
) =
  let {
    any: State = enum2int(index_set_1of2(d));
    any: Val = enum2int(index_set_2of2(d));
    any: q_off = enum2int(min(State)) - 1;
    any: dd =
      array2d(
        State,
        Val,
        [if occurs(d_sv) then enum2int(deopt(d_sv)) - q_off else 0 endif | d_sv in d],
      );
    any: qq0 = enum2int(q0) - q_off;
    any: FF = {enum2int(i) - q_off | i in F};
  } in
  if min(Val) = 1 then fzn_regular(index2int(enum2int(x)), card(State), max(Val), dd, qq0, FF)
  else fzn_regular_set(index2int(enum2int(x)), card(State), Val, dd, qq0, FF) endif;

This will be part of the next release. In addition, we'll add support for fzn_regular_set to Gecode.

@krzku, the trick to overriding this constraint in the solver library is to define the "real" solver built-in using a 1d array, and then rewrite into that version:

predicate jacop_regular_set(
  array [int] of var int: x,
  int: Q,
  set of int: S,
  array [int] of int: d,
  int: q0,
  set of int: F,
);

predicate fzn_regular_set(
  array [int] of var int: x,
  int: Q,
  set of int: S,
  array [int, int] of int: d,
  int: q0,
  set of int: F,
) = jacop_regular_set(x, Q, S, array1d(d), q0, F);

This works because you know that the index set of d is [1..Q, S], so you can do the 1d-indexing in your own code.

[Pierre-Flener]

Thanks for the workaround @guidotack!
Do you also have one for cost_regular?
One of my student groups has a real-world sports scheduling model that relies heavily on it.

[krzku]

Unfortunately your definition gives the following error if I keep fzn_regular_deprecated.mzn :(

Error: type error: Type array[int,int] of int is not allowed in as a FlatZinc builtin argument, arrays must be one dimensional
/Applications/MiniZincIDE.app/Contents/Resources/share/minizinc/std/fzn_regular_set.mzn.deprecated.mzn:5.3-28

It works if I remove the file fzn_regular_deprecated.mzn.

[krzku]

BTW, in my original definition of jacop_regular_set I already used 1d array.

[krzku]

I think, I know what creates the problem. I pass additional parameter, minimial index of d. My definitions are as follows.

predicate jacop_regular_set(array[int] of var int: x, int: Q, set of int: S,
array[int] of int: d, int: q0, set of int: F, int: min_index);

predicate fzn_regular_set(array[int] of var int: x, int: Q, set of int: S,
array[int,int] of int: d, int: q0, set of int: F) =
jacop_regular_set(x, Q, S, array1d(d), q0, F, min(index_set_2of2(d)))
;

It seems that parameter min(index_set_2of2(d)) triggers an error but only when deprecation definition is present.

[guidotack]

@Pierre-Flener I don't think we have a cost_regular propagator in Gecode (at least I couldn't find one right now, @zayenz correct me if I'm wrong). I guess if you want the stronger filtering, you could try posting a regular constraint as a redundant constraint in addition to cost_regular.

@krzku You need to copy the following definition for the deprecated call from the standard library fzn_regular_set.mzn file into your version, that should get rid of the compilation issues:

% Deprecated call
predicate fzn_regular(
  array [int] of var int: x,
  int: Q,
  set of int: S,
  array [int, int] of int: d,
  int: q0,
  set of int: F,
) = fzn_regular_set(x, Q, S, d, q0, F);

[zayenz]

@Pierre-Flener I don't think we have a cost_regular propagator in Gecode (at least I couldn't find one right now, @zayenz correct me if I'm wrong). I guess if you want the stronger filtering, you could try posting a regular constraint as a redundant constraint in addition to cost_regular.

No, we don't have a cost-regular, and I wonder what systems if any have that implemented? SICStus can probably use the case constraint as a way to model it.

In general, I think it would be good if the standard decomposition of cost_regular in MiniZInc posted the base regular constraint, as a way to let solvers that handle regular automatically pick it up instead of always decomposing it fully.

[Pierre-Flener]

Thanks @guidotack and @zayenz for your helpful replies!