Non-Redundant constraint

[wlaw59]

I still wanted to confirm this. The following example has a non-redundant constraint.

>>> symbolic N;
>>> symbolic F(1);
>>> symbolic col(2);
>>> S := {[i,j,k]  : 0<=i<N and 0<=j<F(i) and k=col(i,j)};

S := {[i,j] : 0<=i<N and 0<=j<N and j=F(i)};

The non-redundant constraint is not removed, and it is place in the correct position.

for(t1 = 0; t1 <= N-1; t1++) {
  for(t2 = 0; t2 <= F(t1)-1; t2++) {
    t3=col(t1,t2);
    s0(t1,t2,t3);
  }
}

Update
Eddie gave me an example that reveals another bug with this .

symbolic NNZ,N_C,N_R,index(1),index1(1),col(3);
Idense := { [i, k, j] : k - col(i,k,j) = 0 && i >= 0 && k >= 0 && index(i) >= 0 && j - index(i) >= 0 && NNZ - index1(i) >= 0 && -i + N_R - 1 >= 0 && -k + N_C - 1 >= 0 && -j + index1(i) - 1 >= 0 };
codegen(Idense);

Here is a more simple case of the same problem:
S := {[i,j] : 0<=i<N and 0<=j<N and j=G(i,j)};

Tuowen’s output

if (N_C >= 1 && NNZ >= 1) { 
  for(t1 = 0; t1 <= N_R-1; t1++) {
    if (index(t1) >= 0 && index1(t1) >= index(t1)+1 && NNZ >= index1(t1)) {
      for(t2 = 0; t2 <= N_C-1; t2++) {
        for(t3 = index(t1); t3 <= index1(t1)-1; t3++) {
          if (t2 == col(t1,t2,t3)) {
            s0(t1,t2,t3);
         }
       }
    }
}
}
}

It appears that the function max_ufs_arity looks at the input and output variables and since the guard keeps the ufs in the input tuple even when that uf is not used in a constraint the max arity is never reduced past 3. I need to add a new function that calculates the arity based on the ufs that are actually used in the constraints, since that is what will impact the codegen.