ref: c0280c607f92846cc05cb4a8c20c03fd4cea195a
dir: /sys/src/libsat/satadd.c/
#include <u.h> #include <libc.h> #include <sat.h> #include "impl.h" static SATBlock * newblock(SATSolve *s, int learned) { SATBlock *b; b = calloc(1, SATBLOCKSZ); if(b == nil) saterror(s, "malloc: %r"); b->prev = s->bl[learned].prev; b->next = &s->bl[learned]; b->next->prev = b; b->prev->next = b; b->end = (void*) b->data; return b; } SATClause * satnewclause(SATSolve *s, int n, int learned) { SATBlock *b; SATClause *c; int f, sz; sz = sizeof(SATClause) + (n - 1) * sizeof(int); assert(sz <= SATBLOCKSZ); if(learned) b = s->lastbl; else b = s->bl[0].prev; for(;;){ f = (uchar*)b + SATBLOCKSZ - (uchar*)b->end; if(f >= sz) break; b = b->next; if(b == &s->bl[learned]) b = newblock(s, learned); } c = b->end; memset(c, 0, sizeof(SATClause)); b->end = (void *)((uintptr)b->end + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN); b->last = c; if(learned){ if(s->lastp[1] == &s->learncl) *s->lastp[0] = c; s->lastbl = b; }else c->next = s->learncl; *s->lastp[learned] = c; s->lastp[learned] = &c->next; s->ncl++; return c; } /* this is currently only used to subsume clauses, i.e. n is guaranteed to be less than the last n */ SATClause * satreplclause(SATSolve *s, int n) { SATBlock *b; SATClause *c, **wp; int f, sz, i, l; assert(s->lastbl != nil && s->lastbl->last != nil); b = s->lastbl; c = b->last; f = (uchar*)b + SATBLOCKSZ - (uchar*)c; sz = sizeof(SATClause) + (n - 1) * sizeof(int); assert(f >= sz); b->end = (void *)((uintptr)c + sz + CLAUSEALIGN - 1 & -CLAUSEALIGN); for(i = 0; i < 2; i++){ l = c->l[i]; for(wp = &s->lit[l].watch; *wp != nil && *wp != c; wp = &(*wp)->watch[(*wp)->l[1] == l]) ; assert(*wp != nil); *wp = c->watch[i]; } memset(c, 0, sizeof(SATClause)); return c; } static int litconv(SATSolve *s, int l) { int v, m, n; SATVar *vp; SATLit *lp; m = l >> 31; v = (l + m ^ m) - 1; if(v >= s->nvaralloc){ n = -(-(v+1) & -SATVARALLOC); s->var = vp = satrealloc(s, s->var, n * sizeof(SATVar)); s->lit = lp = satrealloc(s, s->lit, 2 * n * sizeof(SATLit)); memset(vp += s->nvaralloc, 0, (n - s->nvaralloc) * sizeof(SATVar)); memset(lp += 2*s->nvaralloc, 0, 2 * (n - s->nvaralloc) * sizeof(SATLit)); for(; vp < s->var + n; vp++){ vp->lvl = -1; vp->flags = VARPHASE; } for(; lp < s->lit + 2 * n; lp++) lp->val = -1; s->nvaralloc = n; } if(v >= s->nvar) s->nvar = v + 1; return v << 1 | m & 1; } static void addbimp(SATSolve *s, int l0, int l1) { SATLit *lp; lp = &s->lit[NOT(l0)]; lp->bimp = satrealloc(s, lp->bimp, (lp->nbimp + 1) * sizeof(int)); lp->bimp[lp->nbimp++] = l1; } static SATSolve * satadd1special(SATSolve *s, int *a, int n) { int i, l0, l1; if(n == 0){ s->unsat = 1; return s; } l0 = a[0]; l1 = 0; for(i = 1; i < n; i++) if(a[i] != l0){ l1 = a[i]; break; } if(l1 == 0){ l0 = litconv(s, l0); assert(s->lvl == 0); switch(s->lit[l0].val){ case 0: s->unsat = 1; return s; case -1: s->trail = satrealloc(s, s->trail, sizeof(int) * s->nvar); memmove(&s->trail[1], s->trail, sizeof(int) * s->ntrail); s->trail[0] = l0; s->ntrail++; s->var[VAR(l0)].flags |= VARUSER; s->var[VAR(l0)].lvl = 0; s->lit[l0].val = 1; s->lit[NOT(l0)].val = 0; } return s; } if(l0 + l1 == 0) return s; l0 = litconv(s, l0); l1 = litconv(s, l1); addbimp(s, l0, l1); addbimp(s, l1, l0); return s; } SATSolve * satadd1(SATSolve *s, int *a, int n) { SATClause *c; int i, j, l, u; SATVar *v; if(s == nil){ s = satnew(); if(s == nil) saterror(nil, "satnew: %r"); } if(n < 0) for(n = 0; a[n] != 0; n++) ; for(i = 0; i < n; i++) if(a[i] == 0) saterror(s, "satadd1(%p, %p, %d): a[%d]==0, callerpc=%p", s, a, n, i, getcallerpc(&s)); satbackjump(s, 0); if(n <= 2) return satadd1special(s, a, n); /* use stamps to detect repeated literals and tautological clauses */ if(s->stamp >= (uint)-6){ for(i = 0; i < s->nvar; i++) s->var[i].stamp = 0; s->stamp = 1; }else s->stamp += 3; u = 0; for(i = 0; i < n; i++){ l = litconv(s, a[i]); v = &s->var[VAR(l)]; if(v->stamp < s->stamp) u++; if(v->stamp == s->stamp + (~l & 1)) return s; /* tautological */ v->stamp = s->stamp + (l & 1); } if(u <= 2) return satadd1special(s, a, n); s->stamp += 3; c = satnewclause(s, u, 0); c->n = u; for(i = 0, j = 0; i < n; i++){ l = litconv(s, a[i]); v = &s->var[VAR(l)]; if(v->stamp < s->stamp){ c->l[j++] = l; v->stamp = s->stamp; } } assert(j == u); s->ncl0++; return s; } void satvafix(va_list va) { int *d; uintptr *s; if(sizeof(int)==sizeof(uintptr)) return; d = (int *) va; s = (uintptr *) va; do *d++ = *s; while((int)*s++ != 0); } SATSolve * sataddv(SATSolve *s, ...) { va_list va; va_start(va, s); /* horrible hack */ satvafix(va); s = satadd1(s, (int*)va, -1); va_end(va); return s; }