add libsat

1 files changed, 206 insertions, 0 deletions

diff --git a/sys/src/libsat/misc.c b/sys/src/libsat/misc.c
new file mode 100644
index 000000000..e7e843529
--- /dev/null
+++ b/sys/src/libsat/misc.c
@@ -0,0 +1,206 @@
+#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");
+	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);
+}