diff options
Diffstat (limited to 'omega/examples/experiments/gemm/gemm.out')
| -rw-r--r-- | omega/examples/experiments/gemm/gemm.out | 58 |
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); + } + } + } + } + } + } +} + +>>> +>>> |