From 2e2ae33a47951ec99ddefd61b8f16ffb47a88fed Mon Sep 17 00:00:00 2001
From: aiju <devnull@localhost>
Date: Thu, 22 Mar 2018 12:46:04 +0000
Subject: sat: add satget

---
 sys/src/libsat/mkfile   |  1 +
 sys/src/libsat/satget.c | 33 +++++++++++++++++++++++++++++++++
 2 files changed, 34 insertions(+)
 create mode 100644 sys/src/libsat/satget.c

(limited to 'sys/src/libsat')

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;
+}
-- 
cgit v1.2.3