sys/src/libsat/debug.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <sat.h>
   4 #include "impl.h"
   5
   6 static SATSolve *globsat;
   7
   8 static int
   9 satclausefmt(Fmt *f)
  10 {
  11         SATClause *c;
  12         char *s;
  13         int i, fl;
  14
  15         fl = f->flags;
  16         c = va_arg(f->args, SATClause *);
  17         if(c == nil)
  18                 return fmtstrcpy(f, "Λ");
  19         if(c->n == 0)
  20                 return fmtstrcpy(f, "ε");
  21         s = "%s%d";
  22         for(i = 0; i < c->n; i++){
  23                 if((fl & FmtSign) != 0)
  24                         switch(globsat->lit[c->l[i]].val){
  25                         case 1: s = "%s[%d]"; break;
  26                         case 0: s = "%s(%d)"; break;
  27                         case -1: s = "%s%d"; break;
  28                         default: abort();
  29                         }
  30                 fmtprint(f, s, i != 0 ? " ∨ " : "", signf(c->l[i]));
  31         }
  32         return 0;
  33 }
  34
  35 void
  36 satprintstate(SATSolve *s)
  37 {
  38         int i;
  39         Fmt f;
  40         char buf[512];
  41         SATVar *v;
  42
  43         fmtfdinit(&f, 1, buf, sizeof(buf));
  44         fmtprint(&f, "trail:\n");
  45         for(i = 0; i < s->ntrail; i++){
  46                 v = &s->var[VAR(s->trail[i])];
  47                 fmtprint(&f, "%c%-8d %- 8d %-8d ", i == s->forptr ? '*' : ' ', i, signf(s->trail[i]), v->lvl);
  48                 if(v->isbinreason)
  49                         fmtprint(&f, "%d ∨ %d\n", signf(s->trail[i]), signf(v->binreason));
  50                 else
  51                         fmtprint(&f, "%+Γ\n", v->reason);
  52         }
  53         fmtrune(&f, '\n');
  54         fmtfdflush(&f);
  55 }
  56
  57 void
  58 satsanity(SATSolve *s)
  59 {
  60         int i, j, k, m, tl, s0, s1;
  61         SATVar *v;
  62         SATLit *l;
  63         SATClause *c;
  64
  65         for(c = s->cl; c != nil; c = c->next){
  66                 assert(c->n >= 2);
  67                 assert((uint)((uchar*)c->next - (uchar*)c) >= sizeof(SATClause) + (c->n - 1) * sizeof(int));
  68                 for(j = 0; j < c->n; j++)
  69                         assert((uint)c->l[j] < 2*s->nvar);
  70                 for(i = 0; i < 2; i++)
  71                         c->watch[i] = (void*)((uintptr)c->watch[i] | 1);
  72         }
  73         for(i = 0; i < s->nvar; i++){
  74                 tl = -1;
  75                 for(j = 0; j < s->ntrail; j++)
  76                         if(VAR(s->trail[j]) == i){
  77                                 assert(tl == -1);
  78                                 tl = j;
  79                         }
  80                 v = &s->var[i];
  81                 l = &s->lit[2*i];
  82                 if(l->val >= 0){
  83                         assert(l->val <= 1);
  84                         assert(l[0].val + l[1].val == 1);
  85                         assert((uint)v->lvl <= s->lvl);
  86                         assert(tl != -1);
  87                         assert(s->trail[tl] == 2*i+l[1].val);
  88                         assert(tl >= s->decbd[v->lvl]);
  89                         assert(v->lvl == s->lvl || tl < s->decbd[v->lvl+1]);
  90                 }else{
  91                         assert(l[0].val == -1 && l[1].val == -1);
  92                         assert(v->lvl == -1);
  93                         assert(v->heaploc >= 0);
  94                         assert(tl == -1);
  95                 }
  96                 assert(v->heaploc == -1 || (uint)v->heaploc <= s->nheap && s->heap[v->heaploc] == v);
  97                 for(j = 0; j < 2; j++){
  98                         m = 2 * i + j;
  99                         for(c = l[j].watch; c != nil; c = c->watch[k]){
 100                                 k = c->l[1] == m;
 101                                 assert(k || c->l[0] == m);
 102                                 assert((uintptr)c->watch[k] & 1);
 103                                 c->watch[k] = (void*)((uintptr)c->watch[k] & ~1);
 104                         }
 105                 }
 106         }
 107         for(c = s->cl; c != nil; c = c->next)
 108                 for(i = 0; i < 2; i++)
 109                         assert(((uintptr)c->watch[i] & 1) == 0);
 110         if(s->forptr == s->ntrail)
 111                 for(c = s->cl; c != nil; c = c->next){
 112                         s0 = s->lit[c->l[0]].val;
 113                         s1 = s->lit[c->l[1]].val;
 114                         if(s0 != 0 && s1 != 0 || s0 == 1 || s1 == 1)
 115                                 continue;
 116                         for(i = 2; i < c->n; i++)
 117                                 if(s->lit[c->l[i]].val != 0){
 118                                         satprintstate(s);
 119                                         print("watchlist error: %+Γ\n", c);
 120                                         assert(0);
 121                                 }
 122                 }
 123 }
 124
 125 void
 126 satdebuginit(SATSolve *s)
 127 {
 128         globsat = s;
 129         fmtinstall(L'Γ', satclausefmt);
 130 }