ref: e9e55a21f66a3eff114025dcb1fe62570d0fa3e6
dir: /sys/src/libsat/misc.c/
#include <u.h> #include <libc.h> #include <sat.h> #include "impl.h" SATSolve * satnew(void) { SATSolve *s; s = calloc(1, sizeof(SATSolve)); if(s == nil) return nil; s->bl[0].next = s->bl[0].prev = &s->bl[0]; s->bl[1].next = s->bl[1].prev = &s->bl[1]; s->bl[0].end = (uchar*)&s->bl[0] + SATBLOCKSZ; /* this block is "full" */ s->bl[1].end = (uchar*)&s->bl[1] + SATBLOCKSZ; s->lastp[0] = &s->cl; s->lastp[1] = &s->learncl; s->lastbl = &s->bl[1]; s->randfn = (long(*)(void*)) lrand; s->goofprob = 0.02 * (1UL<<31); s->varρ = 1/0.9; s->clauseρ = 1/0.999; s->trivlim = 10; s->purgeΔ = 10000; s->purgeδ = 100; s->purgeα = 0.2; s->flushψ = (1ULL<<32)*0.05; s->Δactivity = 1; s->Δclactivity = 1; return s; } void satfree(SATSolve *s) { SATBlock *b, *bb; int i; if(s == nil) return; for(i = 0; i < 2; i++) for(b = s->bl[i].next; b != &s->bl[i]; b = bb){ bb = b->next; free(b); } for(i = 0; i < 2 * s->nvar; i++) free(s->lit[i].bimp); free(s->heap); free(s->trail); free(s->decbd); free(s->var); free(s->lit); free(s->cflcl); free(s->fullrcfl); free(s->fullrlits); free(s->scrap); free(s); } void saterror(SATSolve *s, char *msg, ...) { char buf[ERRMAX]; va_list va; va_start(va, msg); vsnprint(buf, sizeof(buf), msg, va); va_end(va); s->scratched = 1; if(s != nil && s->errfun != nil) s->errfun(buf, s->erraux); sysfatal("%s", buf); } int satval(SATSolve *s, int l) { int m, v; if(s->unsat) return -1; m = l >> 31; v = (l + m ^ m) - 1; if(v < 0 || v >= s->nvar) return -1; return s->lit[2*v+(m&1)].val; } int satnrand(SATSolve *s, int n) { long slop, v; if(n <= 1) return 0; slop = 0x7fffffff % n; do v = s->randfn(s->randaux); while(v <= slop); return v % n; } void * satrealloc(SATSolve *s, void *v, ulong n) { v = realloc(v, n); if(v == nil) saterror(s, "realloc: %r"); setmalloctag(v, getcallerpc(&s)); return v; } #define LEFT(x) (2*(x)+1) #define RIGHT(x) (2*(x)+2) #define UP(x) ((x)-1>>1) static SATVar * heapswap(SATSolve *s, int i, int j) { SATVar *r; if(i == j) return s->heap[i]; r = s->heap[i]; s->heap[i] = s->heap[j]; s->heap[j] = r; s->heap[i]->heaploc = i; s->heap[j]->heaploc = j; return r; } static void heapup(SATSolve *s, int i) { int m; m = i; for(;;){ if(LEFT(i) < s->nheap && s->heap[LEFT(i)]->activity > s->heap[m]->activity) m = LEFT(i); if(RIGHT(i) < s->nheap && s->heap[RIGHT(i)]->activity > s->heap[m]->activity) m = RIGHT(i); if(i == m) break; heapswap(s, m, i); i = m; } } static void heapdown(SATSolve *s, int i) { int p; for(; i > 0 && s->heap[p = UP(i)]->activity < s->heap[i]->activity; i = p) heapswap(s, i, p); } SATVar * satheaptake(SATSolve *s) { SATVar *r; assert(s->nheap > 0); r = heapswap(s, 0, --s->nheap); heapup(s, 0); r->heaploc = -1; return r; } void satheapput(SATSolve *s, SATVar *v) { assert(s->nheap < s->nvar); v->heaploc = s->nheap; s->heap[s->nheap++] = v; heapdown(s, s->nheap - 1); } void satreheap(SATSolve *s, SATVar *v) { int i; i = v->heaploc; if(i < 0) return; heapup(s, i); heapdown(s, i); } void satheapreset(SATSolve *s) { int i, n, j; s->heap = satrealloc(s, s->heap, s->nvar * sizeof(SATVar *)); n = s->nvar; s->nheap = n; for(i = 0; i < n; i++){ s->heap[i] = &s->var[i]; s->heap[i]->heaploc = i; } for(i = 0; i < n - 1; i++){ j = i + satnrand(s, n - i); heapswap(s, i, j); heapdown(s, i); } heapdown(s, n - 1); }