ref: 87df80019e3676583f2d60d500179ddcfabab584
parent: d68417bc01ef1258e707d95d4785c189fcad5834
author: aiju <devnull@localhost>
date: Sat Mar 17 23:03:12 EDT 2018
add sat(1) command
--- /dev/null
+++ b/sys/src/cmd/sat.c
@@ -1,0 +1,303 @@
+#include <u.h>
+#include <libc.h>
+#include <sat.h>
+#include <bio.h>
+#include <ctype.h>
+
+typedef struct Trie Trie;
+typedef struct Var Var;
+Biobuf *bin, *bout;
+
+struct Trie {+ u64int hash;
+ Trie *c[2];
+ uchar l;
+};
+struct Var {+ Trie trie;
+ char *name;
+ int n;
+ Var *next;
+};
+Trie *root;
+Var *vlist, **vlistp = &vlist;
+int varctr;
+
+static void*
+emalloc(ulong n)
+{+ void *v;
+
+ v = malloc(n);
+ if(v == nil) sysfatal("malloc: %r");+ setmalloctag(v, getcallerpc(&n));
+ memset(v, 0, n);
+ return v;
+}
+
+u64int
+hash(char *s)
+{+ u64int h;
+
+ h = 0xcbf29ce484222325ULL;
+ for(; *s != 0; s++){+ h ^= *s;
+ h *= 0x100000001b3ULL;
+ }
+ return h;
+}
+
+int
+ctz(u64int d)
+{+ int r;
+
+ d &= -d;
+ r = 0;
+ if((int)d == 0) r += 32, d >>= 32;
+ r += ((d & 0xffff0000) != 0) << 4;
+ r += ((d & 0xff00ff00) != 0) << 3;
+ r += ((d & 0xf0f0f0f0) != 0) << 2;
+ r += ((d & 0xcccccccc) != 0) << 1;
+ r += ((d & 0xaaaaaaaa) != 0);
+ return r;
+}
+
+Trie *
+trieget(u64int h)
+{+ Trie *t, *s, **tp;
+ u64int d;
+
+ tp = &root;
+ for(;;){+ t = *tp;
+ if(t == nil){+ t = emalloc(sizeof(Var));
+ t->hash = h;
+ t->l = 64;
+ *tp = t;
+ return t;
+ }
+ d = (h ^ t->hash) << 64 - t->l >> 64 - t->l;
+ if(d == 0 || t->l == 0){+ if(t->l == 64)
+ return t;
+ tp = &t->c[h >> t->l & 1];
+ continue;
+ }
+ s = emalloc(sizeof(Trie));
+ s->hash = h;
+ s->l = ctz(d);
+ s->c[t->hash >> s->l & 1] = t;
+ *tp = s;
+ tp = &s->c[h >> s->l & 1];
+ }
+}
+
+Var *
+varget(char *n)
+{+ Var *v, **vp;
+
+ v = (Var*) trieget(hash(n));
+ if(v->name == nil){+ gotv:
+ v->name = strdup(n);
+ v->n = ++varctr;
+ *vlistp = v;
+ vlistp = &v->next;
+ return v;
+ }
+ if(strcmp(v->name, n) == 0)
+ return v;
+ for(vp = (Var**)&v->trie.c[0]; (v = *vp) != nil; vp = (Var**)&v->trie.c[0])
+ if(strcmp(v->name, n) == 0)
+ return v;
+ v = emalloc(sizeof(Var));
+ *vp = v;
+ goto gotv;
+}
+
+static int
+isvarchar(int c)
+{+ return isalnum(c) || c == '_' || c == '-' || c >= 0x80;
+}
+
+char lexbuf[512];
+enum { TEOF = -1, TVAR = -2 };+int peektok;
+
+int
+lex(void)
+{+ int c;
+ char *p;
+
+ if(peektok != 0){+ c = peektok;
+ peektok = 0;
+ return c;
+ }
+ do
+ c = Bgetc(bin);
+ while(c >= 0 && isspace(c) && c != '\n');
+ if(c == '#'){+ do
+ c = Bgetc(bin);
+ while(c >= 0 && c != '\n');
+ if(c < 0) return TEOF;
+ c = Bgetc(bin);
+ }
+ if(c < 0) return TEOF;
+ if(isvarchar(c)){+ p = lexbuf;
+ *p++ = c;
+ while(c = Bgetc(bin), c >= 0 && isvarchar(c))
+ if(p < lexbuf + sizeof(lexbuf) - 1)
+ *p++ = c;
+ *p = 0;
+ Bungetc(bin);
+ return TVAR;
+ }
+ return c;
+}
+
+void
+superman(int t)
+{+ peektok = t;
+}
+
+int
+clause(SATSolve *s)
+{+ int t;
+ int n;
+ int not, min, max;
+ char *p;
+ static int *clbuf, nclbuf;
+
+ n = 0;
+ not = 1;
+ min = -1;
+ max = -1;
+ for(;;)
+ switch(t = lex()){+ case '[':
+ t = lex();
+ if(t == TVAR){+ min = strtol(lexbuf, &p, 10);
+ if(p == lexbuf || *p != 0 || min < 0) goto syntax;
+ t = lex();
+ }else
+ min = 0;
+ if(t == ']'){+ max = min;
+ break;
+ }
+ if(t != ',') goto syntax;
+ t = lex();
+ if(t == TVAR){+ max = strtol(lexbuf, &p, 10);
+ if(p == lexbuf || *p != 0 || max < 0) goto syntax;
+ t = lex();
+ }else
+ max = -1;
+ if(t != ']') goto syntax;
+ break;
+ case TVAR:
+ if(n == nclbuf){+ clbuf = realloc(clbuf, (nclbuf + 32) * sizeof(int));
+ nclbuf += 32;
+ }
+ clbuf[n++] = not * varget(lexbuf)->n;
+ not = 1;
+ break;
+ case '!':
+ not *= -1;
+ break;
+ case TEOF:
+ case '\n':
+ case ';':
+ goto out;
+ default:
+ sysfatal("unexpected token %d", t);+ }
+out:
+ if(n != 0)
+ if(min >= 0)
+ satrange1(s, clbuf, n, min, max< 0 ? n : max);
+ else
+ satadd1(s, clbuf, n);
+ return t != TEOF;
+syntax:
+ sysfatal("syntax error");+ return 0;
+}
+
+int oneflag, multiflag;
+
+void
+usage(void)
+{+ fprint(2, "usage: %s [-1m] [file]\n", argv0);
+ exits("usage");+}
+
+void
+main(int argc, char **argv)
+{+ SATSolve *s;
+ Var *v;
+
+ ARGBEGIN {+ case '1': oneflag++; break;
+ case 'm': multiflag++; break;
+ default: usage();
+ } ARGEND;
+
+ switch(argc){+ case 0:
+ bin = Bfdopen(0, OREAD);
+ break;
+ case 1:
+ bin = Bopen(argv[0], OREAD);
+ break;
+ default: usage();
+ }
+ if(bin == nil) sysfatal("Bopen: %r");+ s = satnew();
+ if(s == nil) sysfatal("satnew: %r");+ while(clause(s))
+ ;
+ if(multiflag){ + bout = Bfdopen(1, OWRITE);
+ while(satmore(s) > 0){+ for(v = vlist; v != nil; v = v->next)
+ if(satval(s, v->n) > 0)
+ Bprint(bout, "%s ", v->name);
+ Bprint(bout, "\n");
+ Bflush(bout);
+ }
+ }else if(oneflag){+ if(satsolve(s) == 0)
+ exits("unsat");+ bout = Bfdopen(1, OWRITE);
+ for(v = vlist; v != nil; v = v->next)
+ if(satval(s, v->n) > 0)
+ Bprint(bout, "%s ", v->name);
+ Bprint(bout, "\n");
+ Bflush(bout);
+ }else{+ if(satsolve(s) == 0)
+ exits("unsat");+ bout = Bfdopen(1, OWRITE);
+ for(v = vlist; v != nil; v = v->next)
+ Bprint(bout, "%s %d\n", v->name, satval(s, v->n));
+ Bflush(bout);
+ }
+ exits(nil);
+}