HoistGuard also needs to check the arity

[wlaw59]

This means that we need to be able to iterate over the constraints and examine each of the variables that we encounter. I have no idea how to do this… To avoid having to learn I am printing out all of the different ways that we can examine arity. Found it: max_ufs_arity_of_set.
Also, this revealed another bug. hoistGuard also needs to check the arity. However, the example as Eddie gave it to me doesn’t quite work. I have edited the example above, but more work needs to be done.

Mahdi - Dependence relation from forward sole CSC that needs inspector
{ [ In_2, In_4, Out_2] : Li(In_2,In_4) = Out_2 && 0 <= In_2 && 0 <= Out_2 && In_2 < Out_2 && In_2 < n && In_4 < Lp_(In_2) && Lp(In_2) < In_4 && Out_2 < n }

symbolic Li(2);
symbolic Lp(1);
symbolic Lp_(1);
symbolic n;
S := {[i,j,k] : Li(i,j) = k && 0 <= i && 0<= k && i < k && i < n && j < Lp_(i) && Lp(i) < j && k < n};

for(t1 = 0; t1 <= n-2; t1++) {
  for(t2 = Lp(t1)+1; t2 <= Lp_(t1)-1; t2++) {
    if (n >= Li(t1,t2)+1 && Li(t1,t2) >= t1+1) {
      t3=Li(t1,t2);
      s0(t1,t2,t3);
    }
  }
}

Mahdi: The output code is correct and optimized

Mahdi - Incomplete Cholesky dependence relation

Original:
R22 = { [i1, i2, i3, i4, o1, o2] : o2 = i3 && rowIdx(i2) = o1 && rowIdx(i4) = rowIdx(i3) && 0 <= i1 && 0 <= o1 && i2 <= i4 && colPtr(rowIdx(i2)) <= i3 && rowIdx(i4 + 1) <= rowIdx(i4) && i1 < o1 && i1 + 1 < n && i2 < colPtr(i1 + 1) && colPtr(i1) < i2 && i3 < colPtr(rowIdx(i2) + 1) && i4 < colPtr(i1 + 1) && o1 + 1 < n && o2 < colPtr(o1 + 1) && colPtr(o1) < o2 }

Conversion to Omega:

symbolic n;
symbolic rowIdx(2);
symbolic rowIdx_(3);
symbolic rowIdx__(4);
symbolic rowIdx___(4);
symbolic colPtr(1);
symbolic colPtr_(1);
symbolic colPtr__(5);
symbolic colPtr___(5);
symbolic colPtr____(2);
symbolic colPtr_____(2);

S := { [i1, i2, i3, i4, o1, o2] : o2 = i3 && rowIdx(i1,i2) = o1 && rowIdx__(i1,i2,i3,i4) = rowIdx_(i1,i2,i3) && 0 <= i1 && 0 <= o1 && i2 <= i4 && colPtr____(i1,i2) <= i3 && rowIdx___(i1,i2,i3,i4) <= rowIdx__(i1,i2,i3,i4) && i1 < o1 && i1 + 1 < n && i2 < colPtr_(i1) && colPtr(i1) < i2 && i3 < colPtr_____(i1,i2) && i4 < colPtr_(i1) && o1 + 1 < n && o2 < colPtr___(i1,i2,i3,i4,o1) && colPtr__(i1,i2,i3,i4,o1) < o2 };

Codegen S;
Mahdi: Output from omega in Touwen’s master branch:

for(t1 = 0; t1 <= n-3; t1++) {
  for(t2 = colPtr(t1)+1; t2 <= colPtr_(t1)-1; t2++) {
    if (rowIdx(t1,t2) >= t1+1 && n >= rowIdx(t1,t2)+2) {
      for(t3 = colPtr____(t1,t2); t3 <= colPtr_____(t1,t2)-1; t3++) {
        for(t4 = t2; t4 <= colPtr_(t1)-1; t4++) {
          if (rowIdx__(t1,t2,t3,t4) == rowIdx_(t1,t2,t3) && rowIdx__(t1,t2,t3,t4) >= rowIdx___(t1,t2,t3,t4)) {
            t5=rowIdx(t1,t2);
            if (colPtr___(t1,t2,t3,t4,t5) >= t3+1 && t3 >= colPtr__(t1,t2,t3,t4,t5)+1) {
              s0(t1,t2,t3,t4,t5,t3);
            }
          }
        }
      }
    }
  }
}

Mahdi: The output code seems to be correct and optimized

Mahdi - Forward Solve original code

symbolic Lp_(1);
symbolic n;
S1 := { [ j, 0, 0, 0] : 0 <= j < n }
S2 := { [j, 0, p, 0] : 0 <= j < n && Lp(j) < p < Lp_(j) }
codegen S1,S2;

Failing example:

Copyright (C) 2011-2012 University of Utah

symbolic Lp(1);
symbolic n;
S1 := { [ j, 0, 0, 0] : 0 <= j < n };
S2 := { [j, 0, p, 0] : 0 <= j < n && Lp(j) < p < Lp_(j) };
Function Lp_ not declared
...skipping to statement end...
symbolic Lp_(1);
S2 := { [j, 0, p, 0] : 0 <= j < n && Lp(j) < p < Lp_(j) };
codegen S1,S2;
oc: ../../../../chill-dev-tuowen/omega/omega_lib/obj/../src/RelVar.cc:27: omega::Var_Decl* omega::Rel_Body::get_local(omega::Global_Var_ID): Assertion `G->arity() == 0' failed.
Aborted (core dumped)
symbolic Lp(1);
symbolic Lp_(1);
symbolic n;
S1 := { [ j, 0] : 0 <= j < n };
S2 := { [j, p] : 0 <= j < n && Lp(j) < p < Lp_(j) };
codegen S1,S2;

codegen S1,S2 given {[j] : Lp(j) > 0};

Tuowen:
without given clause:

for(t1 = 0; t1 <= n-1; t1++) {
  if (Lp(t1) >= 0) {
    s0(t1,0);
  }
  for(t2 = Lp(t1)+1; t2 <= min(Lp_(t1)-1,-1); t2++) {
    s1(t1,t2);
  }
  if (Lp(t1) <= -1 && Lp_(t1) >= 1) {
    s0(t1,0);
    s1(t1,0);
  }
  for(t2 = max(Lp(t1)+1,1); t2 <= Lp_(t1)-1; t2++) {
    s1(t1,t2);
  }
  if (Lp_(t1) <= 0 && Lp(t1) <= -1) {
    s0(t1,0);
  }
}

With given clause:
for(t1 = 0; t1 <= n-1; t1++) {
  s0(t1,0);
  for(t2 = Lp(t1)+1; t2 <= Lp_(t1)-1; t2++) {
    s1(t1,t2);
  }
}

Mahdi: The output code that says “With given clause” is our expected code.

Union:

symbolic Lp(1);
symbolic Lp_(1);
symbolic n;
S := { [ j, 0] : 0 <= j < n } union { [j, p] : 0 <= j < n && Lp(j) < p < Lp_(j) };
codegen S;

Tuowen:
for(t1 = 0; t1 <= n-1; t1++) {
  for(t2 = Lp(t1)+1; t2 <= min(Lp_(t1)-1,-1); t2++) {
    s0(t1,t2);
  }
  s0(t1,0);
  for(t2 = max(Lp(t1)+1,1); t2 <= Lp_(t1)-1; t2++) {
    s0(t1,t2);
  }
}