summaryrefslogtreecommitdiff
path: root/omega/examples/experiments
diff options
context:
space:
mode:
Diffstat (limited to 'omega/examples/experiments')
-rwxr-xr-xomega/examples/experiments/gemm/codegen.input14
-rw-r--r--omega/examples/experiments/gemm/gemm.out58
-rwxr-xr-xomega/examples/experiments/gemv/codegen.input14
-rw-r--r--omega/examples/experiments/gemv/gemv.out40
-rwxr-xr-xomega/examples/experiments/lu/codegen.input33
-rw-r--r--omega/examples/experiments/lu/lu.out141
-rwxr-xr-xomega/examples/experiments/qr/codegen.input17
-rw-r--r--omega/examples/experiments/qr/qr.out54
-rwxr-xr-xomega/examples/experiments/swim/swim-codegen.input53
-rw-r--r--omega/examples/experiments/swim/swim.out176
10 files changed, 600 insertions, 0 deletions
diff --git a/omega/examples/experiments/gemm/codegen.input b/omega/examples/experiments/gemm/codegen.input
new file mode 100755
index 0000000..cf1554b
--- /dev/null
+++ b/omega/examples/experiments/gemm/codegen.input
@@ -0,0 +1,14 @@
+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;
+
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);
+ }
+ }
+ }
+ }
+ }
+ }
+}
+
+>>>
+>>>
diff --git a/omega/examples/experiments/gemv/codegen.input b/omega/examples/experiments/gemv/codegen.input
new file mode 100755
index 0000000..4152560
--- /dev/null
+++ b/omega/examples/experiments/gemv/codegen.input
@@ -0,0 +1,14 @@
+symbolic n, over1, over2;
+
+s0:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+s1:= { [t1] : 1+t1 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= n };
+s2:= { [t1,t2,t3,t4,t5] : t1 = 2 && t3 = 0 && t5 = 0 && 1 <= t2 <= n && 1 <= t4 <= n && 0 <= over2 <= 3 && over1 <= 3 && n < over1+t2 };
+s3:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 1 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+s4:= { [t1,t2,t3] : exists ( alpha : t2 = 1+4alpha && 1+t3 = 0 && t1 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && over1+t2 <= n && 1 <= t2) };
+s5:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 0 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
+s6:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 1 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
+s7:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t5 = 2 && t1 = 1 && t3 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+
+codegen s0,s1,s2,s3,s4,s5,s6,s7;
+
+
diff --git a/omega/examples/experiments/gemv/gemv.out b/omega/examples/experiments/gemv/gemv.out
new file mode 100644
index 0000000..b9dd445
--- /dev/null
+++ b/omega/examples/experiments/gemv/gemv.out
@@ -0,0 +1,40 @@
+>>> symbolic n, over1, over2;
+>>>
+>>> s0:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+>>> s1:= { [t1] : 1+t1 = 0 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= n };
+>>> s2:= { [t1,t2,t3,t4,t5] : t1 = 2 && t3 = 0 && t5 = 0 && 1 <= t2 <= n && 1 <= t4 <= n && 0 <= over2 <= 3 && over1 <= 3 && n < over1+t2 };
+>>> s3:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t1 = 1 && t3 = 1 && t5 = 1 && 0 <= over2 <= 3 && 0 <= over1 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+>>> s4:= { [t1,t2,t3] : exists ( alpha : t2 = 1+4alpha && 1+t3 = 0 && t1 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && over1+t2 <= n && 1 <= t2) };
+>>> s5:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 0 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
+>>> s6:= { [t1,t2,t3,t4,t5] : exists ( alpha : t2 = 1+4alpha && t5 = 1 && t1 = 1 && t3 = 2 && 0 <= over1 <= 3 && 1 <= t4 <= n && over2 <= 3 && 1 <= t2 && over1+t2 <= n && n < over2+t4) };
+>>> s7:= { [t1,t2,t3,t4,t5] : exists ( alpha,beta : t2 = 1+4beta && t4 = 1+4alpha && t5 = 2 && t1 = 1 && t3 = 1 && 0 <= over1 <= 3 && 0 <= over2 <= 3 && 1 <= t4 && 1 <= t2 && over1+t2 <= n && over2+t4 <= n) };
+>>>
+>>> codegen s0,s1,s2,s3,s4,s5,s6,s7;
+if (over2 >= 0 && over1 <= 3 && over2 <= 3) {
+ if (over1 >= 0) {
+ if (n >= 1) {
+ s1(-1);
+ }
+ for(t2 = 1; t2 <= n-over1; t2 += 4) {
+ s4(1,t2,-1);
+ for(t4 = 1; t4 <= n-over2; t4 += 4) {
+ s0(1,t2,1,t4,0);
+ s3(1,t2,1,t4,1);
+ s7(1,t2,1,t4,2);
+ }
+ for(t4 = max(1,n-over2+1); t4 <= n; t4++) {
+ s5(1,t2,2,t4,0);
+ s6(1,t2,2,t4,1);
+ }
+ }
+ }
+ for(t2 = max(1,n-over1+1); t2 <= n; t2++) {
+ for(t4 = 1; t4 <= n; t4++) {
+ s2(2,t2,0,t4,0);
+ }
+ }
+}
+
+>>>
+>>>
+>>>
diff --git a/omega/examples/experiments/lu/codegen.input b/omega/examples/experiments/lu/codegen.input
new file mode 100755
index 0000000..0505f2d
--- /dev/null
+++ b/omega/examples/experiments/lu/codegen.input
@@ -0,0 +1,33 @@
+symbolic n, over1, over2, over3;
+
+s0:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+s1:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 1 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && t12-62, t14+2 <= t2 <= t8 <= t12 <= t8+6 && t2-1, t10-254 <= t6 <= t10 && 1, t14-255 <= t4 <= t14 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && over3+t12 <= n && over2+t10 <= n) };
+s2:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha : t2 = 2+64alpha && 1+t4 = t6 && t7 = 0 && t9 = 0 && t1 = 0 && t3 = 2 && t5 = 0 && 2, t6-63 <= t2 <= t6 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+s3:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha : t2 = 2+64alpha && t5 = 1 && t7 = 0 && t9 = 0 && t1 = 0 && t3 = 2 && t2-1 <= t4 < t6 <= t2+63, n && t4 < t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 2 <= t2) };
+s4:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2tau = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8+8sigma = 2 && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t15 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 <= t2+62 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && over1+t12 <= n) };
+s5:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta : t2 = 2+64beta && t4 = 2+256alpha && 1+t3 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t1 = 0 && t5 = 1 && 2, t6-255 <= t4 <= t10 < t6 <= t2-2 && t8-63 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+s6:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma : t4 = 2+256gamma && t6 = 1+256alpha && t2 = 2+64beta && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && 1+t7 = 0 && t9 = 0 && t11 = 0 && 1, t8-255 <= t6 <= t8 < t4 <= t10 <= t2-2, t4+255 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2 <= n) };
+s7:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t4 = 2+256alpha && t6 = 1+256beta && t2 = 2+64gamma && 1+t5 = 0 && t7 = 0 && t11 = 0 && t13 = 0 && t1 = 0 && 2+t9 = 0 && 1+t3 = 0 && t4+64, t10-63 <= t2 <= t8 <= t10 <= t8+7, n && 1, t12-255 <= t6 <= t12 <= t4-1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+s8:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t4 = 2+256alpha && t6 = 1+256beta && 2+t10 = t2 && t2 = 2+64gamma && t7 = 0 && t11 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t9 = 1 && 1+t3 = 0 && 1+t5 = 0 && t4+64, t12-63 <= t2 <= t8 <= t12 <= t8+7, n && 1, t14-255 <= t6 <= t14 <= t4-1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2 <= t4+256) };
+s9:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8 = 2+8tau && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t15 = 1 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t8 <= t2+56 && over1+t12 <= n) };
+s10:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8tau && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t7 = 0 && t9 = 0 && t1 = 0 && 1+t11 = 0 && 1+t3 = 0 && 1+t5 = 0 && t6+1, t10-254 <= t4 <= t10 <= t2-4 && t8-56 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 1 <= t6) };
+s11:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8beta && 2gamma = t10 && t6 = 1+256delta && t2 = 2+64tau && t4 = 2+256alpha && n = t12 && over1 = 1 && t7 = 0 && t9 = 0 && t13 = 0 && t15 = 0 && t1 = 0 && t11 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t2-4, t4+254 && t12-63 <= t2 <= t8 <= t12 <= t8+7 && 0 <= over2 <= 1 && 0 <= over3 <= 1) };
+s12:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8beta && 2gamma = t10 && t6 = 1+256delta && t2 = 2+64tau && t4 = 2+256alpha && n = t12 && over1 = 1 && t7 = 0 && t9 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t11 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t8-56 <= t2 <= t8 <= t12 <= t8+7 && 0 <= over2 <= 1 && 0 <= over3 <= 1) };
+s13:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8 = 2+8tau && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t1 = 0 && t15 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 <= t2+62 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && over1+t12 <= n) };
+s14:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta : t2 = 2+64beta && t4 = 2+256alpha && t1 = 0 && 1+t3 = 0 && t5 = 0 && t7 = 0 && t9 = 0 && 2, t8-255 <= t4 <= t6 < t8 <= t2-2 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2 <= n) };
+s15:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma : t2 = 1+t6+256gamma && t6 = 1+64alpha && t4 = 1+256beta && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 0 && t9 = 0 && t11 = 0 && 1, t8-255 <= t4 <= t8 <= t2-2 && t2-1, t10-255 <= t6 <= t10 <= n && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2 <= n) };
+s16:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && t5 = 0 && t7 = 1 && t11 = 0 && t13 = 0 && t1 = 0 && 1+t9 = 0 && t3 = 0 && t12+2, t10-63 <= t2 <= t8 <= t10 <= t8+7, n && 1, t12-255 <= t4 <= t12 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2-1 <= t6 <= n) };
+s17:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && t5 = 0 && t7 = 1 && t1 = 0 && t9 = 0 && t3 = 0 && t8-56, t4+65 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2-1 <= t6 <= n && 1 <= t4) };
+s18:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && t2 = 1+t6+256gamma && t6 = 1+64delta && t4 = 1+256alpha && n = t10 && over2 = 1 && t5 = 0 && t7 = 1 && t11 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t9 = 3 && t3 = 0 && t14+2, t12-63 <= t2 <= t8 <= t12 <= t8+7, t10 && 1, t14-255 <= t4 <= t14 && t10-255 <= t6 <= t10 && 0 <= over1 <= 1 && 0 <= over3 <= 1) };
+s19:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+s20:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 3 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && 1, t14-255 <= t4 <= t14 <= t2-2 && t2, t12-6 <= t8 <= t12 && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && t8 <= t2+56 && over2+t10 <= n && over3+t12 <= n) };
+s21:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8tau && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && 2delta = t10+t6 && 1+t11 = 0 && t7 = 1 && t9 = 2 && t1 = 0 && t3 = 0 && t5 = 0 && t8-56, t4+65 <= t2 <= t8 <= n && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && 1 <= t4 && over2+t10 <= n) };
+s22:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && 2delta = 1+t10 && t4 = 1+256alpha && t2 = 1+t6 && n = t12 && t6 = 1+64gamma && over3 = 1 && t7 = 1 && t9 = 2 && t13 = 0 && t15 = 1 && t1 = 0 && t11 = 3 && t3 = 0 && t5 = 0 && 1, t14-255 <= t4 <= t14 < t6 < t8 <= t12 <= t8+7, t6+64 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && t6 <= t10 && over2+t10 <= t12) };
+s23:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && 2delta = 1+t10 && t4 = 1+256alpha && t2 = 1+t6 && t12 = n && t6 = 1+64gamma && over3 = 1 && t7 = 1 && t9 = 2 && t13 = 0 && t15 = 3 && t1 = 0 && t11 = 3 && t3 = 0 && t5 = 0 && 1, t14-255 <= t4 <= t14 < t6 < t8 <= n <= t8+7 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && t8-57 <= t6 <= t10 && over2+t10 <= n) };
+s24:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+s25:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 5 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && t12-62, t14+2 <= t2 <= t8 <= t12 <= t8+6 && t2-1, t10-254 <= t6 <= t10 && 1, t14-255 <= t4 <= t14 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && over2+t10 <= n && over3+t12 <= n) };
+s26:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+s27:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 7 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && 1, t14-255 <= t4 <= t14 <= t2-2 && t12-6, t2 <= t8 <= t12 && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && t8 <= t2+56 && over2+t10 <= n && over3+t12 <= n) };
+
+codegen 1 s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22,s23,s24,s25,s26,s27;
+
diff --git a/omega/examples/experiments/lu/lu.out b/omega/examples/experiments/lu/lu.out
new file mode 100644
index 0000000..443a4db
--- /dev/null
+++ b/omega/examples/experiments/lu/lu.out
@@ -0,0 +1,141 @@
+>>> symbolic n, over1, over2, over3;
+>>>
+>>> s0:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+>>> s1:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 1 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && t12-62, t14+2 <= t2 <= t8 <= t12 <= t8+6 && t2-1, t10-254 <= t6 <= t10 && 1, t14-255 <= t4 <= t14 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && over3+t12 <= n && over2+t10 <= n) };
+>>> s2:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha : t2 = 2+64alpha && 1+t4 = t6 && t7 = 0 && t9 = 0 && t1 = 0 && t3 = 2 && t5 = 0 && 2, t6-63 <= t2 <= t6 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+>>> s3:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha : t2 = 2+64alpha && t5 = 1 && t7 = 0 && t9 = 0 && t1 = 0 && t3 = 2 && t2-1 <= t4 < t6 <= t2+63, n && t4 < t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 2 <= t2) };
+>>> s4:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2tau = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8+8sigma = 2 && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t15 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 <= t2+62 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && over1+t12 <= n) };
+>>> s5:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta : t2 = 2+64beta && t4 = 2+256alpha && 1+t3 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t1 = 0 && t5 = 1 && 2, t6-255 <= t4 <= t10 < t6 <= t2-2 && t8-63 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+>>> s6:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma : t4 = 2+256gamma && t6 = 1+256alpha && t2 = 2+64beta && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && 1+t7 = 0 && t9 = 0 && t11 = 0 && 1, t8-255 <= t6 <= t8 < t4 <= t10 <= t2-2, t4+255 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2 <= n) };
+>>> s7:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t4 = 2+256alpha && t6 = 1+256beta && t2 = 2+64gamma && 1+t5 = 0 && t7 = 0 && t11 = 0 && t13 = 0 && t1 = 0 && 2+t9 = 0 && 1+t3 = 0 && t4+64, t10-63 <= t2 <= t8 <= t10 <= t8+7, n && 1, t12-255 <= t6 <= t12 <= t4-1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1) };
+>>> s8:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t4 = 2+256alpha && t6 = 1+256beta && 2+t10 = t2 && t2 = 2+64gamma && t7 = 0 && t11 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t9 = 1 && 1+t3 = 0 && 1+t5 = 0 && t4+64, t12-63 <= t2 <= t8 <= t12 <= t8+7, n && 1, t14-255 <= t6 <= t14 <= t4-1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2 <= t4+256) };
+>>> s9:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8 = 2+8tau && t1 = 0 && 1+t3 = 0 && 1+t5 = 0 && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t15 = 1 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t8 <= t2+56 && over1+t12 <= n) };
+>>> s10:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8tau && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t7 = 0 && t9 = 0 && t1 = 0 && 1+t11 = 0 && 1+t3 = 0 && 1+t5 = 0 && t6+1, t10-254 <= t4 <= t10 <= t2-4 && t8-56 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && 1 <= t6) };
+>>> s11:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8beta && 2gamma = t10 && t6 = 1+256delta && t2 = 2+64tau && t4 = 2+256alpha && n = t12 && over1 = 1 && t7 = 0 && t9 = 0 && t13 = 0 && t15 = 0 && t1 = 0 && t11 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t2-4, t4+254 && t12-63 <= t2 <= t8 <= t12 <= t8+7 && 0 <= over2 <= 1 && 0 <= over3 <= 1) };
+>>> s12:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8beta && 2gamma = t10 && t6 = 1+256delta && t2 = 2+64tau && t4 = 2+256alpha && n = t12 && over1 = 1 && t7 = 0 && t9 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t11 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t8-56 <= t2 <= t8 <= t12 <= t8+7 && 0 <= over2 <= 1 && 0 <= over3 <= 1) };
+>>> s13:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && 2alpha = t10 && t6 = 1+256beta && t2 = 2+64gamma && t4 = 2+256delta && t8 = 2+8tau && t7 = 0 && t9 = 0 && t11 = 1 && t13 = 0 && t1 = 0 && t15 = 2 && 1+t3 = 0 && 1+t5 = 0 && 1, t14-255 <= t6 <= t14 < t4 <= t10 <= t4+254, t2-4 && t2, t12-6 <= t8 <= t12 <= t2+62 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && over1+t12 <= n) };
+>>> s14:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta : t2 = 2+64beta && t4 = 2+256alpha && t1 = 0 && 1+t3 = 0 && t5 = 0 && t7 = 0 && t9 = 0 && 2, t8-255 <= t4 <= t6 < t8 <= t2-2 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2 <= n) };
+>>> s15:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma : t2 = 1+t6+256gamma && t6 = 1+64alpha && t4 = 1+256beta && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 0 && t9 = 0 && t11 = 0 && 1, t8-255 <= t4 <= t8 <= t2-2 && t2-1, t10-255 <= t6 <= t10 <= n && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2 <= n) };
+>>> s16:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && t5 = 0 && t7 = 1 && t11 = 0 && t13 = 0 && t1 = 0 && 1+t9 = 0 && t3 = 0 && t12+2, t10-63 <= t2 <= t8 <= t10 <= t8+7, n && 1, t12-255 <= t4 <= t12 && 0 <= over1 <= 1 && 0 <= over3 <= 1 && 0 <= over2 <= 1 && t2-1 <= t6 <= n) };
+>>> s17:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9] : exists ( alpha,beta,gamma,delta : t8 = 2+8delta && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && t5 = 0 && t7 = 1 && t1 = 0 && t9 = 0 && t3 = 0 && t8-56, t4+65 <= t2 <= t8 <= n && 0 <= over3 <= 1 && 0 <= over2 <= 1 && 0 <= over1 <= 1 && t2-1 <= t6 <= n && 1 <= t4) };
+>>> s18:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && t2 = 1+t6+256gamma && t6 = 1+64delta && t4 = 1+256alpha && n = t10 && over2 = 1 && t5 = 0 && t7 = 1 && t11 = 0 && t13 = 0 && t15 = 1 && t1 = 0 && t9 = 3 && t3 = 0 && t14+2, t12-63 <= t2 <= t8 <= t12 <= t8+7, t10 && 1, t14-255 <= t4 <= t14 && t10-255 <= t6 <= t10 && 0 <= over1 <= 1 && 0 <= over3 <= 1) };
+>>> s19:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+>>> s20:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 3 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && 1, t14-255 <= t4 <= t14 <= t2-2 && t2, t12-6 <= t8 <= t12 && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && t8 <= t2+56 && over2+t10 <= n && over3+t12 <= n) };
+>>> s21:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11] : exists ( alpha,beta,gamma,delta,tau : t8 = 2+8tau && t2 = 1+t6+256alpha && t6 = 1+64beta && t4 = 1+256gamma && 2delta = t10+t6 && 1+t11 = 0 && t7 = 1 && t9 = 2 && t1 = 0 && t3 = 0 && t5 = 0 && t8-56, t4+65 <= t2 <= t8 <= n && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && 1 <= t4 && over2+t10 <= n) };
+>>> s22:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && 2delta = 1+t10 && t4 = 1+256alpha && t2 = 1+t6 && n = t12 && t6 = 1+64gamma && over3 = 1 && t7 = 1 && t9 = 2 && t13 = 0 && t15 = 1 && t1 = 0 && t11 = 3 && t3 = 0 && t5 = 0 && 1, t14-255 <= t4 <= t14 < t6 < t8 <= t12 <= t8+7, t6+64 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && t6 <= t10 && over2+t10 <= t12) };
+>>> s23:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta : t8 = 2+8beta && 2delta = 1+t10 && t4 = 1+256alpha && t2 = 1+t6 && t12 = n && t6 = 1+64gamma && over3 = 1 && t7 = 1 && t9 = 2 && t13 = 0 && t15 = 3 && t1 = 0 && t11 = 3 && t3 = 0 && t5 = 0 && 1, t14-255 <= t4 <= t14 < t6 < t8 <= n <= t8+7 && 0 <= over1 <= 1 && 0 <= over2 <= 1 && t8-57 <= t6 <= t10 && over2+t10 <= n) };
+>>> s24:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+>>> s25:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 5 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && t12-62, t14+2 <= t2 <= t8 <= t12 <= t8+6 && t2-1, t10-254 <= t6 <= t10 && 1, t14-255 <= t4 <= t14 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && over2+t10 <= n && over3+t12 <= n) };
+>>> s26:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : 1=2 };
+>>> s27:= { [t1,t2,t3,t4,t5,t6,t7,t8,t9,t10,t11,t12,t13,t14,t15] : exists ( alpha,beta,gamma,delta,tau,sigma : 2sigma = t12 && t2 = 1+t6+256alpha && 2beta = 1+t10 && t4 = 1+256gamma && t6 = 1+64delta && t8 = 2+8tau && t15 = 7 && t9 = 2 && t11 = 1 && t13 = 0 && t1 = 0 && t3 = 0 && t5 = 0 && t7 = 1 && 1, t14-255 <= t4 <= t14 <= t2-2 && t12-6, t2 <= t8 <= t12 && t2-1, t10-254 <= t6 <= t10 && 0 <= over2 <= 1 && 0 <= over3 <= 1 && 0 <= over1 <= 1 && t8 <= t2+56 && over2+t10 <= n && over3+t12 <= n) };
+>>>
+>>> codegen 1 s0,s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12,s13,s14,s15,s16,s17,s18,s19,s20,s21,s22,s23,s24,s25,s26,s27;
+if (over1 >= 0 && over1 <= 1 && over3 <= 1 && over3 >= 0 && over2 >= 0 && over2 <= 1) {
+ for(t2 = 2; t2 <= n; t2 += 64) {
+ for(t4 = 2; t4 <= t2-64; t4 += 256) {
+ for(t6 = 1; t6 <= t4-1; t6 += 256) {
+ for(t8 = t6; t8 <= min(t6+255,t4-1); t8++) {
+ for(t10 = t4; t10 <= min(t2-2,t4+255); t10++) {
+ s6(0,t2,-1,t4,-1,t6,-1,t8,0,t10,0);
+ }
+ }
+ for(t8 = t2; t8 <= min(n,t2+56); t8 += 8) {
+ for(t10 = t8; t10 <= min(t8+7,n); t10++) {
+ for(t12 = t6; t12 <= min(t6+255,t4-1); t12++) {
+ s7(0,t2,-1,t4,-1,t6,0,t8,-2,t10,0,t12,0);
+ }
+ }
+ for(t10 = t4; t10 <= min(t2-4,t4+254); t10 += 2) {
+ s10(0,t2,-1,t4,-1,t6,0,t8,0,t10,-1);
+ for(t12 = t8; t12 <= min(-over1+n,t8+6); t12 += 2) {
+ for(t14 = t6; t14 <= min(t4-1,t6+255); t14++) {
+ s4(0,t2,-1,t4,-1,t6,0,t8,0,t10,1,t12,0,t14,0);
+ s9(0,t2,-1,t4,-1,t6,0,t8,0,t10,1,t12,0,t14,1);
+ s13(0,t2,-1,t4,-1,t6,0,t8,0,t10,1,t12,0,t14,2);
+ }
+ }
+ if (t8 >= n-7 && over1 >= 1) {
+ for(t14 = t6; t14 <= min(t4-1,t6+255); t14++) {
+ s11(0,t2,-1,t4,-1,t6,0,t8,0,t10,2,n,0,t14,0);
+ s12(0,t2,-1,t4,-1,t6,0,t8,0,t10,2,n,0,t14,1);
+ }
+ }
+ }
+ if (t4 >= t2-256) {
+ for(t12 = t8; t12 <= min(t8+7,n); t12++) {
+ for(t14 = t6; t14 <= min(t6+255,t4-1); t14++) {
+ s8(0,t2,-1,t4,-1,t6,0,t8,1,t2-2,0,t12,0,t14,1);
+ }
+ }
+ }
+ }
+ }
+ for(t6 = t4; t6 <= min(t4+254,t2-3); t6++) {
+ for(t8 = t6+1; t8 <= min(t2-2,t4+255); t8++) {
+ s14(0,t2,-1,t4,0,t6,0,t8,0);
+ }
+ }
+ for(t6 = t4+1; t6 <= min(t2-2,t4+255); t6++) {
+ for(t8 = t2; t8 <= min(n,t2+63); t8++) {
+ for(t10 = t4; t10 <= t6-1; t10++) {
+ s5(0,t2,-1,t4,1,t6,0,t8,0,t10,1);
+ }
+ }
+ }
+ }
+ for(t4 = 1; t4 <= t2-65; t4 += 256) {
+ for(t6 = t2-1; t6 <= n; t6 += 256) {
+ for(t8 = t4; t8 <= min(t4+255,t2-2); t8++) {
+ for(t10 = t6; t10 <= min(n,t6+255); t10++) {
+ s15(0,t2,0,t4,0,t6,0,t8,0,t10,0);
+ }
+ }
+ for(t8 = t2; t8 <= min(t2+56,n); t8 += 8) {
+ for(t10 = t8; t10 <= min(n,t8+7); t10++) {
+ for(t12 = t4; t12 <= min(t4+255,t2-2); t12++) {
+ s16(0,t2,0,t4,0,t6,1,t8,-1,t10,0,t12,0);
+ }
+ }
+ s17(0,t2,0,t4,0,t6,1,t8,0);
+ for(t10 = t6; t10 <= min(n-over2,t6+254); t10 += 2) {
+ s21(0,t2,0,t4,0,t6,1,t8,2,t10,-1);
+ for(t12 = t8; t12 <= min(t8+6,n-over3); t12 += 2) {
+ for(t14 = t4; t14 <= min(t2-2,t4+255); t14++) {
+ s1(0,t2,0,t4,0,t6,1,t8,2,t10,1,t12,0,t14,1);
+ s20(0,t2,0,t4,0,t6,1,t8,2,t10,1,t12,0,t14,3);
+ s25(0,t2,0,t4,0,t6,1,t8,2,t10,1,t12,0,t14,5);
+ s27(0,t2,0,t4,0,t6,1,t8,2,t10,1,t12,0,t14,7);
+ }
+ }
+ if (over3 >= 1 && t8 >= n-7) {
+ for(t14 = t4; t14 <= min(t6-1,t4+255); t14++) {
+ s22(0,t2,0,t4,0,t6,1,t8,2,t10,3,n,0,t14,1);
+ s23(0,t2,0,t4,0,t6,1,t8,2,t10,3,n,0,t14,3);
+ }
+ }
+ }
+ if (t6 >= n-255 && over2 >= 1) {
+ for(t12 = t8; t12 <= min(t8+7,n); t12++) {
+ for(t14 = t4; t14 <= min(t2-2,t4+255); t14++) {
+ s18(0,t2,0,t4,0,t6,1,t8,3,n,0,t12,0,t14,1);
+ }
+ }
+ }
+ }
+ }
+ }
+ for(t4 = t2-1; t4 <= min(t2+62,n-1); t4++) {
+ for(t8 = t4+1; t8 <= n; t8++) {
+ s2(0,t2,2,t4,0,t4+1,0,t8,0);
+ }
+ for(t6 = t4+1; t6 <= min(n,t2+63); t6++) {
+ for(t8 = t4+1; t8 <= n; t8++) {
+ s3(0,t2,2,t4,1,t6,0,t8,0);
+ }
+ }
+ }
+ }
+}
+
+>>>
+>>>
diff --git a/omega/examples/experiments/qr/codegen.input b/omega/examples/experiments/qr/codegen.input
new file mode 100755
index 0000000..01f8496
--- /dev/null
+++ b/omega/examples/experiments/qr/codegen.input
@@ -0,0 +1,17 @@
+symbolic M, N;
+
+s1:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : 1+In_3 = 0 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 0 <= In_6 < N };
+s2:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && 1+In_2 = In_4 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 1 <= In_4 <= In_6+1, N && In_6 < M };
+s3:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 1 && 0 <= In_6 < N };
+s4:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && 1+In_2 = In_4 && In_7 = 0 && In_1 = 0 && In_5 = 2 && 1 <= In_4 <= In_6+1, N && In_6 < M };
+s5:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 1 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 0 <= In_6 < N };
+s6:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 0 && In_7 = 0 && In_6 = In_2 && 0 <= In_2 <= In_4-2 && In_4 < N };
+s7:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 3 && In_7 = 0 && 0 <= In_2 <= In_6 < M && In_2+2 <= In_4 < N };
+s8:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 2 && In_7 = 0 && In_6 = M && In_2+2 <= In_4 <= N && 0 <= In_2 };
+s9:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 3 && In_7 = 1 && 0 <= In_2 <= In_6 < M && In_2+2 <= In_4 <= N };
+s10:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 2 && In_4 = N && In_6 = M && In_5 = 0 && In_7 = 0 && In_1 = 0 && 0 <= In_2 < N };
+s11:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_5 = 0 && In_3 = 3 && In_7 = 0 && In_1 = 0 && In_6 = In_2 && In_4 = 1+In_2 && 0 <= In_2 <= N-2 };
+s12:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_5 = 3 && In_3 = 3 && In_7 = 0 && In_1 = 0 && In_4 = 1+In_2 && 0 <= In_2 <= In_6 < M && In_2 <= N-2 };
+
+
+codegen s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12;
diff --git a/omega/examples/experiments/qr/qr.out b/omega/examples/experiments/qr/qr.out
new file mode 100644
index 0000000..e09cc75
--- /dev/null
+++ b/omega/examples/experiments/qr/qr.out
@@ -0,0 +1,54 @@
+>>> symbolic M, N;
+>>>
+>>> s1:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : 1+In_3 = 0 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 0 <= In_6 < N };
+>>> s2:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && 1+In_2 = In_4 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 1 <= In_4 <= In_6+1, N && In_6 < M };
+>>> s3:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 1 && 0 <= In_6 < N };
+>>> s4:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 0 && 1+In_2 = In_4 && In_7 = 0 && In_1 = 0 && In_5 = 2 && 1 <= In_4 <= In_6+1, N && In_6 < M };
+>>> s5:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 1 && In_4 = 1+In_6 && In_2 = In_6 && In_7 = 0 && In_1 = 0 && In_5 = 0 && 0 <= In_6 < N };
+>>> s6:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 0 && In_7 = 0 && In_6 = In_2 && 0 <= In_2 <= In_4-2 && In_4 < N };
+>>> s7:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 3 && In_7 = 0 && 0 <= In_2 <= In_6 < M && In_2+2 <= In_4 < N };
+>>> s8:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 2 && In_7 = 0 && In_6 = M && In_2+2 <= In_4 <= N && 0 <= In_2 };
+>>> s9:= { [In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_1 = 0 && In_3 = 4 && In_5 = 3 && In_7 = 1 && 0 <= In_2 <= In_6 < M && In_2+2 <= In_4 <= N };
+>>> s10:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_3 = 2 && In_4 = N && In_6 = M && In_5 = 0 && In_7 = 0 && In_1 = 0 && 0 <= In_2 < N };
+>>> s11:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_5 = 0 && In_3 = 3 && In_7 = 0 && In_1 = 0 && In_6 = In_2 && In_4 = 1+In_2 && 0 <= In_2 <= N-2 };
+>>> s12:= {[In_1,In_2,In_3,In_4,In_5,In_6,In_7] : In_5 = 3 && In_3 = 3 && In_7 = 0 && In_1 = 0 && In_4 = 1+In_2 && 0 <= In_2 <= In_6 < M && In_2 <= N-2 };
+>>>
+>>>
+>>> codegen s1,s2,s3,s4,s5,s6,s7,s8,s9,s10,s11,s12;
+for(t2 = 0; t2 <= N-1; t2++) {
+ s0(0,t2,-1,t2+1,0,t2,0);
+ for(t6 = t2+1-1; t6 <= M-1; t6++) {
+ s1(0,t2,0,t2+1,0,t6,0);
+ }
+ s2(0,t2,0,t2+1,1,t2,0);
+ for(t6 = t2+1-1; t6 <= M-1; t6++) {
+ s3(0,t2,0,t2+1,2,t6,0);
+ }
+ s4(0,t2,1,t2+1,0,t2,0);
+ s9(0,t2,2,N,0,M,0);
+ if (N >= t2+2) {
+ s10(0,t2,3,t2+1,0,t2+1-1,0);
+ for(t6 = t2; t6 <= M-1; t6++) {
+ s11(0,t2,3,t2+1,3,t6,0);
+ }
+ }
+ for(t4 = t2+2; t4 <= N; t4++) {
+ if (N >= t4+1) {
+ s5(0,t2,4,t4,0,t2,0);
+ }
+ s7(0,t2,4,t4,2,M,0);
+ if (N >= t4+1) {
+ for(t6 = t2; t6 <= M-1; t6++) {
+ s6(0,t2,4,t4,3,t6,0);
+ s8(0,t2,4,t4,3,t6,1);
+ }
+ }
+ else {
+ for(t6 = t2; t6 <= M-1; t6++) {
+ s8(0,t2,4,t4,3,t6,1);
+ }
+ }
+ }
+}
+
+>>>
diff --git a/omega/examples/experiments/swim/swim-codegen.input b/omega/examples/experiments/swim/swim-codegen.input
new file mode 100755
index 0000000..4e558bc
--- /dev/null
+++ b/omega/examples/experiments/swim/swim-codegen.input
@@ -0,0 +1,53 @@
+symbolic N3,M,N;
+
+
+s0:= {[t,i,j] : 0 <= j <= N-1 && 0 <= i <= M-1 && 0 <= t <= N3-1 };
+t0:={[t,i,j] -> [0,t,0,i,0,j,0]};
+s1:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1};
+t1:={[t,j] -> [0,t,1,j,0,0,0]};
+s2:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1};
+t2:={[t,i] -> [0,t,2,i,0,0,0]};
+s3:= {[t] : 0 <= t <= N3-1 };
+t3:={[t] -> [0,t,3,0,0,0,0]};
+s4:= {[t,i,j] : 0 <= j <= N-1 && i=M-1 && 0 <= t <= N3-1 };
+t4:={[t,i,j] -> [0,t,4,i,0,j,0] };
+s5:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1 };
+t5:={[t,j] -> [0,t,8,j,0,0,0]};
+s6:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1 };
+t6:={[t,i] -> [0,t,9,i,0,0,0]};
+s7:= {[t] : 0 <= t <= N3-1 };
+t7:={[t] -> [0,t,10,0,0,0,0]};
+s8:= {[t,i,j] : 0 <= j <= N-1 && M-2 <= i <= M-1 && 0 <= t <= N3-1 };
+t8:= {[t,i,j] -> [0,t,12,i,0,j,0]};
+s9:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1 };
+t9:={[t,j] -> [0,t,15,j,0,0,0]};
+s10:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1 };
+t10:={[t,i] -> [0,t,16,i,3,0,0]};
+s11:= {[t] : 0 <= t <= N3-1 };
+t11:={[t] -> [0,t,17,0,0,0,0]};
+s12:= {[t,i,j] : 0 <= j <= N-1 && 0 <= i <= 1 && 0 <= t <= N3-1 };
+t12:= {[t,i,j] -> [0,t,11,i,0,j,0]};
+s13:= {[t,i,j] : N-2 <= j <= N-1 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+t13:= {[t,i,j] -> [0,t,14,i,0,j,0]};
+s14:= {[t,i,j] : 0 <= j <= 1 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+t14:= {[t,i,j] -> [0,t,13,i,0,j,0]};
+s15:= {[t,i,j] : 2 <= j <= N-3 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+t15:={[t,i,j] -> [0,t,0,i+3,0,j+2,2]};
+
+s16:= {[t,i,j] : 0 <= j <= N-1 && i=0 && 0 <= t <= N3-1 };
+t16:={[t,i,j] -> [0,t,5,i,0,j,0] };
+
+s17:= {[t,i,j] : j =N-1 && 1<= i <=M-2 && 0 <= t <= N3-1 };
+t17:={[t,i,j] -> [0,t,6,i,0,j,0] };
+
+s18:= {[t,i,j] : j =0 && 1<= i <=M-2 && 0 <= t <= N3-1};
+t18:={[t,i,j] -> [0,t,7,i,0,j,0] };
+
+s19:= {[t,i,j] :1 <= j <= N-2 && 1 <= i <= M-2 && 0 <= t <= N3-1 };
+t19:={[t,i,j] -> [0,t,0,i+2,0,j+1,1]};
+
+
+
+codegen 2 t0:s0,t1:s1,t2:s2,t3:s3,t4:s4,t5:s5,t6:s6,t7:s7,t8:s8,t9:s9,t10:s10,t11:s11,t12:s12,t13:s13,t14:s14,t15:s15,t16:s16,t17:s17,t18:s18,t19:s19;
+#codegen 2 s0,t1:s1,t2:s2,t3:s3,t4:s4,t5:s5,t6:s6,t7:s7,t8:s8,t9:s9,t10:s10,t11:s11,t12:s12,t13:s13,t14:s14,t15:s15,t16:s16,t17:s17,t18:s18,t19:s19;
+
diff --git a/omega/examples/experiments/swim/swim.out b/omega/examples/experiments/swim/swim.out
new file mode 100644
index 0000000..6adffdb
--- /dev/null
+++ b/omega/examples/experiments/swim/swim.out
@@ -0,0 +1,176 @@
+>>> symbolic N3,M,N;
+>>>
+>>>
+>>> s0:= {[t,i,j] : 0 <= j <= N-1 && 0 <= i <= M-1 && 0 <= t <= N3-1 };
+>>> t0:={[t,i,j] -> [0,t,0,i,0,j,0]};
+>>> s1:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1};
+>>>
+>>> t1:={[t,j] -> [0,t,1,j,0,0,0]};
+>>> s2:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1};
+>>> t2:={[t,i] -> [0,t,2,i,0,0,0]};
+>>>
+>>> s3:= {[t] : 0 <= t <= N3-1 };
+>>>
+>>> t3:={[t] -> [0,t,3,0,0,0,0]};
+>>>
+>>> s4:= {[t,i,j] : 0 <= j <= N-1 && i=M-1 && 0 <= t <= N3-1 };
+>>> t4:={[t,i,j] -> [0,t,4,i,0,j,0] };
+>>> s5:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1 };
+>>>
+>>> t5:={[t,j] -> [0,t,8,j,0,0,0]};
+>>>
+>>> s6:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1 };
+>>>
+>>> t6:={[t,i] -> [0,t,9,i,0,0,0]};
+>>>
+>>> s7:= {[t] : 0 <= t <= N3-1 };
+>>>
+>>> t7:={[t] -> [0,t,10,0,0,0,0]};
+>>>
+>>> s8:= {[t,i,j] : 0 <= j <= N-1 && M-2 <= i <= M-1 && 0 <= t <= N3-1 };
+>>> t8:= {[t,i,j] -> [0,t,12,i,0,j,0]};
+>>> s9:= {[t,j] : 0 <= j <= N-1 && 0 <= t <= N3-1 };
+>>>
+>>> t9:={[t,j] -> [0,t,15,j,0,0,0]};
+>>> s10:= {[t,i] : 0 <= i <= M-1 && 0 <= t <= N3-1 };
+>>> t10:={[t,i] -> [0,t,16,i,3,0,0]};
+>>>
+>>> s11:= {[t] : 0 <= t <= N3-1 };
+>>>
+>>> t11:={[t] -> [0,t,17,0,0,0,0]};
+>>>
+>>> s12:= {[t,i,j] : 0 <= j <= N-1 && 0 <= i <= 1 && 0 <= t <= N3-1 };
+>>> t12:= {[t,i,j] -> [0,t,11,i,0,j,0]};
+>>> s13:= {[t,i,j] : N-2 <= j <= N-1 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+>>> t13:= {[t,i,j] -> [0,t,14,i,0,j,0]};
+>>> s14:= {[t,i,j] : 0 <= j <= 1 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+>>> t14:= {[t,i,j] -> [0,t,13,i,0,j,0]};
+>>> s15:= {[t,i,j] : 2 <= j <= N-3 && 2 <= i <= M-3 && 0 <= t <= N3-1 };
+>>> t15:={[t,i,j] -> [0,t,0,i+3,0,j+2,2]};
+>>>
+>>> s16:= {[t,i,j] : 0 <= j <= N-1 && i=0 && 0 <= t <= N3-1 };
+>>> t16:={[t,i,j] -> [0,t,5,i,0,j,0] };
+>>>
+>>> s17:= {[t,i,j] : j =N-1 && 1<= i <=M-2 && 0 <= t <= N3-1 };
+>>> t17:={[t,i,j] -> [0,t,6,i,0,j,0] };
+>>>
+>>> s18:= {[t,i,j] : j =0 && 1<= i <=M-2 && 0 <= t <= N3-1};
+>>> t18:={[t,i,j] -> [0,t,7,i,0,j,0] };
+>>>
+>>> s19:= {[t,i,j] :1 <= j <= N-2 && 1 <= i <= M-2 && 0 <= t <= N3-1 };
+>>> t19:={[t,i,j] -> [0,t,0,i+2,0,j+1,1]};
+>>>
+>>>
+>>>
+>>> codegen 2 t0:s0,t1:s1,t2:s2,t3:s3,t4:s4,t5:s5,t6:s6,t7:s7,t8:s8,t9:s9,t10:s10,t11:s11,t12:s12,t13:s13,t14:s14,t15:s15,t16:s16,t17:s17,t18:s18,t19:s19;
+for(t2 = 0; t2 <= N3-1; t2++) {
+ if (N >= 1) {
+ for(t4 = 0; t4 <= min(2,M-1); t4++) {
+ for(t6 = 0; t6 <= N-1; t6++) {
+ s0(t2,t4,t6);
+ }
+ }
+ for(t4 = 3; t4 <= min(M-1,4); t4++) {
+ for(t6 = 0; t6 <= min(1,N-1); t6++) {
+ s0(t2,t4,t6);
+ }
+ for(t6 = 2; t6 <= min(3,N-1); t6++) {
+ s0(t2,t4,t6);
+ s19(t2,t4-2,t6-1);
+ }
+ for(t6 = 4; t6 <= N-1; t6++) {
+ s0(t2,t4,t6);
+ s19(t2,t4-2,t6-1);
+ }
+ }
+ for(t4 = 5; t4 <= M-1; t4++) {
+ for(t6 = 0; t6 <= min(1,N-1); t6++) {
+ s0(t2,t4,t6);
+ }
+ for(t6 = 2; t6 <= min(N-1,3); t6++) {
+ s0(t2,t4,t6);
+ s19(t2,t4-2,t6-1);
+ }
+ for(t6 = 4; t6 <= N-1; t6++) {
+ s0(t2,t4,t6);
+ s19(t2,t4-2,t6-1);
+ s15(t2,t4-3,t6-2);
+ }
+ }
+ }
+ if (M >= 3) {
+ if (M >= 5) {
+ for(t6 = 2; t6 <= min(N-1,3); t6++) {
+ s19(t2,M-2,t6-1);
+ }
+ for(t6 = 4; t6 <= N-1; t6++) {
+ s19(t2,M-2,t6-1);
+ s15(t2,M-3,t6-2);
+ }
+ }
+ else {
+ for(t6 = 2; t6 <= N-1; t6++) {
+ s19(t2,M-2,t6-1);
+ }
+ }
+ }
+ for(t4 = 0; t4 <= N-1; t4++) {
+ s1(t2,t4);
+ }
+ for(t4 = 0; t4 <= M-1; t4++) {
+ s2(t2,t4);
+ }
+ s3(t2);
+ for(t6 = 0; t6 <= N-1; t6++) {
+ s4(t2,M-1,t6);
+ }
+ for(t6 = 0; t6 <= N-1; t6++) {
+ s16(t2,0,t6);
+ }
+ for(t4 = 1; t4 <= M-2; t4++) {
+ s17(t2,t4,N-1);
+ }
+ for(t4 = 1; t4 <= M-2; t4++) {
+ s18(t2,t4,0);
+ }
+ for(t4 = 0; t4 <= N-1; t4++) {
+ s5(t2,t4);
+ }
+ for(t4 = 0; t4 <= M-1; t4++) {
+ s6(t2,t4);
+ }
+ s7(t2);
+ if (N >= 1) {
+ for(t4 = 0; t4 <= 1; t4++) {
+ for(t6 = 0; t6 <= N-1; t6++) {
+ s12(t2,t4,t6);
+ }
+ }
+ for(t4 = M-2; t4 <= M-1; t4++) {
+ for(t6 = 0; t6 <= N-1; t6++) {
+ s8(t2,t4,t6);
+ }
+ }
+ }
+ for(t4 = 2; t4 <= M-3; t4++) {
+ for(t6 = 0; t6 <= 1; t6++) {
+ s14(t2,t4,t6);
+ }
+ }
+ for(t4 = 2; t4 <= M-3; t4++) {
+ for(t6 = N-2; t6 <= N-1; t6++) {
+ s13(t2,t4,t6);
+ }
+ }
+ for(t4 = 0; t4 <= N-1; t4++) {
+ s9(t2,t4);
+ }
+ for(t4 = 0; t4 <= M-1; t4++) {
+ s10(t2,t4);
+ }
+ s11(t2);
+}
+
+>>> #codegen 2 s0,t1:s1,t2:s2,t3:s3,t4:s4,t5:s5,t6:s6,t7:s7,t8:s8,t9:s9,t10:s10,t11:s11,t12:s12,t13:s13,t14:s14,t15:s15,t16:s16,t17:s17,t18:s18,t19:s19;
+>>>
+>>>
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-02-02 07:00:06 +0000