sys/src/cmd/sat.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <sat.h>
   4 #include <bio.h>
   5 #include <ctype.h>
   6
   7 typedef struct Trie Trie;
   8 typedef struct Var Var;
   9 Biobuf *bin, *bout;
  10
  11 struct Trie {
  12         u64int hash;
  13         Trie *c[2];
  14         uchar l;
  15 };
  16 struct Var {
  17         Trie trie;
  18         char *name;
  19         int n;
  20         Var *next;
  21 };
  22 Trie *root;
  23 Var *vlist, **vlistp = &vlist;
  24 int varctr;
  25
  26 static void*
  27 emalloc(ulong n)
  28 {
  29         void *v;
  30
  31         v = malloc(n);
  32         if(v == nil) sysfatal("malloc: %r");
  33         setmalloctag(v, getcallerpc(&n));
  34         memset(v, 0, n);
  35         return v;
  36 }
  37
  38 u64int
  39 hash(char *s)
  40 {
  41         u64int h;
  42
  43         h = 0xcbf29ce484222325ULL;
  44         for(; *s != 0; s++){
  45                 h ^= *s;
  46                 h *= 0x100000001b3ULL;
  47         }
  48         return h;
  49 }
  50
  51 int
  52 ctz(u64int d)
  53 {
  54         int r;
  55
  56         d &= -d;
  57         r = 0;
  58         if((int)d == 0) r += 32, d >>= 32;
  59         r += ((d & 0xffff0000) != 0) << 4;
  60         r += ((d & 0xff00ff00) != 0) << 3;
  61         r += ((d & 0xf0f0f0f0) != 0) << 2;
  62         r += ((d & 0xcccccccc) != 0) << 1;
  63         r += ((d & 0xaaaaaaaa) != 0);
  64         return r;
  65 }
  66
  67 Trie *
  68 trieget(u64int h)
  69 {
  70         Trie *t, *s, **tp;
  71         u64int d;
  72
  73         tp = &root;
  74         for(;;){
  75                 t = *tp;
  76                 if(t == nil){
  77                         t = emalloc(sizeof(Var));
  78                         t->hash = h;
  79                         t->l = 64;
  80                         *tp = t;
  81                         return t;
  82                 }
  83                 d = (h ^ t->hash) << 64 - t->l >> 64 - t->l;
  84                 if(d == 0 || t->l == 0){
  85                         if(t->l == 64)
  86                                 return t;
  87                         tp = &t->c[h >> t->l & 1];
  88                         continue;
  89                 }
  90                 s = emalloc(sizeof(Trie));
  91                 s->hash = h;
  92                 s->l = ctz(d);
  93                 s->c[t->hash >> s->l & 1] = t;
  94                 *tp = s;
  95                 tp = &s->c[h >> s->l & 1];
  96         }
  97 }
  98
  99 Var *
 100 varget(char *n)
 101 {
 102         Var *v, **vp;
 103
 104         v = (Var*) trieget(hash(n));
 105         if(v->name == nil){
 106         gotv:
 107                 v->name = strdup(n);
 108                 v->n = ++varctr;
 109                 *vlistp = v;
 110                 vlistp = &v->next;
 111                 return v;
 112         }
 113         if(strcmp(v->name, n) == 0)
 114                 return v;
 115         for(vp = (Var**)&v->trie.c[0]; (v = *vp) != nil; vp = (Var**)&v->trie.c[0])
 116                 if(strcmp(v->name, n) == 0)
 117                         return v;
 118         v = emalloc(sizeof(Var));
 119         *vp = v;
 120         goto gotv;
 121 }
 122
 123 static int
 124 isvarchar(int c)
 125 {
 126         return isalnum(c) || c == '_' || c == '-' || c >= 0x80;
 127 }
 128
 129 char lexbuf[512];
 130 enum { TEOF = -1, TVAR = -2 };
 131 int peektok;
 132
 133 int
 134 lex(void)
 135 {
 136         int c;
 137         char *p;
 138
 139         if(peektok != 0){
 140                 c = peektok;
 141                 peektok = 0;
 142                 return c;
 143         }
 144         do
 145                 c = Bgetc(bin);
 146         while(c >= 0 && isspace(c) && c != '\n');
 147         if(c == '#'){
 148                 do
 149                         c = Bgetc(bin);
 150                 while(c >= 0 && c != '\n');
 151                 if(c < 0) return TEOF;
 152                 c = Bgetc(bin);
 153         }
 154         if(c < 0) return TEOF;
 155         if(isvarchar(c)){
 156                 p = lexbuf;
 157                 *p++ = c;
 158                 while(c = Bgetc(bin), c >= 0 && isvarchar(c))
 159                         if(p < lexbuf + sizeof(lexbuf) - 1)
 160                                 *p++ = c;
 161                 *p = 0;
 162                 Bungetc(bin);
 163                 return TVAR;
 164         }
 165         return c;
 166 }
 167
 168 void
 169 superman(int t)
 170 {
 171         peektok = t;
 172 }
 173
 174 int
 175 clause(SATSolve *s)
 176 {
 177         int t;
 178         int n;
 179         int not, min, max;
 180         char *p;
 181         static int *clbuf, nclbuf;
 182
 183         n = 0;
 184         not = 1;
 185         min = -1;
 186         max = -1;
 187         for(;;)
 188                 switch(t = lex()){
 189                 case '[':
 190                         t = lex();
 191                         if(t == TVAR){
 192                                 min = strtol(lexbuf, &p, 10);
 193                                 if(p == lexbuf || *p != 0 || min < 0) goto syntax;
 194                                 t = lex();
 195                         }else
 196                                 min = 0;
 197                         if(t == ']'){
 198                                 max = min;
 199                                 break;
 200                         }
 201                         if(t != ',') goto syntax;
 202                         t = lex();
 203                         if(t == TVAR){
 204                                 max = strtol(lexbuf, &p, 10);
 205                                 if(p == lexbuf || *p != 0 || max < 0) goto syntax;
 206                                 t = lex();
 207                         }else
 208                                 max = -1;
 209                         if(t != ']') goto syntax;
 210                         break;
 211                 case TVAR:
 212                         if(n == nclbuf){
 213                                 clbuf = realloc(clbuf, (nclbuf + 32) * sizeof(int));
 214                                 nclbuf += 32;
 215                         }
 216                         clbuf[n++] = not * varget(lexbuf)->n;
 217                         not = 1;
 218                         break;
 219                 case '!':
 220                         not *= -1;
 221                         break;
 222                 case TEOF:
 223                 case '\n':
 224                 case ';':
 225                         goto out;
 226                 default:
 227                         sysfatal("unexpected token %d", t);
 228                 }
 229 out:
 230         if(n != 0)
 231                 if(min >= 0)
 232                         satrange1(s, clbuf, n, min, max< 0 ? n : max);
 233                 else
 234                         satadd1(s, clbuf, n);
 235         return t != TEOF;
 236 syntax:
 237         sysfatal("syntax error");
 238         return 0;
 239 }
 240
 241 int oneflag, multiflag;
 242
 243 void
 244 usage(void)
 245 {
 246         fprint(2, "usage: %s [-1m] [file]\n", argv0);
 247         exits("usage");
 248 }
 249
 250 void
 251 main(int argc, char **argv)
 252 {
 253         SATSolve *s;
 254         Var *v;
 255
 256         ARGBEGIN {
 257         case '1': oneflag++; break;
 258         case 'm': multiflag++; break;
 259         default: usage();
 260         } ARGEND;
 261
 262         switch(argc){
 263         case 0:
 264                 bin = Bfdopen(0, OREAD);
 265                 break;
 266         case 1:
 267                 bin = Bopen(argv[0], OREAD);
 268                 break;
 269         default: usage();
 270         }
 271         if(bin == nil) sysfatal("Bopen: %r");
 272         s = satnew();
 273         if(s == nil) sysfatal("satnew: %r");
 274         while(clause(s))
 275                 ;
 276         if(multiflag){
 277                 bout = Bfdopen(1, OWRITE);
 278                 while(satmore(s) > 0){
 279                         for(v = vlist; v != nil; v = v->next)
 280                                 if(satval(s, v->n) > 0)
 281                                         Bprint(bout, "%s ", v->name);
 282                         Bprint(bout, "\n");
 283                         Bflush(bout);
 284                 }
 285         }else if(oneflag){
 286                 if(satsolve(s) == 0)
 287                         exits("unsat");
 288                 bout = Bfdopen(1, OWRITE);
 289                 for(v = vlist; v != nil; v = v->next)
 290                         if(satval(s, v->n) > 0)
 291                                 Bprint(bout, "%s ", v->name);
 292                 Bprint(bout, "\n");
 293                 Bflush(bout);
 294         }else{
 295                 if(satsolve(s) == 0)
 296                         exits("unsat");
 297                 bout = Bfdopen(1, OWRITE);
 298                 for(v = vlist; v != nil; v = v->next)
 299                         Bprint(bout, "%s %d\n", v->name, satval(s, v->n));
 300                 Bflush(bout);
 301         }
 302         exits(nil);
 303 }