sys/src/libsat/satget.c

   1 #include <u.h>
   2 #include <libc.h>
   3 #include <sat.h>
   4 #include "impl.h"
   5
   6 int
   7 satget(SATSolve *s, int i, int *t, int n)
   8 {
   9         SATClause *c;
  10         SATLit *l;
  11         int j, k;
  12
  13         for(c = s->cl; c != s->learncl; c = c->next)
  14                 if(i-- == 0){
  15                         for(j = 0; j < n && j < c->n; j++)
  16                                 t[j] = signf(c->l[j]);
  17                         return c->n;
  18                 }
  19         for(l = s->lit; l < s->lit + 2 * s->nvar; l++)
  20                 for(k = 0; k < l->nbimp; k++)
  21                         if(i-- == 0){
  22                                 if(n > 0) t[0] = -signf(l - s->lit);
  23                                 if(n > 1) t[1] = signf(l->bimp[k]);
  24                                 return 2;
  25                         }
  26         for(; c != 0; c = c->next)
  27                 if(i-- == 0){
  28                         for(j = 0; j < n && j < c->n; j++)
  29                                 t[j] = signf(c->l[j]);
  30                         return c->n;
  31                 }
  32         return -1;
  33 }