From 87df80019e3676583f2d60d500179ddcfabab584 Mon Sep 17 00:00:00 2001 From: aiju Date: Sun, 18 Mar 2018 03:03:12 +0000 Subject: [PATCH] add sat(1) command --- sys/src/cmd/sat.c | 303 ++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 303 insertions(+) create mode 100644 sys/src/cmd/sat.c diff --git a/sys/src/cmd/sat.c b/sys/src/cmd/sat.c new file mode 100644 index 000000000..0a0b940fe --- /dev/null +++ b/sys/src/cmd/sat.c @@ -0,0 +1,303 @@ +#include +#include +#include +#include +#include + +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); +}