shithub: riscv

Download patch

ref: 382d37dbf0ee8bf5af9594e922db6094e30ace2a
parent: 80474f7f59ee755cd1967c5703e3be724582f001
author: aiju <devnull@localhost>
date: Wed Mar 28 13:08:30 EDT 2018 

add forp


--- /dev/null
+++ b/sys/src/cmd/forp/cvt.c
@@ -1,0 +1,525 @@
+#include <u.h>
+#include <libc.h>
+#include <mp.h>
+#include <sat.h>
+#include "dat.h"
+#include "fns.h"
+
+SATSolve *sat;
+int satvar = 3; /* 1 = false, 2 = true */
+#define SVAR(n, i) ((n)->vars[(i) < (n)->size ? (i) : (n)->size - 1])
+int nassertvar;
+int *assertvar;
+
+static int
+max(int a, int b)
+{
+	return a < b ? b : a;
+}
+
+static int
+min(int a, int b)
+{
+	return a > b ? b : a;
+}
+
+static void
+symsat(Node *n)
+{
+	Symbol *s;
+	int i;
+	
+	s = n->sym;
+	assert(s->type == SYMBITS);
+	n->size = s->size + ((s->flags & SYMFSIGNED) == 0);
+	n->vars = emalloc(sizeof(int) * n->size);
+	for(i = 0; i < s->size; i++){
+		if(s->vars[i] == 0)
+			s->vars[i] = satvar++;
+		n->vars[i] = s->vars[i];
+	}
+	if((s->flags & SYMFSIGNED) == 0)
+		n->vars[i] = 1;
+}
+
+static void
+numsat(Node *n)
+{
+	mpint *m;
+	int i, sz, j;
+	
+	m = n->num;
+	assert(m != nil);
+	assert(m->sign > 0);
+	sz = mpsignif(m) + 1;
+	n->size = sz;
+	n->vars = emalloc(sizeof(int) * sz);
+	for(i = 0; i < m->top; i++){
+		for(j = 0; j < Dbits; j++)
+			if(i * Dbits + j < sz-1)
+				n->vars[i * Dbits + j] = 1 + ((m->p[i] >> j & 1) != 0);
+	}
+	n->vars[sz - 1] = 1;
+}
+
+static void
+nodevars(Node *n, int nv)
+{
+	int i;
+
+	n->size = nv;
+	n->vars = emalloc(sizeof(int) * nv);
+	for(i = 0; i < nv; i++)
+		n->vars[i] = 1;
+}
+
+static void
+assign(Node *t, Node *n)
+{
+	Symbol *s;
+	int i;
+	
+	s = t->sym;
+	for(i = 0; i < s->size; i++){
+		if(i < n->size)
+			s->vars[i] = n->vars[i];
+		else
+			s->vars[i] = n->vars[n->size - 1];
+	}
+}
+
+static void
+opeq(Node *r, Node *n1, Node *n2, int neq)
+{
+	int i, m, a, b, *t;
+
+	nodevars(r, 2);
+	m = max(n1->size, n2->size);
+	t = malloc(m * sizeof(int));
+	for(i = 0; i < m; i++){
+		a = SVAR(n1, i);
+		b = SVAR(n2, i);
+		t[i] = satlogicv(sat, neq ? 6 : 9, a, b, 0);
+	}
+	if(neq)
+		r->vars[0] = sator1(sat, t, m);
+	else
+		r->vars[0] = satand1(sat, t, m);
+	free(t);
+}
+
+static void
+oplogic(Node *r, Node *n1, Node *n2, int op)
+{
+	int m, i, a, b, *t;
+	
+	m = max(n1->size, n2->size);
+	nodevars(r, m);
+	t = r->vars;
+	for(i = 0; i < m; i++){
+		a = SVAR(n1, i);
+		b = SVAR(n2, i);
+		switch(op){
+		case OPOR:
+			t[i] = satorv(sat, a, b, 0);
+			break;
+		case OPAND:
+			t[i] = satandv(sat, a, b, 0);
+			break;
+		case OPXOR:
+			t[i] = satlogicv(sat, 6, a, b, 0);
+			break;
+		default: abort();
+		}
+	}
+}
+
+static int
+tologic(Node *n)
+{
+	int i;
+
+	for(i = 1; i < n->size; i++)
+		if(n->vars[i] != 1)
+			break;
+	if(i == n->size)
+		return n->vars[0];
+	return sator1(sat, n->vars, n->size);
+}
+
+static void
+opllogic(Node *rn, Node *n1, Node *n2, int op)
+{
+	int a, b;
+	
+	a = tologic(n1);
+	b = tologic(n2);
+	nodevars(rn, 2);
+	switch(op){
+	case OPLAND:
+		rn->vars[0] = satandv(sat, a, b, 0);
+		break;
+	case OPLOR:
+		rn->vars[0] = satorv(sat, a, b, 0);
+		break;
+	case OPIMP:
+		rn->vars[0] = satorv(sat, -a, b, 0);
+		break;
+	case OPEQV:
+		rn->vars[0] = satlogicv(sat, 9, a, b, 0);
+		break;
+	default:
+		abort();
+	}
+}
+
+static void
+opcom(Node *r, Node *n1)
+{
+	int i;
+	
+	nodevars(r, n1->size);
+	for(i = 0; i < n1->size; i++)
+		r->vars[i] = -n1->vars[i];
+}
+
+static void
+opneg(Node *r, Node *n1)
+{
+	int i, c;
+	
+	nodevars(r, n1->size);
+	c = 2;
+	for(i = 0; i < n1->size; i++){
+		r->vars[i] = satlogicv(sat, 9, n1->vars[i], c, 0);
+		if(i < n1->size - 1)
+			c = satandv(sat, -n1->vars[i], c, 0);
+	}
+}
+
+static void
+opnot(Node *r, Node *n1)
+{
+	nodevars(r, 2);
+	r->vars[0] = -tologic(n1);
+}
+
+static void
+opadd(Node *rn, Node *n1, Node *n2, int sub)
+{
+	int i, m, c, a, b;
+	
+	m = max(n1->size, n2->size) + 1;
+	nodevars(rn, m);
+	c = 1 + sub;
+	sub = 1 - 2 * sub;
+	for(i = 0; i < m; i++){
+		a = SVAR(n1, i);
+		b = SVAR(n2, i) * sub;
+		rn->vars[i] = satlogicv(sat, 0x96, c, a, b, 0);
+		c = satlogicv(sat, 0xe8, c, a, b, 0);
+	}
+}
+
+static void
+oplt(Node *rn, Node *n1, Node *n2, int le)
+{
+	int i, m, a, b, t, *r;
+	
+	nodevars(rn, 2);
+	m = max(n1->size, n2->size);
+	r = emalloc(sizeof(int) * (m + le));
+	t = 2;
+	for(i = m; --i >= 0; ){
+		if(i == m - 1){
+			a = SVAR(n2, i);
+			b = SVAR(n1, i);
+		}else{
+			a = SVAR(n1, i);
+			b = SVAR(n2, i);
+		}
+		r[i] = satandv(sat, -a, b, t, 0);
+		t = satlogicv(sat, 0x90, a, b, t, 0);
+	}
+	if(le)
+		r[m] = t;
+	rn->vars[0] = sator1(sat, r, m + le);
+}
+
+static void
+opidx(Node *rn, Node *n1, Node *n2, Node *n3)
+{
+	int i, j, k, s;
+	
+	j = mptoi(n2->num);
+	if(n3 == nil) k = j;
+	else k = mptoi(n3->num);
+	if(j > k){
+		nodevars(rn, 1);
+		return;
+	}
+	s = k - j + 1;
+	nodevars(rn, s + 1);
+	for(i = 0; i < s; i++)
+		rn->vars[i] = SVAR(n1, j + i);
+}
+
+static void
+oprsh(Node *rn, Node *n1, Node *n2)
+{
+	int i, j, a, b, q;
+
+	nodevars(rn, n1->size);
+	memcpy(rn->vars, n1->vars, sizeof(int) * n1->size);
+	for(i = 0; i < n2->size; i++){
+		if(n2->vars[i] == 1) continue;
+		if(n2->vars[i] == 2){
+			for(j = 0; j < n1->size; j++)
+				rn->vars[j] = SVAR(rn, j + (1<<i));
+			continue;
+		}
+		for(j = 0; j < n1->size; j++){
+			a = rn->vars[j];
+			b = SVAR(rn, j + (1<<i));
+			q = n2->vars[i];
+			rn->vars[j] = satlogicv(sat, 0xca, a, b, q, 0);
+		}
+	}
+}
+
+static void
+oplsh(Node *rn, Node *n1, Node *n2, uint sz)
+{
+	int i, j, a, b, q;
+	u32int m;
+	
+	m = 0;
+	for(i = n2->size; --i >= 0; )
+		m = m << 1 | n2->vars[i] != m;
+	m += n1->size;
+	if(m > sz) m = sz;
+	nodevars(rn, m);
+	for(i = 0; i < m; i++)
+		rn->vars[i] = SVAR(n1, i);
+	for(i = 0; i < n2->size; i++){
+		if(n2->vars[i] == 1) continue;
+		if(n2->vars[i] == 2){
+			for(j = m; --j >= 0; )
+				rn->vars[j] = j >= 1<<i ? rn->vars[j - (1<<i)] : 1;
+			continue;
+		}
+		for(j = m; --j >= 0; ){
+			a = rn->vars[j];
+			b = j >= 1<<i ? rn->vars[j - (1<<i)] : 1;
+			q = n2->vars[i];
+			rn->vars[j] = satlogicv(sat, 0xca, a, b, q, 0);
+		}
+	}	
+}
+
+static void
+optern(Node *rn, Node *n1, Node *n2, Node *n3, uint sz)
+{
+	uint m;
+	int i, a, b, q;
+	
+	m = n1->size;
+	if(n2->size > m) m = n2->size;
+	if(m > sz) m = sz;
+	nodevars(rn, m);
+	q = tologic(n1);
+	for(i = 0; i < m; i++){
+		a = SVAR(n3, i);
+		b = SVAR(n2, i);
+		rn->vars[i] = satlogicv(sat, 0xca, a, b, q, 0);
+	}
+}
+
+static int *
+opmul(int *n1v, int s1, int *n2v, int s2)
+{
+	int i, k, t, s;
+	int *r, *q0, *q1, *z, nq0, nq1, nq;
+
+	s1--;
+	s2--;
+	r = emalloc(sizeof(int) * (s1 + s2 + 2));
+	nq = 2 * (min(s1, s2) + 1);
+	q0 = emalloc(nq * sizeof(int));
+	q1 = emalloc(nq * sizeof(int));
+	nq0 = nq1 = 0;
+	for(k = 0; k <= s1 + s2 + 1; k++){
+		if(k == s1 || k == s1 + s2 + 1){ assert(nq0 < nq); q0[nq0++] = 2; }
+		if(k == s2){ assert(nq0 < nq); q0[nq0++] = 2; }
+		for(i = max(0, k - s2); i <= k && i <= s1; i++){
+			assert(nq0 < nq);
+			t = satandv(sat, n1v[i], n2v[k - i], 0);
+			q0[nq0++] = i == s1 ^ k-i == s2 ? -t : t;
+		}
+		assert(nq0 > 0);
+		while(nq0 > 1){
+			if(nq0 == 2){
+				t = satlogicv(sat, 0x6, q0[0], q0[1], 0);
+				s = satandv(sat, q0[0], q0[1], 0);
+				q0[0] = t;
+				assert(nq1 < nq);
+				q1[nq1++] = s;
+				break;
+			}
+			t = satlogicv(sat, 0x96, q0[nq0-3], q0[nq0-2], q0[nq0-1], 0);
+			s = satlogicv(sat, 0xe8, q0[nq0-3], q0[nq0-2], q0[nq0-1], 0);
+			q0[nq0-3] = t;
+			nq0 -= 2;
+			assert(nq1 < nq);
+			q1[nq1++] = s;
+		}
+		r[k] = q0[0];
+		z=q0, q0=q1, q1=z;
+		nq0 = nq1;
+		nq1 = 0;
+	}
+	free(q0);
+	free(q1);
+	return r;
+}
+
+static void
+opabs(Node *q, Node *n)
+{
+	int i;
+	int s, c;
+
+	nodevars(q, n->size + 1);
+	s = n->vars[n->size - 1];
+	c = s;
+	for(i = 0; i < n->size; i++){
+		q->vars[i] = satlogicv(sat, 0x96, n->vars[i], s, c, 0);
+		c = satandv(sat, -n->vars[i], c, 0);
+	}
+}
+
+static void
+opdiv(Node *q, Node *r, Node *n1, Node *n2)
+{
+	Node *s;
+	int i;
+	
+	if(q == nil) q = node(ASTTEMP);
+	if(r == nil) r = node(ASTTEMP);
+	nodevars(q, n1->size);
+	nodevars(r, n2->size);
+	for(i = 0; i < n1->size; i++)
+		q->vars[i] = satvar++;
+	for(i = 0; i < n2->size; i++)
+		r->vars[i] = satvar++;
+	s = node(ASTBIN, OPEQ, node(ASTBIN, OPADD, node(ASTBIN, OPMUL, q, n2), r), n1); convert(s, -1); assume(s);
+	s = node(ASTBIN, OPGE, r, node(ASTNUM, mpnew(0))); convert(s, -1); assume(s);
+	s = node(ASTBIN, OPLT, r, node(ASTUN, OPABS, n2)); convert(s, -1); assume(s);
+}
+
+void
+convert(Node *n, uint sz)
+{
+	if(n->size > 0) return;
+	switch(n->type){
+	case ASTTEMP:
+		assert(n->size > 0);
+		break;
+	case ASTSYM:
+		symsat(n);
+		break;
+	case ASTNUM:
+		numsat(n);
+		break;
+	case ASTBIN:
+		if(n->op == OPASS){
+			if(n->n1 == nil || n->n1->type != ASTSYM)
+				error(n, "convert: '%ε' invalid lval", n->n1);
+			convert(n->n2, n->n1->sym->size);
+			assert(n->n2->size > 0);
+			assign(n->n1, n->n2);
+			break;
+		}
+		switch(n->op){
+		case OPAND: case OPOR: case OPXOR:
+		case OPADD: case OPSUB: case OPLSH:
+		case OPCOMMA:
+			convert(n->n1, sz);
+			convert(n->n2, sz);
+			break;
+		default:
+			convert(n->n1, -1);
+			convert(n->n2, -1);
+		}
+		assert(n->n1->size > 0);
+		assert(n->n2->size > 0);
+		switch(n->op){
+		case OPCOMMA: n->size = n->n2->size; n->vars = n->n2->vars; break;
+		case OPEQ: opeq(n, n->n1, n->n2, 0); break;
+		case OPNEQ: opeq(n, n->n1, n->n2, 1); break;
+		case OPLT: oplt(n, n->n1, n->n2, 0); break;
+		case OPLE: oplt(n, n->n1, n->n2, 1); break;
+		case OPGT: oplt(n, n->n2, n->n1, 0); break;
+		case OPGE: oplt(n, n->n2, n->n1, 1); break;
+		case OPXOR: case OPAND: case OPOR: oplogic(n, n->n1, n->n2, n->op); break;
+		case OPLAND: case OPLOR: case OPIMP: case OPEQV: opllogic(n, n->n1, n->n2, n->op); break;
+		case OPADD: opadd(n, n->n1, n->n2, 0); break;
+		case OPSUB: opadd(n, n->n1, n->n2, 1); break;
+		case OPLSH: oplsh(n, n->n1, n->n2, sz); break;
+		case OPRSH: oprsh(n, n->n1, n->n2); break;
+		case OPMUL: n->vars = opmul(n->n1->vars, n->n1->size, n->n2->vars, n->n2->size); n->size = n->n1->size + n->n2->size; break;
+		case OPDIV: opdiv(n, nil, n->n1, n->n2); break;
+		case OPMOD: opdiv(nil, n, n->n1, n->n2); break;
+		default:
+			error(n, "convert: unimplemented op %O", n->op);
+		}
+		break;
+	case ASTUN:
+		convert(n->n1, sz);
+		switch(n->op){
+		case OPCOM: opcom(n, n->n1); break;
+		case OPNEG: opneg(n, n->n1); break;
+		case OPNOT: opnot(n, n->n1); break;
+		case OPABS: opabs(n, n->n1); break;
+		default:
+			error(n, "convert: unimplemented op %O", n->op);
+		}
+		break;
+	case ASTIDX:
+		if(n->n2->type != ASTNUM || n->n3 != nil && n->n3->type != ASTNUM)
+			error(n, "non-constant in indexing expression");
+		convert(n->n1, (n->n3 != nil ? mptoi(n->n3->num) : mptoi(n->n2->num)) + 1);
+		opidx(n, n->n1, n->n2, n->n3);
+		break;
+	case ASTTERN:
+		convert(n->n1, -1);
+		convert(n->n2, sz);
+		convert(n->n3, sz);
+		optern(n, n->n1, n->n2, n->n3, sz);
+		break;
+	default:
+		error(n, "convert: unimplemented %α", n->type);
+	}
+}
+
+void
+assume(Node *n)
+{
+	assert(n->size > 0);
+	satadd1(sat, n->vars, n->size);
+}
+
+void
+obviously(Node *n)
+{
+	assertvar = realloc(assertvar, sizeof(int) * (nassertvar + 1));
+	assert(assertvar != nil);
+	assertvar[nassertvar++] = -tologic(n);
+}
+
+void
+cvtinit(void)
+{
+	sat = sataddv(nil, -1, 0);
+	sataddv(sat, 2, 0);
+}
--- /dev/null
+++ b/sys/src/cmd/forp/dat.h
@@ -1,0 +1,94 @@
+typedef struct Line Line;
+typedef struct Node Node;
+typedef struct Symbol Symbol;
+typedef struct Trie Trie;
+typedef struct TrieHead TrieHead;
+
+struct Line {
+	char *filen;
+	int lineno;
+};
+
+struct TrieHead {
+	uvlong hash;
+	int l;
+};
+
+enum { TRIEB = 4 };
+struct Trie {
+	TrieHead;
+	Trie *n[1<<TRIEB];
+};
+
+struct Symbol {
+	TrieHead;
+	char *name;
+	int type;
+	int size;
+	int flags;
+	int *vars;
+	Symbol *next;
+};
+enum {
+	SYMNONE,
+	SYMBITS,
+};
+enum {
+	SYMFSIGNED = 1,
+};
+
+struct Node {
+	int type;
+	Line;
+	int op;
+	mpint *num;
+	Symbol *sym;
+	Node *n1, *n2, *n3;
+	int size;
+	int *vars;
+};
+enum {
+	ASTINVAL,
+	ASTSYM,
+	ASTNUM,
+	ASTBIN,
+	ASTUN,
+	ASTIDX,
+	ASTTERN,
+	ASTTEMP,
+};
+enum {
+	OPINVAL,
+	OPABS,
+	OPADD,
+	OPAND,
+	OPASS,
+	OPCOM,
+	OPCOMMA,
+	OPDIV,
+	OPEQ,
+	OPEQV,
+	OPGE,
+	OPGT,
+	OPIMP,
+	OPLAND,
+	OPLE,
+	OPLOR,
+	OPLSH,
+	OPLT,
+	OPMOD,
+	OPMUL,
+	OPNEG,
+	OPNEQ,
+	OPNOT,
+	OPOR,
+	OPRSH,
+	OPSUB,
+	OPXOR,
+};
+
+extern Symbol *syms;
+
+#pragma varargck type "ε" Node*
+#pragma varargck type "α" int
+#pragma varargck type "O" int
--- /dev/null
+++ b/sys/src/cmd/forp/fns.h
@@ -1,0 +1,18 @@
+typedef struct SATSolve SATSolve;
+
+void *emalloc(ulong);
+void *erealloc(void *, ulong);
+void parse(char *);
+void error(Line *, char *, ...);
+Node *node(int t, ...);
+Symbol *symget(char *);
+void convert(Node *, uint);
+void obviously(Node *);
+void go(int);
+void assume(Node *);
+int satand1(SATSolve *, int *, int);
+int satandv(SATSolve *, ...);
+int sator1(SATSolve *, int *, int);
+int satorv(SATSolve *, ...);
+int satlogic1(SATSolve *, u64int, int *, int);
+int satlogicv(SATSolve *, u64int, ...);
--- /dev/null
+++ b/sys/src/cmd/forp/forp.c
@@ -1,0 +1,159 @@
+#include <u.h>
+#include <libc.h>
+#include <mp.h>
+#include <sat.h>
+#include "dat.h"
+#include "fns.h"
+
+extern SATSolve *sat;
+extern int *assertvar, nassertvar;
+
+int
+printval(Symbol *s, Fmt *f)
+{
+	int i;
+	
+	if(s->type != SYMBITS) return 0;
+	fmtprint(f, "%s = ", s->name);
+	for(i = s->size - 1; i >= 0; i--)
+		switch(satval(sat, s->vars[i])){
+		case 1: fmtrune(f, '1'); break;
+		case 0: fmtrune(f, '0'); break;
+		case -1: fmtrune(f, '?'); break;
+		default: abort();
+		}
+	fmtprint(f, "\n");
+	return 0;
+}
+
+void
+debugsat(void)
+{
+	int i, j, rc;
+	int *t;
+	int ta;
+	Fmt f;
+	char buf[256];
+	
+	ta = 0;
+	t = nil;
+	fmtfdinit(&f, 1, buf, 256);
+	for(i = 0;;){
+		rc = satget(sat, i, t, ta);
+		if(rc < 0) break;
+		if(rc > ta){
+			ta = rc;
+			t = realloc(t, ta * sizeof(int));
+			continue;
+		}
+		i++;
+		fmtprint(&f, "%d: ", i);
+		for(j = 0; j < rc; j++)
+			fmtprint(&f, "%s%d", j==0?"":" ∨ ", t[j]);
+		fmtprint(&f, "\n");
+	}
+	free(t);
+	fmtfdflush(&f);
+}
+
+void
+tabheader(Fmt *f)
+{
+	Symbol *s;
+	int l, first;
+	
+	first = 0;
+	for(s = syms; s != nil; s = s->next){
+		if(s->type != SYMBITS) continue;
+		l = strlen(s->name);
+		if(s->size > l) l = s->size;
+		fmtprint(f, "%s%*s", first++ != 0 ? " " : "", l, s->name);
+	}
+	fmtrune(f, '\n');
+}
+
+void
+tabrow(Fmt *f)
+{
+	Symbol *s;
+	int i, l, first;
+	
+	first = 0;
+	for(s = syms; s != nil; s = s->next){
+		if(s->type != SYMBITS) continue;
+		if(first++ != 0) fmtrune(f, ' ');
+		l = strlen(s->name);
+		if(s->size > l) l = s->size;
+		for(i = l - 1; i > s->size - 1; i--)
+			fmtrune(f, ' ');
+		for(; i >= 0; i--)
+			switch(satval(sat, s->vars[i])){
+			case 1: fmtrune(f, '1'); break;
+			case 0: fmtrune(f, '0'); break;
+			case -1: fmtrune(f, '?'); break;
+			default: abort();
+			}
+	}
+	fmtrune(f, '\n');
+}
+
+void
+go(int mflag)
+{
+	Fmt f;
+	char buf[256];
+	Symbol *s;
+
+	if(nassertvar == 0)
+		sysfatal("left as an exercise to the reader");
+	satadd1(sat, assertvar, nassertvar);
+//	debugsat();
+	if(mflag){
+		fmtfdinit(&f, 1, buf, sizeof(buf));
+		tabheader(&f);
+		fmtfdflush(&f);
+		while(satmore(sat) > 0){
+			tabrow(&f);
+			fmtfdflush(&f);
+		}
+	}else{
+		if(satsolve(sat) == 0)
+			print("Proved.\n");
+		else{
+			fmtfdinit(&f, 1, buf, sizeof(buf));
+			for(s = syms; s != nil; s = s->next)
+				printval(s, &f);
+			fmtfdflush(&f);
+		}
+	}
+}
+
+void
+usage(void)
+{
+	fprint(2, "usage: %s [ -m ] [ file ]\n", argv0);
+	exits("usage");
+}
+
+void
+main(int argc, char **argv)
+{
+	typedef void init(void);
+	init miscinit, cvtinit, parsinit;
+	static int mflag;
+	
+	ARGBEGIN{
+	case 'm': mflag++; break;
+	default: usage();
+	}ARGEND;
+	
+	if(argc > 1) usage();
+
+	quotefmtinstall();
+	fmtinstall('B', mpfmt);
+	miscinit();
+	cvtinit();
+	parsinit();
+	parse(argc > 0 ? argv[0] : nil);
+	go(mflag);
+}
--- /dev/null
+++ b/sys/src/cmd/forp/logic.c
@@ -1,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;
+}
--- /dev/null
+++ b/sys/src/cmd/forp/misc.c
@@ -1,0 +1,246 @@
+#include <u.h>
+#include <libc.h>
+#include <mp.h>
+#include "dat.h"
+#include "fns.h"
+
+char *astnames[] = {
+	[ASTINVAL] "ASTINVAL",
+	[ASTSYM] "ASTSYM",
+	[ASTNUM] "ASTNUM",
+	[ASTBIN] "ASTBIN",
+	[ASTUN] "ASTUN",
+	[ASTIDX] "ASTIDX",
+	[ASTTERN] "ASTTERN",
+	[ASTTEMP] "ASTTEMP",
+};
+
+char *opnames[] = {
+	[OPABS] "OPABS",
+	[OPADD] "OPADD",
+	[OPAND] "OPAND",
+	[OPASS] "OPASS",
+	[OPCOM] "OPCOM",
+	[OPCOMMA] "OPCOMMA",
+	[OPDIV] "OPDIV",
+	[OPEQ] "OPEQ",
+	[OPEQV] "OPEQV",
+	[OPGE] "OPGE",
+	[OPGT] "OPGT",
+	[OPIMP] "OPIMP",
+	[OPINVAL] "OPINVAL",
+	[OPLAND] "OPLAND",
+	[OPLE] "OPLE",
+	[OPLOR] "OPLOR",
+	[OPLSH] "OPLSH",
+	[OPLT] "OPLT",
+	[OPMOD] "OPMOD",
+	[OPMUL] "OPMUL",
+	[OPNEG] "OPNEG",
+	[OPNEQ] "OPNEQ",
+	[OPNOT] "OPNOT",
+	[OPOR] "OPOR",
+	[OPRSH] "OPRSH",
+	[OPSUB] "OPSUB",
+	[OPXOR] "OPXOR",
+};
+
+Trie *root;
+Symbol *syms, **lastsymp = &syms;
+
+void *
+emalloc(ulong sz)
+{
+	void *v;
+	
+	v = malloc(sz);
+	if(v == nil) sysfatal("malloc: %r");
+	setmalloctag(v, getmalloctag(&sz));
+	memset(v, 0, sz);
+	return v;
+}
+
+void *
+erealloc(void *v, ulong sz)
+{
+	v = realloc(v, sz);
+	if(v == nil) sysfatal("realloc: %r");
+	setrealloctag(v, getmalloctag(&v));
+	return v;
+}
+
+static int
+astfmt(Fmt *f)
+{
+	int t;
+	
+	t = va_arg(f->args, int);
+	if(t >= nelem(astnames) || astnames[t] == nil)
+		return fmtprint(f, "%d", t);
+	return fmtprint(f, "%s", astnames[t]);
+}
+
+static int
+opfmt(Fmt *f)
+{
+	int t;
+	
+	t = va_arg(f->args, int);
+	if(t >= nelem(opnames) || opnames[t] == nil)
+		return fmtprint(f, "%d", t);
+	return fmtprint(f, "%s", opnames[t]);
+}
+
+static int
+clz(uvlong v)
+{
+	int n;
+	
+	n = 0;
+	if(v >> 32 == 0) {n += 32; v <<= 32;}
+	if(v >> 48 == 0) {n += 16; v <<= 16;}
+	if(v >> 56 == 0) {n += 8; v <<= 8;}
+	if(v >> 60 == 0) {n += 4; v <<= 4;}
+	if(v >> 62 == 0) {n += 2; v <<= 2;}
+	if(v >> 63 == 0) {n += 1; v <<= 1;}
+	return n;
+}
+
+static u64int
+hash(char *s)
+{
+	u64int h;
+	
+	h = 0xcbf29ce484222325ULL;
+	for(; *s != 0; s++){
+		h ^= *s;
+		h *= 0x100000001b3ULL;
+	}
+	return h;
+}
+
+static Symbol *
+trieget(uvlong hash)
+{
+	Trie **tp, *t, *s;
+	uvlong d;
+	
+	tp = &root;
+	for(;;){
+		t = *tp;
+		if(t == nil){
+			t = emalloc(sizeof(Symbol));
+			t->hash = hash;
+			t->l = 64;
+			*tp = t;
+			return (Symbol *) t;
+		}
+		d = (hash ^ t->hash) & -(1ULL<<64 - t->l);
+		if(d == 0 || t->l == 0){
+			if(t->l == 64)
+				return (Symbol *) t;
+			tp = &t->n[hash << t->l >> 64 - TRIEB];
+		}else{
+			s = emalloc(sizeof(Trie));
+			s->hash = hash;
+			s->l = clz(d) & -TRIEB;
+			s->n[t->hash << s->l >> 64 - TRIEB] = t;
+			*tp = s;
+			tp = &s->n[hash << s->l >> 64 - TRIEB];
+		}
+	}
+}
+
+Symbol *
+symget(char *name)
+{
+	uvlong h;
+	Symbol *s;
+	
+	h = hash(name);
+	while(s = trieget(h), s->name != nil && strcmp(s->name, name) != 0)
+		h++;
+	if(s->name == nil){
+		s->name = strdup(name);
+		*lastsymp = s;
+		lastsymp = &s->next;
+	}
+	return s;
+}
+
+void
+trieprint(Trie *t, char *pref, int bits)
+{
+	int i;
+
+	if(t == nil) {print("%snil\n", pref); return;}
+	if(t->l == 64) {print("%s%#.8p %.*llux '%s'\n", pref, t, (t->l - bits + 3) / 4, t->hash << bits >> bits >> 64 - t->l, ((Symbol*)t)->name); return;}
+	print("%s%#.8p %.*llux %d\n", pref, t, (t->l - bits + 3) / 4, t->hash << bits >> bits >> 64 - t->l, t->l);
+	for(i = 0; i < (1<<TRIEB); i++){
+		if(t->n[i] == nil) continue;
+		print("%s%x:\n", pref, i);
+		trieprint(t->n[i], smprint("\t%s", pref), t->l);
+	}
+}
+
+Node *
+node(int t, ...)
+{
+	Node *n;
+	va_list va;
+	extern Line line;
+	
+	n = emalloc(sizeof(Node));
+	n->type = t;
+	n->Line = line;
+	va_start(va, t);
+	switch(t){
+	case ASTSYM:
+		n->sym = va_arg(va, Symbol *);
+		break;
+	case ASTNUM:
+		n->num = va_arg(va, mpint *);
+		break;
+	case ASTBIN:
+		n->op = va_arg(va, int);
+		n->n1 = va_arg(va, Node *);
+		n->n2 = va_arg(va, Node *);
+		break;
+	case ASTUN:
+		n->op = va_arg(va, int);
+		n->n1 = va_arg(va, Node *);
+		break;
+	case ASTIDX:
+	case ASTTERN:
+		n->n1 = va_arg(va, Node *);
+		n->n2 = va_arg(va, Node *);
+		n->n3 = va_arg(va, Node *);
+		break;
+	case ASTTEMP:
+		break;
+	default:
+		sysfatal("node: unknown type %α", t);
+	}
+	va_end(va);
+	return n;
+}
+
+static int
+triedesc(Trie *t, int(*f)(Symbol *, va_list), va_list va)
+{
+	int i, rc;
+	
+	if(t == nil) return 0;
+	if(t->l == 64) return f((Symbol *) t, va);
+	rc = 0;
+	for(i = 0; i < 1<<TRIEB; i++)
+		rc += triedesc(t->n[i], f, va);
+	return rc;
+}
+
+void
+miscinit(void)
+{
+	fmtinstall(L'α', astfmt);
+	fmtinstall(L'O', opfmt);
+}
--- /dev/null
+++ b/sys/src/cmd/forp/mkfile
@@ -1,0 +1,14 @@
+</$objtype/mkfile
+
+BIN=/$objtype/bin
+TARG=forp
+OFILES=\
+	forp.$O\
+	parse.$O\
+	misc.$O\
+	cvt.$O\
+	logic.$O\
+
+HFILES=dat.h fns.h
+
+</sys/src/cmd/mkone
--- /dev/null
+++ b/sys/src/cmd/forp/parse.c
@@ -1,0 +1,454 @@
+#include <u.h>
+#include <libc.h>
+#include <bio.h>
+#include <ctype.h>
+#include <mp.h>
+#include "dat.h"
+#include "fns.h"
+
+Biobuf *bin;
+Line line;
+char lexbuf[512];
+int peektok;
+
+enum {
+	TEOF = -1,
+	TSYM = -2,
+	TNUM = -3,
+	TBIT = -4,
+	TOBVIOUSLY = -5,
+	TEQ = -6,
+	TNEQ = -7,
+	TLSH = -8,
+	TRSH = -9,
+	TLE = -10,
+	TGE = -11,
+	TLAND = -12,
+	TLOR = -13,
+	TASSUME = -14,
+	TIMP = -15,
+	TEQV = -16,
+	TSIGNED = -17,
+};
+
+typedef struct Keyword Keyword;
+typedef struct Oper Oper;
+struct Keyword {
+	char *name;
+	int tok;
+};
+/* both tables must be sorted */
+static Keyword kwtab[] = {
+	"assume", TASSUME,
+	"bit", TBIT,
+	"obviously", TOBVIOUSLY,
+	"signed", TSIGNED,
+};
+/* <=> is implemented through a hack below */
+static Keyword koptab[] = {
+	"!=", TNEQ,
+	"&&", TLAND,
+	"<<", TLSH,
+	"<=", TLE,
+	"==", TEQ,
+	"=>", TIMP,
+	">=", TGE,
+	">>", TRSH,
+	"||", TLOR,
+};
+static Keyword *kwjmp[128];
+static Keyword *kopjmp[128];
+struct Oper {
+	int tok;
+	int type;
+	int pred;
+	char *str;
+};
+#define MAXPREC 15
+static Oper optab[] = {
+	'*', OPMUL, 14, "*",
+	'/', OPDIV, 14, "/",
+	'%', OPMOD, 14, "%",
+	'+', OPADD, 13, "+",
+	'-', OPSUB, 13, "-",
+	TLSH, OPLSH, 12, "<<",
+	TRSH, OPRSH, 12, ">>",
+	'<', OPLT, 11, "<",
+	TLE, OPLE, 11, "<=",
+	'>', OPGT, 11, ">",
+	TGE, OPGE, 11, ">=",
+	TEQ, OPEQ, 10, "==",
+	TNEQ, OPNEQ, 10, "!=",
+	'&', OPAND, 9, "&",
+	'^', OPXOR, 8, "^",
+	'|', OPOR, 7, "|",
+	TLAND, OPLAND, 6, "&&",
+	TLOR, OPLOR, 5, "||",
+	TEQV, OPEQV, 4, "<=>",
+	TIMP, OPIMP, 4, "=>",
+	/* ?: */
+	'=', OPASS, 2, "=",
+	',', OPCOMMA, 1, ",",
+	-1, OPNOT, MAXPREC, "!",
+	-1, OPCOM, MAXPREC, "~",
+	-1, OPNEG, MAXPREC, "-",
+};
+
+void
+error(Line *l, char *msg, ...)
+{
+	char buf[256];
+	Fmt f;
+	va_list va;
+
+	if(l == nil) l = &line;
+	fmtfdinit(&f, 2, buf, sizeof(buf));
+	fmtprint(&f, "%s:%d: ", l->filen, l->lineno);
+	va_start(va, msg);
+	fmtvprint(&f, msg, va);
+	va_end(va);
+	fmtrune(&f, '\n');
+	fmtfdflush(&f);
+	exits("error");
+}
+
+static int
+tokfmt(Fmt *f)
+{
+	int t;
+	Keyword *k;
+	
+	t = va_arg(f->args, int);
+	if(t >= ' ' && t < 0x7f) return fmtprint(f, "%c", t);
+	for(k = kwtab; k < kwtab + nelem(kwtab); k++)
+		if(k->tok == t)
+			return fmtprint(f, "%s", k->name);
+	for(k = koptab; k < koptab + nelem(koptab); k++)
+		if(k->tok == t)
+			return fmtprint(f, "%s", k->name);
+	switch(t){
+	case TSYM: return fmtprint(f, "TSYM"); break;
+	case TNUM: return fmtprint(f, "TNUM"); break;
+	case TEOF: return fmtprint(f, "eof"); break;
+	default: return fmtprint(f, "%d", t); break;
+	}
+}
+
+static int
+exprfmt(Fmt *f)
+{
+	Node *n;
+	Oper *o;
+	int w;
+	
+	n = va_arg(f->args, Node *);
+	if(n == nil) return fmtprint(f, "nil");
+	switch(n->type){
+	case ASTSYM: return fmtprint(f, "%s", n->sym->name);
+	case ASTBIN:
+		for(o = optab; o < optab + nelem(optab); o++)
+			if(o->type == n->op)
+				break;
+		if(o == optab + nelem(optab)) return fmtprint(f, "[unknown operation %O]", n->op);
+		w = f->width;
+		if(w > o->pred) fmtrune(f, '(');
+		fmtprint(f, "%*ε %s %*ε", o->pred, n->n1, o->str, o->pred + 1, n->n2);
+		if(w > o->pred) fmtrune(f, ')');
+		return 0;
+	case ASTNUM: return fmtprint(f, "0x%B", n->num);
+	default: return fmtprint(f, "???(%α)", n->type);
+	}
+}
+
+static int
+issymchar(int c)
+{
+	return c >= 0 && (isalnum(c) || c == '_' || c >= 0x80);
+}
+
+static int
+lex(void)
+{
+	int c, d;
+	char *p;
+	Keyword *kw;
+
+	if(peektok != 0){
+		c = peektok;
+		peektok = 0;
+		return c;
+	}
+loop:
+	do{
+		c = Bgetc(bin);
+		if(c == '\n') line.lineno++;
+	}while(c >= 0 && isspace(c));
+	if(c < 0) return TEOF;
+	if(c == '/'){
+		c = Bgetc(bin);
+		if(c == '/'){
+			do
+				c = Bgetc(bin);
+			while(c >= 0 && c != '\n');
+			if(c < 0) return TEOF;
+			line.lineno++;
+			goto loop;
+		}else if(c == '*'){
+		s0:
+			c = Bgetc(bin);
+			if(c != '*') goto s0;
+		s1:
+			c = Bgetc(bin);
+			if(c == '*') goto s1;
+			if(c != '/') goto s0;
+			goto loop;
+		}else{
+			Bungetc(bin);
+			return '/';
+		}
+	}
+	if(isdigit(c)){
+		p = lexbuf;
+		*p++ = c;
+		while(c = Bgetc(bin), issymchar(c))
+			if(p < lexbuf + sizeof(lexbuf) - 1)
+				*p++ = c;
+		Bungetc(bin);
+		*p = 0;
+		strtol(lexbuf, &p, 0);
+		if(p == lexbuf || *p != 0)
+			error(nil, "invalid number %q", lexbuf);
+		return TNUM;
+	}
+	if(issymchar(c)){
+		p = lexbuf;
+		*p++ = c;
+		while(c = Bgetc(bin), issymchar(c))
+			if(p < lexbuf + sizeof(lexbuf) - 1)
+				*p++ = c;
+		Bungetc(bin);
+		*p = 0;
+		c = lexbuf[0];
+		if((signed char)c>= 0 && (kw = kwjmp[c], kw != nil))
+			for(; kw < kwtab + nelem(kwtab) && kw->name[0] == c; kw++)
+				if(strcmp(lexbuf, kw->name) == 0)
+					return kw->tok;
+		return TSYM;
+	}
+	if(kw = kopjmp[c], kw != nil){
+		d = Bgetc(bin);
+		for(; kw < koptab + nelem(koptab) && kw->name[0] == c; kw++)
+			if(kw->name[1] == d){
+				if(kw->tok == TLE){
+					c = Bgetc(bin);
+					if(c == '>')
+						return TEQV;
+					Bungetc(bin);
+				}
+				return kw->tok;
+			}
+		Bungetc(bin);
+	}
+	return c;
+}
+
+static void
+superman(int t)
+{
+	assert(peektok == 0);
+	peektok = t;
+}
+
+static int
+peek(void)
+{
+	if(peektok != 0) return peektok;
+	return peektok = lex();
+}
+
+static void
+expect(int t)
+{
+	int s;
+	
+	s = lex();
+	if(t != s)
+		error(nil, "expected %t, got %t", t, s);
+}
+
+static int
+got(int t)
+{
+	return peek() == t && (lex(), 1);
+}
+
+static Node *
+expr(int level)
+{
+	Node *a, *b, *c;
+	Oper *op;
+	Symbol *s;
+	mpint *num;
+	int t;
+	
+	if(level == MAXPREC+1){
+		switch(t = lex()){
+		case '~': return node(ASTUN, OPCOM, expr(level));
+		case '!': return node(ASTUN, OPNOT, expr(level));
+		case '+': return expr(level);
+		case '-': return node(ASTUN, OPNEG, expr(level));
+		case '(':
+			a = expr(0);
+			expect(')');
+			return a;
+		case TSYM:
+			s = symget(lexbuf);
+			switch(s->type){
+			case SYMNONE:
+				error(nil, "%#q undefined", s->name);
+			default:
+				error(nil, "%#q symbol type error", s->name);
+			case SYMBITS:
+				break;
+			}
+			return node(ASTSYM, s);
+		case TNUM:
+			num = strtomp(lexbuf, nil, 0, nil);
+			return node(ASTNUM, num);
+		default:
+			error(nil, "unexpected %t", t);
+		}
+	}else if(level == MAXPREC){
+		a = expr(level + 1);
+		if(got('[')){
+			b = expr(0);
+			if(got(':'))
+				c = expr(0);
+			else
+				c = nil;
+			expect(']');
+			a = node(ASTIDX, a, b, c);
+		}
+		return a;
+	}else if(level == 3){
+		a = expr(level + 1);
+		if(got('?')){
+			b = expr(level);
+			expect(':');
+			c = expr(level);
+			a = node(ASTTERN, a, b, c);
+		}
+		return a;
+	}
+	a = expr(level+1);
+	for(;;){
+		t = peek();
+		for(op = optab; op < optab + nelem(optab); op++)
+			if(op->tok == t && op->pred >= level)
+				break;
+		if(op == optab+nelem(optab)) return a;
+		lex();
+		a = node(ASTBIN, op->type, a, expr(level+1));
+	}
+}
+
+static void
+vardecl(void)
+{
+	Symbol *s;
+	int l, flags;
+
+	flags = 0;
+	for(;;)
+		switch(l = lex()){
+		case TBIT: if((flags & 1) != 0) goto err; flags |= 1; break;
+		case TSIGNED: if((flags & 2) != 0) goto err; flags |= 2; break;
+		default: superman(l); goto out;
+		}
+out:
+	do{
+		expect(TSYM);
+		s = symget(lexbuf);
+		if(s->type != SYMNONE) error(nil, "%#q redefined", s->name);
+		s->type = SYMBITS;
+		if((flags & 2) != 0)
+			s->flags |= SYMFSIGNED;
+		s->size = 1;
+		if(got('[')){
+			expect(TNUM);
+			s->type = SYMBITS;
+			s->size = strtol(lexbuf, nil, 0);
+			expect(']');
+		}
+		s->vars = emalloc(sizeof(int) * s->size);
+	}while(got(','));
+	expect(';');
+	return;
+err:	error(nil, "syntax error");
+}
+
+static int
+statement(void)
+{
+	Node *n;
+	int t;
+
+	switch(t=peek()){
+	case TEOF:
+		return 0;
+	case TBIT:
+	case TSIGNED:
+		vardecl();
+		break;
+	case TASSUME:
+	case TOBVIOUSLY:
+		lex();
+		n = expr(0);
+		expect(';');
+		convert(n, -1);
+		if(t == TASSUME)
+			assume(n);
+		else
+			obviously(n);
+		break;
+	case ';':
+		lex();
+		break;
+	default:
+		n = expr(0);
+		convert(n, -1);
+		expect(';');
+	}
+	return 1;
+}
+
+void
+parsinit(void)
+{
+	Keyword *k;
+
+	fmtinstall('t', tokfmt);
+	fmtinstall(L'ε', exprfmt);
+	for(k = kwtab; k < kwtab + nelem(kwtab); k++)
+		if(kwjmp[k->name[0]] == nil)
+			kwjmp[k->name[0]] = k;
+	for(k = koptab; k < koptab + nelem(koptab); k++)
+		if(kopjmp[k->name[0]] == nil)
+			kopjmp[k->name[0]] = k;
+}
+
+void
+parse(char *fn)
+{
+	if(fn == nil){
+		bin = Bfdopen(0, OREAD);
+		line.filen = "<stdin>";
+	}else{
+		bin = Bopen(fn, OREAD);
+		line.filen = strdup(fn);
+	}
+	if(bin == nil) sysfatal("open: %r");
+	line.lineno = 1;
+	while(statement())
+		;
+}