add sat(1) command

This commit is contained in:
aiju 2018-03-18 03:03:12 +00:00
parent d68417bc01
commit 87df80019e

303
sys/src/cmd/sat.c Normal file
View file

@ -0,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);
}