]> git.lizzy.rs Git - plan9front.git/blob - sys/src/cmd/forp/logic.c
cwfs: fix listen filedescriptor leaks
[plan9front.git] / sys / src / cmd / forp / logic.c
1 #include <u.h>
2 #include <libc.h>
3 #include <mp.h>
4 #include <sat.h>
5 #include "dat.h"
6 #include "fns.h"
7
8 extern int satvar;
9
10 int
11 satand1(SATSolve *sat, int *a, int n)
12 {
13         int i, j, r;
14         int *b;
15
16         if(n < 0)
17                 for(n = 0; a[n] != 0; n++)
18                         ;
19         r = 2;
20         for(i = j = 0; i < n; i++){
21                 if(a[i] == 1 || a[i] == -2)
22                         return 1;
23                 if(a[i] == 2 || a[i] == -1)
24                         j++;
25                 else
26                         r = a[i];
27         }
28         if(j >= n - 1) return r;
29         r = satvar++;
30         b = malloc(sizeof(int) * (n+1));
31         for(i = j = 0; i < n; i++){
32                 if(a[i] == 2 || a[i] == -1)
33                         continue;
34                 b[j++] = -a[i];
35                 sataddv(sat, -r, a[i], 0);
36         }
37         b[j++] = r;
38         satadd1(sat, b, j);
39         return r;
40 }
41
42 int
43 satandv(SATSolve *sat, ...)
44 {
45         int r;
46         va_list va;
47         
48         va_start(va, sat);
49         satvafix(va);
50         r = satand1(sat, (int*)va, -1);
51         va_end(va);
52         return r;
53 }
54
55 int
56 sator1(SATSolve *sat, int *a, int n)
57 {
58         int i, j, r;
59         int *b;
60
61         if(n < 0)
62                 for(n = 0; a[n] != 0; n++)
63                         ;
64         r = 1;
65         for(i = j = 0; i < n; i++){
66                 if(a[i] == 2 || a[i] == -1)
67                         return 2;
68                 if(a[i] == 1 || a[i] == -2)
69                         j++;
70                 else
71                         r = a[i];
72         }
73         if(j >= n-1) return r;
74         r = satvar++;
75         b = malloc(sizeof(int) * (n+1));
76         for(i = j = 0; i < n; i++){
77                 if(a[i] == 1 || a[i] == -2)
78                         continue;
79                 b[j++] = a[i];
80                 sataddv(sat, r, -a[i], 0);
81         }
82         b[j++] = -r;
83         satadd1(sat, b, j);
84         return r;
85 }
86
87 int
88 satorv(SATSolve *sat, ...)
89 {
90         va_list va;
91         int r;
92         
93         va_start(va, sat);
94         satvafix(va);
95         r = sator1(sat, (int*)va, -1);
96         va_end(va);
97         return r;
98 }
99
100 typedef struct { u8int x, m; } Pi;
101 static Pi *π;
102 static int nπ;
103 static u64int *πm;
104
105 static void
106 pimp(u64int op, int n)
107 {
108         int i, j, k;
109         u8int δ;
110
111         nπ = 0;
112         for(i = 0; i < 1<<n; i++)
113                 if((op >> i & 1) != 0){
114                         π = realloc(π, sizeof(Pi) * (nπ + 1));
115                         π[nπ++] = (Pi){i, 0};
116                 }
117         for(i = 0; i < nπ; i++){
118                 for(j = 0; j < i; j++){
119                         δ = π[i].x ^ π[j].x;
120                         if(δ == 0 || (δ & δ - 1) != 0 || π[i].m != π[j].m) continue;
121                         if(((π[i].m | π[j].m) & δ) != 0) continue;
122                         if(π[nπ-1].x == (π[i].x & π[j].x) && π[nπ-1].m == (π[i].m | δ)) continue;
123                         π = realloc(π, sizeof(Pi) * (nπ + 1));
124                         π[nπ++] = (Pi){π[i].x & π[j].x, π[i].m | δ};
125                 }
126         }
127         for(i = k = 0; i < nπ; i++){
128                 for(j = i+1; j < nπ; j++)
129                         if((π[i].m & ~π[j].m) == 0 && (π[i].x & ~π[j].m) == π[j].x)
130                                 break;
131                 if(j == nπ)
132                         π[k++] = π[i];
133         }
134         nπ = k;
135         assert(nπ <= 1<<n);
136 }
137
138 static void
139 pimpmask(void)
140 {
141         int i, j;
142         u64int m;
143
144         πm = realloc(πm, sizeof(u64int) * nπ);
145         for(i = 0; i < nπ; i++){
146                 m = 0;
147                 for(j = π[i].m; ; j = j - 1 & π[i].m){
148                         m |= 1ULL<<(π[i].x | j);
149                         if(j == 0) break;
150                 }
151                 πm[i] = m;
152         }
153 }
154
155 static int
156 popcnt(u64int m)
157 {
158         m = (m & 0x5555555555555555ULL) + (m >> 1 & 0x5555555555555555ULL);
159         m = (m & 0x3333333333333333ULL) + (m >> 2 & 0x3333333333333333ULL);
160         m = (m & 0x0F0F0F0F0F0F0F0FULL) + (m >> 4 & 0x0F0F0F0F0F0F0F0FULL);
161         m = (m & 0x00FF00FF00FF00FFULL) + (m >> 8 & 0x00FF00FF00FF00FFULL);
162         m = (m & 0x0000FFFF0000FFFFULL) + (m >> 16 & 0x0000FFFF0000FFFFULL);
163         m = (u32int)m + (u32int)(m >> 32);
164         return m;
165 }
166
167 static u64int
168 pimpcover(u64int op, int)
169 {
170         int i, j, maxi, p, maxp;
171         u64int cov, yes, m;
172         
173         yes = 0;
174         cov = op;
175         for(i = 0; i < nπ; i++){
176                 if((yes & 1<<i) != 0) continue;
177                 m = πm[i];
178                 for(j = 0; j < nπ; j++){
179                         if(j == i) continue;
180                         m &= ~πm[j];
181                         if(m == 0) break;
182                 }
183                 if(j == nπ){
184                         yes |= 1<<i;
185                         cov &= ~πm[i];
186                 }
187         }
188         while(cov != 0){
189                 j = popcnt(~cov & cov - 1);
190                 maxi = -1;
191                 maxp = 0;
192                 for(i = 0; i < nπ; i++){
193                         if((πm[i] & 1<<j) == 0) continue;
194                         if((p = popcnt(πm[i] & cov)) > maxp)
195                                 maxi = i, maxp = p;
196                 }
197                 assert(maxi >= 0);
198                 yes |= 1<<maxi;
199                 cov &= ~πm[maxi];
200         }
201         return yes;
202 }
203
204 static void
205 pimpsat(SATSolve *sat, u64int yes, int *a, int n, int r)
206 {
207         int i, j, k;
208         int *cl;
209
210         cl = emalloc(sizeof(int) * (n + 1));
211         while(yes != 0){
212                 i = popcnt(~yes & yes - 1);
213                 yes &= yes - 1;
214                 k = 0;
215                 cl[k++] = r;
216                 for(j = 0; j < n; j++)
217                         if((π[i].m & 1<<j) == 0)
218                                 cl[k++] = (π[i].x >> j & 1) != 0 ? -a[j] : a[j];
219 //              for(i = 0; i < k; i++) print("%d ", cl[i]); print("\n");
220                 satadd1(sat, cl, k);
221         }
222         free(cl);
223 }
224
225 int
226 satlogic1(SATSolve *sat, u64int op, int *a, int n)
227 {
228         int i, j, o, r;
229         int s;
230
231         if(n < 0)
232                 for(n = 0; a[n] != 0; n++)
233                         ;
234         assert(op >> (1<<n) == 0);
235         s = 0;
236         j = -1;
237         for(i = n; --i >= 0; ){
238                 if((uint)(a[i] + 2) > 4){
239                         if(j >= 0) break;
240                         j = i;
241                 }
242                 s = s << 1 | a[i] == 2 | a[i] == -1;
243         }
244         if(i < 0){
245                 if(j < 0) return 1 + (op >> s & 1);
246                 o = op >> s & 1 | op >> s + (1<<j) - 1 & 2;
247                 switch(o){
248                 case 0: return 1;
249                 case 1: return -a[j];
250                 case 2: return a[j];
251                 case 3: return 2;
252                 }
253         }
254         r = satvar++;
255         pimp(op, n);
256         pimpmask();
257         pimpsat(sat, pimpcover(op, n), a, n, r);
258         op ^= (u64int)-1 >> 64-(1<<n);
259         pimp(op, n);
260         pimpmask();
261         pimpsat(sat, pimpcover(op, n), a, n, -r);
262         return r;
263 }
264
265 int
266 satlogicv(SATSolve *sat, u64int op, ...)
267 {
268         va_list va;
269         int r;
270         
271         va_start(va, op);
272         satvafix(va);
273         r = satlogic1(sat, op, (int*)va, -1);
274         va_end(va);
275         return r;
276 }