bool_clause_reif constraints are lost when array_bool_or is redefined

[scand1sk]

I simply redefined the array_bool_or predicate for my solver in my custom redefinitions.mzn file:

predicate array_bool_or(array[int] of var bool: v, var bool: r) = 
    bool_clause_reif(v, [], r);

However, when flattening the 1d_rubiks_cube.mzn problem (attached), the obtained FlatZinc misses all these constraints, and I obtain incorrect answers. array_bool_and constraints are also missing when array_bool_or is redefined. The model generates a few warnings during the flattening, but the obtained FlatZinc is correct when I disable my redefinition.

1d_rubiks_cube.mzn.zip

[guidotack]

The problem here is that you are essentially creating a cyclic redefinition: array_bool_or is rewritten to a clause, and then the clause is again rewritten to array_bool_or (this is hard-coded into the compiler and not controlled by a redefinitions file). The compiler currently doesn't detect and reject this case, and it assumes that it already compiled the array_bool_or so it does not emit any code for it.

If you need to rewrite array_bool_or to a reified clause, you will have to change the redefinition to generate the FlatZinc-level representation, e.g. like this:

predicate array_bool_or(array[int] of var bool: v, var bool: r) =
  bool_clause(v,[r]) /\
  forall (i in index_set(v)) (v[i] -> r);

I should probably add a check for these cyclic definitions so that they result in a proper error message, but it's not that easy (because the cycle is only introduced through the rewriting that's happening inside the compiler).

[scand1sk]

Maybe you cloud detect redefinitions of hard-coded predicates and at least produce a warning?

Le sam. 11 juin 2016 à 04:29, Guido Tack notifications@github.com a écrit :

The problem here is that you are essentially creating a cyclic redefinition: array_bool_or is rewritten to a clause, and then the clause is again rewritten to array_bool_or (this is hard-coded into the compiler and not controlled by a redefinitions file). The compiler currently doesn't detect and reject this case, and it assumes that it already compiled the array_bool_or so it does not emit any code for it.

If you need to rewrite array_bool_or to a reified clause, you will have to change the redefinition to generate the FlatZinc-level representation, e.g. like this:

predicate array_bool_or(array[int] of var bool: v, var bool: r) = bool_clause(v,[r]) /\ forall (i in index_set(v)) (v[i] -> r);

I should probably add a check for these cyclic definitions so that they result in a proper error message, but it's not that easy (because the cycle is only introduced through the rewriting that's happening inside the compiler).

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/MiniZinc/libminizinc/issues/105#issuecomment-225331985, or mute the thread https://github.com/notifications/unsubscribe/AC67NXf8i-PsOXKM4cWZGtHMCM04Pac4ks5qKh2mgaJpZM4IwzvS .

[Dekker1]

array_bool_or is no longer produced since 2.7.0