add forp

1 files changed, 273 insertions, 0 deletions

diff --git a/sys/src/cmd/forp/logic.c b/sys/src/cmd/forp/logic.c
new file mode 100644
index 000000000..b266e3bca
--- /dev/null
+++ b/sys/src/cmd/forp/logic.c
@@ -0,0 +1,273 @@
+#include <u.h>
+#include <libc.h>
+#include <mp.h>
+#include <sat.h>
+#include "dat.h"
+#include "fns.h"
+
+extern int satvar;
+
+int
+satand1(SATSolve *sat, int *a, int n)
+{
+	int i, j, r;
+	int *b;
+
+	if(n < 0)
+		for(n = 0; a[n] != 0; n++)
+			;
+	r = 2;
+	for(i = j = 0; i < n; i++){
+		if(a[i] == 1 || a[i] == -2)
+			return 1;
+		if(a[i] == 2 || a[i] == -1)
+			j++;
+		else
+			r = a[i];
+	}
+	if(j >= n - 1) return r;
+	r = satvar++;
+	b = malloc(sizeof(int) * (n+1));
+	for(i = j = 0; i < n; i++){
+		if(a[i] == 2 || a[i] == -1)
+			continue;
+		b[j++] = -a[i];
+		sataddv(sat, -r, a[i], 0);
+	}
+	b[j++] = r;
+	satadd1(sat, b, j);
+	return r;
+}
+
+int
+satandv(SATSolve *sat, ...)
+{
+	int r;
+	va_list va;
+	
+	va_start(va, sat);
+	r = satand1(sat, (int*)va, -1);
+	va_end(va);
+	return r;
+}
+
+int
+sator1(SATSolve *sat, int *a, int n)
+{
+	int i, j, r;
+	int *b;
+
+	if(n < 0)
+		for(n = 0; a[n] != 0; n++)
+			;
+	r = 1;
+	for(i = j = 0; i < n; i++){
+		if(a[i] == 2 || a[i] == -1)
+			return 2;
+		if(a[i] == 1 || a[i] == -2)
+			j++;
+		else
+			r = a[i];
+	}
+	if(j >= n-1) return r;
+	r = satvar++;
+	b = malloc(sizeof(int) * (n+1));
+	for(i = j = 0; i < n; i++){
+		if(a[i] == 1 || a[i] == -2)
+			continue;
+		b[j++] = a[i];
+		sataddv(sat, r, -a[i], 0);
+	}
+	b[j++] = -r;
+	satadd1(sat, b, j);
+	return r;
+}
+
+int
+satorv(SATSolve *sat, ...)
+{
+	va_list va;
+	int r;
+	
+	va_start(va, sat);
+	r = sator1(sat, (int*)va, -1);
+	va_end(va);
+	return r;
+}
+
+typedef struct { u8int x, m; } Pi;
+static Pi *π;
+static int nπ;
+static u64int *πm;
+
+static void
+pimp(u64int op, int n)
+{
+	int i, j, k;
+	u8int δ;
+
+	nπ = 0;
+	for(i = 0; i < 1<<n; i++)
+		if((op >> i & 1) != 0){
+			π = realloc(π, sizeof(Pi) * (nπ + 1));
+			π[nπ++] = (Pi){i, 0};
+		}
+	for(i = 0; i < nπ; i++){
+		for(j = 0; j < i; j++){
+			δ = π[i].x ^ π[j].x;
+			if(δ == 0 || (δ & δ - 1) != 0 || π[i].m != π[j].m) continue;
+			if(((π[i].m | π[j].m) & δ) != 0) continue;
+			if(π[nπ-1].x == (π[i].x & π[j].x) && π[nπ-1].m == (π[i].m | δ)) continue;
+			π = realloc(π, sizeof(Pi) * (nπ + 1));
+			π[nπ++] = (Pi){π[i].x & π[j].x, π[i].m | δ};
+		}
+	}
+	for(i = k = 0; i < nπ; i++){
+		for(j = i+1; j < nπ; j++)
+			if((π[i].m & ~π[j].m) == 0 && (π[i].x & ~π[j].m) == π[j].x)
+				break;
+		if(j == nπ)
+			π[k++] = π[i];
+	}
+	nπ = k;
+	assert(nπ <= 1<<n);
+}
+
+static void
+pimpmask(void)
+{
+	int i, j;
+	u64int m;
+
+	πm = realloc(πm, sizeof(u64int) * nπ);
+	for(i = 0; i < nπ; i++){
+		m = 0;
+		for(j = π[i].m; ; j = j - 1 & π[i].m){
+			m |= 1ULL<<(π[i].x | j);
+			if(j == 0) break;
+		}
+		πm[i] = m;
+	}
+}
+
+static int
+popcnt(u64int m)
+{
+	m = (m & 0x5555555555555555ULL) + (m >> 1 & 0x5555555555555555ULL);
+	m = (m & 0x3333333333333333ULL) + (m >> 2 & 0x3333333333333333ULL);
+	m = (m & 0x0F0F0F0F0F0F0F0FULL) + (m >> 4 & 0x0F0F0F0F0F0F0F0FULL);
+	m = (m & 0x00FF00FF00FF00FFULL) + (m >> 8 & 0x00FF00FF00FF00FFULL);
+	m = (m & 0x0000FFFF0000FFFFULL) + (m >> 16 & 0x0000FFFF0000FFFFULL);
+	m = (u32int)m + (u32int)(m >> 32);
+	return m;
+}
+
+static u64int
+pimpcover(u64int op, int)
+{
+	int i, j, maxi, p, maxp;
+	u64int cov, yes, m;
+	
+	yes = 0;
+	cov = op;
+	for(i = 0; i < nπ; i++){
+		if((yes & 1<<i) != 0) continue;
+		m = πm[i];
+		for(j = 0; j < nπ; j++){
+			if(j == i) continue;
+			m &= ~πm[j];
+			if(m == 0) break;
+		}
+		if(j == nπ){
+			yes |= 1<<i;
+			cov &= ~πm[i];
+		}
+	}
+	while(cov != 0){
+		j = popcnt(~cov & cov - 1);
+		maxi = -1;
+		maxp = 0;
+		for(i = 0; i < nπ; i++){
+			if((πm[i] & 1<<j) == 0) continue;
+			if((p = popcnt(πm[i] & cov)) > maxp)
+				maxi = i, maxp = p;
+		}
+		assert(maxi >= 0);
+		yes |= 1<<maxi;
+		cov &= ~πm[maxi];
+	}
+	return yes;
+}
+
+static void
+pimpsat(SATSolve *sat, u64int yes, int *a, int n, int r)
+{
+	int i, j, k;
+	int *cl;
+
+	cl = emalloc(sizeof(int) * (n + 1));
+	while(yes != 0){
+		i = popcnt(~yes & yes - 1);
+		yes &= yes - 1;
+		k = 0;
+		cl[k++] = r;
+		for(j = 0; j < n; j++)
+			if((π[i].m & 1<<j) == 0)
+				cl[k++] = (π[i].x >> j & 1) != 0 ? -a[j] : a[j];
+//		for(i = 0; i < k; i++) print("%d ", cl[i]); print("\n");
+		satadd1(sat, cl, k);
+	}
+	free(cl);
+}
+
+int
+satlogic1(SATSolve *sat, u64int op, int *a, int n)
+{
+	int i, j, o, r;
+	int s;
+
+	if(n < 0)
+		for(n = 0; a[n] != 0; n++)
+			;
+	assert(op >> (1<<n) == 0);
+	s = 0;
+	j = -1;
+	for(i = n; --i >= 0; ){
+		if((uint)(a[i] + 2) > 4){
+			if(j >= 0) break;
+			j = i;
+		}
+		s = s << 1 | a[i] == 2 | a[i] == -1;
+	}
+	if(i < 0){
+		if(j < 0) return 1 + (op >> s & 1);
+		o = op >> s & 1 | op >> s + (1<<j) - 1 & 2;
+		switch(o){
+		case 0: return 1;
+		case 1: return -a[j];
+		case 2: return a[j];
+		case 3: return 2;
+		}
+	}
+	r = satvar++;
+	pimp(op, n);
+	pimpmask();
+	pimpsat(sat, pimpcover(op, n), a, n, r);
+	op ^= (u64int)-1 >> 64-(1<<n);
+	pimp(op, n);
+	pimpmask();
+	pimpsat(sat, pimpcover(op, n), a, n, -r);
+	return r;
+}
+
+int
+satlogicv(SATSolve *sat, u64int op, ...)
+{
+	va_list va;
+	int r;
+	
+	va_start(va, op);
+	r = satlogic1(sat, op, (int*)va, -1);
+	va_end(va);
+	return r;
+}