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