]> git.lizzy.rs Git - plan9front.git/blob - sys/src/libsat/satget.c
port: sync two longjmp fixes from drawterm
[plan9front.git] / 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, m;
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(l - s->lit < l->bimp[k] && 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         m = s->lvl == 0 ? s->ntrail : s->decbd[1];
27         for(k = 0; k < m; k++)
28                 if(i-- == 0){
29                         if(n > 0) t[0] = signf(s->trail[k]);
30                         return 1;
31                 }
32         for(; c != 0; c = c->next)
33                 if(i-- == 0){
34                         for(j = 0; j < n && j < c->n; j++)
35                                 t[j] = signf(c->l[j]);
36                         return c->n;
37                 }
38         return -1;
39 }