MiniZinc
bool_clause_reif constraints are lost when array_bool_or is redefined
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.
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).
Maybe you cloud detect redefinitions of hard-coded predicates and at least produce a warning?
Le sam. 11 juin 2016 à 04:29, Guido Tack [email protected] 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 .
