Dvlab Open Wiki
Modulo misbehavior
- Submitted by: Marco
- Date: Dec 29th, 2005
- Assigned to: nobody.
This seems to be a glu-2.0 bug, and we have asked the glu developers for help.
Consider the variable:
var x: [0..3];
The expression x' = x mod 3 gives rise to the following mdd:
( (x = 0)( (x' = 0)) + (x = 1)( (x' = 1)) + (x = 2)( (x' = 2)) ).
Where did ((x = 3)(x' = 0)) go??
Moreover, if x has range [0..8], the same expression gives rise to an mdd containing the (unjustified) term:
(x = 8)(
(x' = 1)
+
(x' = 2)).
I cannot find any problem with our code. The problem seems to be with Glu, and the implementation of mdd_mod is way above my head. - Marco
Pritam and I created a C version of this bug, and tried a few different parameters. What we found is that the mdd_mod code seems to work if the variable ranges are a power of 2 ([0..7]) and the modulus is even. Thus, using a range of [0..7] and a modulus of 6 works perfectly. (Note that you have to modify mdd_mod to see this clearly; there are some combinations that will appear to work because of the modulus restriction. We took out the modulus restriction to see all the possible values that are equivalent.) - Bo