shithub: riscv

--- a/sys/man/2/sat

+++ b/sys/man/2/sat

@@ -36,6 +36,7 @@

 int	satsolve(SATSolve *s);

 int	satmore(SATSolve *s);

 int	satval(SATSolve *s, int lit);

+int	satget(SATSolve *s, int i, int *lit, int nlit);

 void	satreset(SATSolve *s);

 .SH DESCRIPTION

.PP

@@ -122,6 +123,23 @@

 For example, the clause from above corresponds to

.IP

 .B "satrangev(s, 1, 1, 1, 2, 3, 0);"

+.PP

+For debugging purposes, clauses can be retrieved using

+.IR satget .

+It stores the literals of the clause with index

+.I i

+(starting from 0) at location

+.IR lit .

+If there are more than

+.I nlit

+literals, only the first

+.I nlit

+literals are stored.

+If it was successful, it returns the total number of literals in the clause (which may exceed

+.IR nlit ).

+Otherwise (if

+.I idx

+was out of bounds) it returns -1.

.PP

 .I Satreset

 resets all solver state, deleting all learned clauses and variable assignments.

--- a/sys/src/libsat/mkfile

+++ b/sys/src/libsat/mkfile

@@ -9,6 +9,7 @@

 	satsolve.$O \

 	satmore.$O \

 	debug.$O \

+	satget.$O \

 HFILES=\

 	/sys/include/sat.h\

--- /dev/null

+++ b/sys/src/libsat/satget.c

@@ -1,0 +1,33 @@

+#include <u.h>

+#include <libc.h>

+#include <sat.h>

+#include "impl.h"

+int

+satget(SATSolve *s, int i, int *t, int n)

+{

+	SATClause *c;

+	SATLit *l;

+	int j, k;

+	for(c = s->cl; c != s->learncl; c = c->next)

+		if(i-- == 0){

+			for(j = 0; j < n && j < c->n; j++)

+				t[j] = signf(c->l[j]);

+			return c->n;

+		}

+	for(l = s->lit; l < s->lit + 2 * s->nvar; l++)

+		for(k = 0; k < l->nbimp; k++)

+			if(i-- == 0){

+				if(n > 0) t[0] = -signf(l - s->lit);

+				if(n > 1) t[1] = signf(l->bimp[k]);

+				return 2;

+			}

+	for(; c != 0; c = c->next)

+		if(i-- == 0){

+			for(j = 0; j < n && j < c->n; j++)

+				t[j] = signf(c->l[j]);

+			return c->n;

+		}

+	return -1;

+}