add libsat

1 files changed, 130 insertions, 0 deletions

diff --git a/sys/src/libsat/debug.c b/sys/src/libsat/debug.c
new file mode 100644
index 000000000..0f9ffe30f
--- /dev/null
+++ b/sys/src/libsat/debug.c
@@ -0,0 +1,130 @@
+#include <u.h>
+#include <libc.h>
+#include <sat.h>
+#include "impl.h"
+
+static SATSolve *globsat;
+
+static int
+satclausefmt(Fmt *f)
+{
+	SATClause *c;
+	char *s;
+	int i, fl;
+	
+	fl = f->flags;
+	c = va_arg(f->args, SATClause *);
+	if(c == nil)
+		return fmtstrcpy(f, "Λ");
+	if(c->n == 0)
+		return fmtstrcpy(f, "ε");
+	s = "%s%d";
+	for(i = 0; i < c->n; i++){
+		if((fl & FmtSign) != 0)
+			switch(globsat->lit[c->l[i]].val){
+			case 1: s = "%s[%d]"; break;
+			case 0: s = "%s(%d)"; break;
+			case -1: s = "%s%d"; break;
+			default: abort();
+			}
+		fmtprint(f, s, i != 0 ? " ∨ " : "", signf(c->l[i]));
+	}
+	return 0;
+}
+
+void
+satprintstate(SATSolve *s)
+{
+	int i;
+	Fmt f;
+	char buf[512];
+	SATVar *v;
+	
+	fmtfdinit(&f, 1, buf, sizeof(buf));
+	fmtprint(&f, "trail:\n");
+	for(i = 0; i < s->ntrail; i++){
+		v = &s->var[VAR(s->trail[i])];
+		fmtprint(&f, "%c%-8d %- 8d %-8d ", i == s->forptr ? '*' : ' ', i, signf(s->trail[i]), v->lvl);
+		if(v->isbinreason)
+			fmtprint(&f, "%d ∨ %d\n", signf(s->trail[i]), signf(v->binreason));
+		else
+			fmtprint(&f, "%+Γ\n", v->reason);
+	}
+	fmtrune(&f, '\n');
+	fmtfdflush(&f);
+}
+
+void
+satsanity(SATSolve *s)
+{
+	int i, j, k, m, tl, s0, s1;
+	SATVar *v;
+	SATLit *l;
+	SATClause *c;
+	
+	for(c = s->cl; c != nil; c = c->next){
+		assert(c->n >= 2);
+		assert((uint)((uchar*)c->next - (uchar*)c) >= sizeof(SATClause) + (c->n - 1) * sizeof(int));
+		for(j = 0; j < c->n; j++)
+			assert((uint)c->l[j] < 2*s->nvar);
+		for(i = 0; i < 2; i++)
+			c->watch[i] = (void*)((uintptr)c->watch[i] | 1);
+	}
+	for(i = 0; i < s->nvar; i++){
+		tl = -1;
+		for(j = 0; j < s->ntrail; j++)
+			if(VAR(s->trail[j]) == i){
+				assert(tl == -1);
+				tl = j;
+			}
+		v = &s->var[i];
+		l = &s->lit[2*i];
+		if(l->val >= 0){
+			assert(l->val <= 1);
+			assert(l[0].val + l[1].val == 1);
+			assert((uint)v->lvl <= s->lvl);
+			assert(tl != -1);
+			assert(s->trail[tl] == 2*i+l[1].val);
+			assert(tl >= s->decbd[v->lvl]);
+			assert(v->lvl == s->lvl || tl < s->decbd[v->lvl+1]);
+		}else{
+			assert(l[0].val == -1 && l[1].val == -1);
+			assert(v->lvl == -1);
+			assert(v->heaploc >= 0);
+			assert(tl == -1);
+		}
+		assert(v->heaploc == -1 || (uint)v->heaploc <= s->nheap && s->heap[v->heaploc] == v);
+		for(j = 0; j < 2; j++){
+			m = 2 * i + j;
+			for(c = l[j].watch; c != nil; c = c->watch[k]){
+				k = c->l[1] == m;
+				assert(k || c->l[0] == m);
+				assert((uintptr)c->watch[k] & 1);
+				c->watch[k] = (void*)((uintptr)c->watch[k] & ~1);
+			}
+		}
+	}
+	for(c = s->cl; c != nil; c = c->next)
+		for(i = 0; i < 2; i++)
+			assert(((uintptr)c->watch[i] & 1) == 0);
+	if(s->forptr == s->ntrail)
+		for(c = s->cl; c != nil; c = c->next){
+			s0 = s->lit[c->l[0]].val;
+			s1 = s->lit[c->l[1]].val;
+			if(s0 != 0 && s1 != 0 || s0 == 1 || s1 == 1)
+				continue;
+			for(i = 2; i < c->n; i++)
+				if(s->lit[c->l[i]].val != 0){
+					satprintstate(s);
+					print("watchlist error: %+Γ\n", c);
+					assert(0);
+				}
+		}
+}
+
+void
+satdebuginit(SATSolve *s)
+{
+	globsat = s;
+	fmtinstall(L'Γ', satclausefmt);
+}