add swiss german kbmap (thanks mike)

[plan9front.git] / sys / src / libsat / satget.c

diff --git a/sys/src/libsat/satget.c b/sys/src/libsat/satget.c
index 2643111355975060b2aa54c3cb7bd1b693b617b4..ae5f5ccecb62e20ba9949ffc8aea7ef0a34ff760 100644 (file)
--- a/sys/src/libsat/satget.c
+++ b/sys/src/libsat/satget.c
@@ -8,7 +8,7 @@ satget(SATSolve *s, int i, int *t, int n)
 {
        SATClause *c;
        SATLit *l;
-       int j, k;
+       int j, k, m;
        
        for(c = s->cl; c != s->learncl; c = c->next)
                if(i-- == 0){
@@ -18,11 +18,17 @@ satget(SATSolve *s, int i, int *t, int n)
                }
        for(l = s->lit; l < s->lit + 2 * s->nvar; l++)
                for(k = 0; k < l->nbimp; k++)
-                       if(i-- == 0){
+                       if(l - s->lit < l->bimp[k] && 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++)