7 newblock(SATSolve *s, int learned)
11 b = calloc(1, SATBLOCKSZ);
13 saterror(s, "malloc: %r");
14 b->prev = s->bl[learned].prev;
15 b->next = &s->bl[learned];
18 b->end = (void*) b->data;
23 satnewclause(SATSolve *s, int n, int learned)
29 sz = sizeof(SATClause) + (n - 1) * sizeof(int);
30 assert(sz <= SATBLOCKSZ);
36 f = (uchar*)b + SATBLOCKSZ - (uchar*)b->end;
39 if(b == &s->bl[learned])
40 b = newblock(s, learned);
43 memset(c, 0, sizeof(SATClause));
44 b->end = (void *)((uintptr)b->end + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN);
47 if(s->lastp[1] == &s->learncl)
52 *s->lastp[learned] = c;
53 s->lastp[learned] = &c->next;
58 /* this is currently only used to subsume clauses, i.e. n is guaranteed to be less than the last n */
60 satreplclause(SATSolve *s, int n)
66 assert(s->lastbl != nil && s->lastbl->last != nil);
69 f = (uchar*)b + SATBLOCKSZ - (uchar*)c;
70 sz = sizeof(SATClause) + (n - 1) * sizeof(int);
72 b->end = (void *)((uintptr)c + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN);
73 for(i = 0; i < 2; i++){
75 for(wp = &s->lit[l].watch; *wp != nil && *wp != c; wp = &(*wp)->watch[(*wp)->l[1] == l])
80 memset(c, 0, sizeof(SATClause));
85 litconv(SATSolve *s, int l)
93 if(v >= s->nvaralloc){
94 n = -(-(v+1) & -SATVARALLOC);
95 s->var = vp = satrealloc(s, s->var, n * sizeof(SATVar));
96 s->lit = lp = satrealloc(s, s->lit, 2 * n * sizeof(SATLit));
97 memset(vp += s->nvaralloc, 0, (n - s->nvaralloc) * sizeof(SATVar));
98 memset(lp += 2*s->nvaralloc, 0, 2 * (n - s->nvaralloc) * sizeof(SATLit));
99 for(; vp < s->var + n; vp++){
101 vp->flags = VARPHASE;
103 for(; lp < s->lit + 2 * n; lp++)
109 return v << 1 | m & 1;
113 addbimp(SATSolve *s, int l0, int l1)
117 lp = &s->lit[NOT(l0)];
118 lp->bimp = satrealloc(s, lp->bimp, (lp->nbimp + 1) * sizeof(int));
119 lp->bimp[lp->nbimp++] = l1;
123 satadd1special(SATSolve *s, int *a, int n)
133 for(i = 1; i < n; i++)
141 switch(s->lit[l0].val){
146 s->trail = satrealloc(s, s->trail, sizeof(int) * s->nvar);
147 memmove(&s->trail[1], s->trail, sizeof(int) * s->ntrail);
150 s->var[VAR(l0)].flags |= VARUSER;
151 s->var[VAR(l0)].lvl = 0;
153 s->lit[NOT(l0)].val = 0;
157 if(l0 + l1 == 0) return s;
166 satadd1(SATSolve *s, int *a, int n)
175 saterror(nil, "satnew: %r");
178 for(n = 0; a[n] != 0; n++)
180 for(i = 0; i < n; i++)
182 saterror(s, "satadd1(%p, %p, %d): a[%d]==0, callerpc=%p", s, a, n, i, getcallerpc(&s));
185 return satadd1special(s, a, n);
186 /* use stamps to detect repeated literals and tautological clauses */
187 if(s->stamp >= (uint)-6){
188 for(i = 0; i < s->nvar; i++)
194 for(i = 0; i < n; i++){
195 l = litconv(s, a[i]);
197 if(v->stamp < s->stamp) u++;
198 if(v->stamp == s->stamp + (~l & 1))
199 return s; /* tautological */
200 v->stamp = s->stamp + (l & 1);
203 return satadd1special(s, a, n);
205 c = satnewclause(s, u, 0);
207 for(i = 0, j = 0; i < n; i++){
208 l = litconv(s, a[i]);
210 if(v->stamp < s->stamp){
226 if(sizeof(int)==sizeof(uintptr)) return;
231 while((int)*s++ != 0);
236 sataddv(SATSolve *s, ...)
243 s = satadd1(s, (int*)va, -1);