How to dynamically rewrite CLP(FD) constraints to help reification

Question

My question is linked to this (now 1-year-old) post regarding reification issues in a CLP(FD) program : link

The prolog file I give to the SWI engine is programmatically written on-the-fly, based on some data that users can add/edit/remove with another application (the same that calls the engine afterwards).

I want to detect some special cases to dynamically rewrite constraints to help the "engine" find the smallest possible domains. An example :

 constr(X,Y,Z) :-
   X in {1,2,3,4,5,6,7},
   Y in {3,5,7},
   Z in {1,2},
   ((X #= 3)) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   ((Z #= 1)) #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

If I call constr(3,Y,Z)., I get Z #= 1 or Z #= 2.

One solution is to automatically replace the last two lines by

((X #= 3)) #==> T, 
((Z #= 1)) #<==> T, 
T #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)).

With this one I get Z #= 1.

The trouble is I can have this :

   ((X #= 3)) #==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   ((Z #= 1)) #<==> ((Y mod 7 #= 0) #\/ (Y mod 3 #= 0)).

How to detect this ? Can the Prolog engine help me to do this ? I thought I could programmatically replace each right operand by a reification variable :

   ((X #= 3)) #==> J,
   ((Z #= 1)) #<==> K,
   J #<==> ((Y mod 3 #= 0) #\/ (Y mod 7 #= 0)),
   K #<==> ((Y mod 7 #= 0) #\/ (Y mod 3 #= 0)).

But in that case the same "reification" problem occurs.

Thanks for your help.