Merge branch 'master' into doe

1 files changed, 58 insertions, 0 deletions

diff --git a/omega/examples/experiments/gemm/gemm.out b/omega/examples/experiments/gemm/gemm.out
new file mode 100644
index 0000000..dfd0156
--- /dev/null
+++ b/omega/examples/experiments/gemm/gemm.out
@@ -0,0 +1,58 @@
+>>> symbolic n, over1, over2;
+>>> s0:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta,tau : 2tau = 1+t10 && 2alpha = 1+t8 && t2 = 1+512beta && t4 = 1+128gamma && t6 = 1+8delta && t1 = 0 && t3 = 0 && t5 = 1 && t7 = 2 && t9 = 1 && t11 = 0 && t13 = 0 && 1, t12-511 <= t2 <= t12 <= n && 1, t10-6 <= t6 <= t10 && 1, t8-126 <= t4 <= t8 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && over2+t10 <= n && over1+t8 <= n) };
+>>> s1:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta : t4 = 1+128beta && t2 = 1+512alpha && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 0 && t9 = 0 && 1, t8-127 <= t4 <= t8 <= n && 1, t2 <= t6 <= n, t2+511 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+>>> s2:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma : t6 = 1+8gamma && t4 = 1+128alpha && t2 = 1+512beta && t5 = 1 && t9 = 0 && t11 = 0 && t1 = 0 && 1+t7 = 0 && t3 = 0 && 1, t10-511 <= t2 <= t10 <= n && 1, t8-7 <= t6 <= t8 <= n && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 1 <= t4 <= n) };
+>>> s3:= { [t1,t2,t3,t4,t5,t6,t7] : exists ( alpha,beta,gamma : t6 = 1+8gamma && t4 = 1+128alpha && t2 = 1+512beta && t5 = 1 && t1 = 0 && t7 = 0 && t3 = 0 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 1 <= t2 <= n && 1 <= t4 <= n && 1 <= t6 <= n) };
+>>> s4:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma : t6 = 1+8beta && t4 = 1+128gamma && t2 = 1+512alpha && n = t8 && over1 = 1 && t5 = 1 && t9 = 0 && t11 = 0 && t13 = 0 && t1 = 0 && t7 = 4 && t3 = 0 && 1, t12-511 <= t2 <= t12 <= t8 <= t4+127 && 1, t10-7 <= t6 <= t10 <= t8 && 0 <= over2 <= 1 && t4 <= t8) };
+>>> s5:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta,tau : 2tau = 1+t10 && 2alpha = 1+t8 && t2 = 1+512beta && t4 = 1+128gamma && t6 = 1+8delta && t1 = 0 && t3 = 0 && t5 = 1 && t7 = 2 && t9 = 1 && t11 = 0 && t13 = 1 && 1, t12-511 <= t2 <= t12 <= n && 1, t10-6 <= t6 <= t10 && 1, t8-126 <= t4 <= t8 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && over2+t10 <= n && over1+t8 <= n) };
+>>> s6:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta,gamma,delta : t6 = 1+8delta && 2alpha = 1+t8 && t2 = 1+512beta && t4 = 1+128gamma && 1+t9 = 0 && t7 = 2 && t1 = 0 && t3 = 0 && t5 = 1 && 1, t8-126 <= t4 <= t8 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && 1 <= t2 <= n && 1 <= t6 <= n && over1+t8 <= n) };
+>>> s7:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t6 = 1+8beta && 2alpha = t8+t4 && t2 = 1+512delta && 1+128gamma = t4 && t10 = n && over2 = 1 && t5 = 1 && t7 = 2 && t11 = 0 && t13 = 0 && t1 = 0 && t9 = 2 && t3 = 0 && 1, t12-511 <= t2 <= t12 <= n <= t6+7 && 1, t8-126 <= t4 <= t8 && 0 <= over1 <= 1 && t6 <= n && over1+t8 <= n) };
+>>> s8:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t6 = 1+8beta && 2alpha = t8+t4 && t2 = 1+512delta && 1+128gamma = t4 && t10 = n && over2 = 1 && t5 = 1 && t7 = 2 && t11 = 0 && t13 = 1 && t1 = 0 && t9 = 2 && t3 = 0 && 1, t12-511 <= t2 <= t12 <= n <= t6+7 && 1, t8-126 <= t4 <= t8 && 0 <= over1 <= 1 && t6 <= n && over1+t8 <= n) };
+>>> s9:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta,tau : 2delta = 1+t10 && 2alpha = 1+t8 && t2 = 1+512beta && t4 = 1+128gamma && t6+8tau = 1 && t13 = 2 && t9 = 1 && t11 = 0 && t1 = 0 && t3 = 0 && t5 = 1 && t7 = 2 && 1, t12-511 <= t2 <= t12 <= n && 1, t10-6 <= t6 <= t10 && 1, t8-126 <= t4 <= t8 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && over2+t10 <= n && over1+t8 <= n) };
+>>> 
+>>> codegen 1 s0,s1,s2,s3,s4,s5,s6,s7,s8,s9;
+if (over1 >= 0 && over2 >= 0 && over2 <= 1 && over1 <= 1) {
+  for(t2 = 1; t2 <= n; t2 += 512) {
+    for(t4 = 1; t4 <= n; t4 += 128) {
+      for(t6 = t2; t6 <= min(n,t2+511); t6++) {
+        for(t8 = t4; t8 <= min(t4+127,n); t8++) {
+          s1(0,t2,0,t4,0,t6,0,t8,0);
+        }
+      }
+      for(t6 = 1; t6 <= n; t6 += 8) {
+        for(t8 = t6; t8 <= min(n,t6+7); t8++) {
+          for(t10 = t2; t10 <= min(t2+511,n); t10++) {
+            s2(0,t2,0,t4,1,t6,-1,t8,0,t10,0);
+          }
+        }
+        s3(0,t2,0,t4,1,t6,0);
+        for(t8 = t4; t8 <= min(-over1+n,t4+126); t8 += 2) {
+          s6(0,t2,0,t4,1,t6,2,t8,-1);
+          for(t10 = t6; t10 <= min(t6+6,-over2+n); t10 += 2) {
+            for(t12 = t2; t12 <= min(n,t2+511); t12++) {
+              s0(0,t2,0,t4,1,t6,2,t8,1,t10,0,t12,0);
+              s5(0,t2,0,t4,1,t6,2,t8,1,t10,0,t12,1);
+              s9(0,t2,0,t4,1,t6,2,t8,1,t10,0,t12,2);
+            }
+          }
+          if (over2 >= 1 && t6 >= n-7) {
+            for(t12 = t2; t12 <= min(n,t2+511); t12++) {
+              s7(0,t2,0,t4,1,t6,2,t8,2,n,0,t12,0);
+              s8(0,t2,0,t4,1,t6,2,t8,2,n,0,t12,1);
+            }
+          }
+        }
+        if (t4 >= n-127 && over1 >= 1) {
+          for(t10 = t6; t10 <= min(n,t6+7); t10++) {
+            for(t12 = t2; t12 <= min(n,t2+511); t12++) {
+              s4(0,t2,0,t4,1,t6,4,n,0,t10,0,t12,0);
+            }
+          }
+        }
+      }
+    }
+  }
+}
+
+>>> 
+>>>