sat: add satget

3 files changed, 52 insertions, 0 deletions

diff --git a/sys/man/2/sat b/sys/man/2/sat
index 7a14b6ae6..0d04f11a9 100644
--- a/sys/man/2/sat
+++ b/sys/man/2/sat
@@ -36,6 +36,7 @@ SATSolve*	satrangev(SATSolve *s, int min, int max, ...);
 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
@@ -123,6 +124,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.
 It retains all user provided clauses.
diff --git a/sys/src/libsat/mkfile b/sys/src/libsat/mkfile
index 08b1639e4..7df422b32 100644
--- a/sys/src/libsat/mkfile
+++ b/sys/src/libsat/mkfile
@@ -9,6 +9,7 @@ OFILES=\
 	satsolve.$O \
 	satmore.$O \
 	debug.$O \
+	satget.$O \
 
 HFILES=\
 	/sys/include/sat.h\
diff --git a/sys/src/libsat/satget.c b/sys/src/libsat/satget.c
new file mode 100644
index 000000000..264311135
--- /dev/null
+++ b/sys/src/libsat/satget.c
@@ -0,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;
+}