summaryrefslogtreecommitdiff
path: root/omega/examples/experiments/lu
diff options
context:
space:
mode:
Diffstat (limited to 'omega/examples/experiments/lu')
-rwxr-xr-xomega/examples/experiments/lu/codegen.input33
-rw-r--r--omega/examples/experiments/lu/lu.out141
2 files changed, 0 insertions, 174 deletions
diff --git a/omega/examples/experiments/lu/codegen.input b/omega/examples/experiments/lu/codegen.input
deleted file mode 100755
index 0505f2d..0000000
--- a/omega/examples/experiments/lu/codegen.input
+++ /dev/null
@@ -1,33 +0,0 @@
-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
deleted file mode 100644
index 443a4db..0000000
--- a/omega/examples/experiments/lu/lu.out
+++ /dev/null
@@ -1,141 +0,0 @@
->>> 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);
- }
- }
- }
- }
-}
-
->>>
->>>
generated by cgit v1.2.3-70-g09d2 (git 2.48.1) at 2025-02-02 16:54:22 +0000