#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);
}

You are viewing proxied material from sdf.org. The copyright of proxied material belongs to its original authors. Any comments or complaints in relation to proxied material should be directed to the original authors of the content concerned. Please see the disclaimer for more details.