sys/src/cmd/forp/forp.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <mp.h>
   4 #include <sat.h>
   5 #include "dat.h"
   6 #include "fns.h"
   7
   8 extern SATSolve *sat;
   9 extern int *assertvar, nassertvar;
  10
  11 int
  12 printval(Symbol *s, Fmt *f)
  13 {
  14         int i;
  15
  16         if(s->type != SYMBITS) return 0;
  17         fmtprint(f, "%s = ", s->name);
  18         for(i = s->size - 1; i >= 0; i--)
  19                 switch(satval(sat, s->vars[i])){
  20                 case 1: fmtrune(f, '1'); break;
  21                 case 0: fmtrune(f, '0'); break;
  22                 case -1: fmtrune(f, '?'); break;
  23                 default: abort();
  24                 }
  25         fmtprint(f, "\n");
  26         return 0;
  27 }
  28
  29 void
  30 debugsat(void)
  31 {
  32         int i, j, rc;
  33         int *t;
  34         int ta;
  35         Fmt f;
  36         char buf[256];
  37
  38         ta = 0;
  39         t = nil;
  40         fmtfdinit(&f, 1, buf, 256);
  41         for(i = 0;;){
  42                 rc = satget(sat, i, t, ta);
  43                 if(rc < 0) break;
  44                 if(rc > ta){
  45                         ta = rc;
  46                         t = realloc(t, ta * sizeof(int));
  47                         continue;
  48                 }
  49                 i++;
  50                 fmtprint(&f, "%d: ", i);
  51                 for(j = 0; j < rc; j++)
  52                         fmtprint(&f, "%s%d", j==0?"":" ∨ ", t[j]);
  53                 fmtprint(&f, "\n");
  54         }
  55         free(t);
  56         fmtfdflush(&f);
  57 }
  58
  59 void
  60 tabheader(Fmt *f)
  61 {
  62         Symbol *s;
  63         int l, first;
  64
  65         first = 0;
  66         for(s = syms; s != nil; s = s->next){
  67                 if(s->type != SYMBITS) continue;
  68                 l = strlen(s->name);
  69                 if(s->size > l) l = s->size;
  70                 fmtprint(f, "%s%*s", first++ != 0 ? " " : "", l, s->name);
  71         }
  72         fmtrune(f, '\n');
  73 }
  74
  75 void
  76 tabrow(Fmt *f)
  77 {
  78         Symbol *s;
  79         int i, l, first;
  80
  81         first = 0;
  82         for(s = syms; s != nil; s = s->next){
  83                 if(s->type != SYMBITS) continue;
  84                 if(first++ != 0) fmtrune(f, ' ');
  85                 l = strlen(s->name);
  86                 if(s->size > l) l = s->size;
  87                 for(i = l - 1; i > s->size - 1; i--)
  88                         fmtrune(f, ' ');
  89                 for(; i >= 0; i--)
  90                         switch(satval(sat, s->vars[i])){
  91                         case 1: fmtrune(f, '1'); break;
  92                         case 0: fmtrune(f, '0'); break;
  93                         case -1: fmtrune(f, '?'); break;
  94                         default: abort();
  95                         }
  96         }
  97         fmtrune(f, '\n');
  98 }
  99
 100 void
 101 go(int mflag)
 102 {
 103         Fmt f;
 104         char buf[256];
 105         Symbol *s;
 106
 107         if(nassertvar == 0)
 108                 sysfatal("left as an exercise to the reader");
 109         satadd1(sat, assertvar, nassertvar);
 110 //      debugsat();
 111         if(mflag){
 112                 fmtfdinit(&f, 1, buf, sizeof(buf));
 113                 tabheader(&f);
 114                 fmtfdflush(&f);
 115                 while(satmore(sat) > 0){
 116                         tabrow(&f);
 117                         fmtfdflush(&f);
 118                 }
 119         }else{
 120                 if(satsolve(sat) == 0)
 121                         print("Proved.\n");
 122                 else{
 123                         fmtfdinit(&f, 1, buf, sizeof(buf));
 124                         for(s = syms; s != nil; s = s->next)
 125                                 printval(s, &f);
 126                         fmtfdflush(&f);
 127                 }
 128         }
 129 }
 130
 131 void
 132 usage(void)
 133 {
 134         fprint(2, "usage: %s [ -m ] [ file ]\n", argv0);
 135         exits("usage");
 136 }
 137
 138 void
 139 main(int argc, char **argv)
 140 {
 141         typedef void init(void);
 142         init miscinit, cvtinit, parsinit;
 143         static int mflag;
 144
 145         ARGBEGIN{
 146         case 'm': mflag++; break;
 147         default: usage();
 148         }ARGEND;
 149
 150         if(argc > 1) usage();
 151
 152         quotefmtinstall();
 153         fmtinstall('B', mpfmt);
 154         miscinit();
 155         cvtinit();
 156         parsinit();
 157         parse(argc > 0 ? argv[0] : nil);
 158         go(mflag);
 159 }