#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;} voidsatfree(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);} voidsaterror(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);} intsatval(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;} intsatnrand(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 voidheapup(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 voidheapdown(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;} voidsatheapput(SATSolve *s, SATVar *v){	assert(s->nheap < s->nvar);	v->heaploc = s->nheap;	s->heap[s->nheap++] = v;	heapdown(s, s->nheap - 1);} voidsatreheap(SATSolve *s, SATVar *v){	int i;		i = v->heaploc;	if(i < 0) return;	heapup(s, i);	heapdown(s, i);} voidsatheapreset(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);}