1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
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);
}
}
}
}
}
}
}
>>>
>>>
|
