11 satand1(SATSolve *sat, int *a, int n)
17 for(n = 0; a[n] != 0; n++)
20 for(i = j = 0; i < n; i++){
21 if(a[i] == 1 || a[i] == -2)
23 if(a[i] == 2 || a[i] == -1)
28 if(j >= n - 1) return r;
30 b = malloc(sizeof(int) * (n+1));
31 for(i = j = 0; i < n; i++){
32 if(a[i] == 2 || a[i] == -1)
35 sataddv(sat, -r, a[i], 0);
43 satandv(SATSolve *sat, ...)
50 r = satand1(sat, (int*)va, -1);
56 sator1(SATSolve *sat, int *a, int n)
62 for(n = 0; a[n] != 0; n++)
65 for(i = j = 0; i < n; i++){
66 if(a[i] == 2 || a[i] == -1)
68 if(a[i] == 1 || a[i] == -2)
73 if(j >= n-1) return r;
75 b = malloc(sizeof(int) * (n+1));
76 for(i = j = 0; i < n; i++){
77 if(a[i] == 1 || a[i] == -2)
80 sataddv(sat, r, -a[i], 0);
88 satorv(SATSolve *sat, ...)
95 r = sator1(sat, (int*)va, -1);
100 typedef struct { u8int x, m; } Pi;
106 pimp(u64int op, int n)
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};
117 for(i = 0; i < nπ; i++){
118 for(j = 0; j < i; j++){
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 | δ};
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)
144 πm = realloc(πm, sizeof(u64int) * nπ);
145 for(i = 0; i < nπ; i++){
147 for(j = π[i].m; ; j = j - 1 & π[i].m){
148 m |= 1ULL<<(π[i].x | j);
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);
168 pimpcover(u64int op, int)
170 int i, j, maxi, p, maxp;
175 for(i = 0; i < nπ; i++){
176 if((yes & 1<<i) != 0) continue;
178 for(j = 0; j < nπ; j++){
189 j = popcnt(~cov & cov - 1);
192 for(i = 0; i < nπ; i++){
193 if((πm[i] & 1<<j) == 0) continue;
194 if((p = popcnt(πm[i] & cov)) > maxp)
205 pimpsat(SATSolve *sat, u64int yes, int *a, int n, int r)
210 cl = emalloc(sizeof(int) * (n + 1));
212 i = popcnt(~yes & yes - 1);
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");
226 satlogic1(SATSolve *sat, u64int op, int *a, int n)
232 for(n = 0; a[n] != 0; n++)
234 assert(op >> (1<<n) == 0);
237 for(i = n; --i >= 0; ){
238 if((uint)(a[i] + 2) > 4){
242 s = s << 1 | a[i] == 2 | a[i] == -1;
245 if(j < 0) return 1 + (op >> s & 1);
246 o = op >> s & 1 | op >> s + (1<<j) - 1 & 2;
249 case 1: return -a[j];
257 pimpsat(sat, pimpcover(op, n), a, n, r);
258 op ^= (u64int)-1 >> 64-(1<<n);
261 pimpsat(sat, pimpcover(op, n), a, n, -r);
266 satlogicv(SATSolve *sat, u64int op, ...)
273 r = satlogic1(sat, op, (int*)va, -1);