Cross Reference: /pkg/src/modules/solver/solver.c

Lines Matching refs:values
173     lbool* values = s->assigns;
179         if (values[next] == l_Undef)
224         if (values[next] == l_Undef)
345     lbool* values = s->assigns;
352         if (values[lit_var(lits[i])] == sig)
402     lbool* values = s->assigns;
404     lbool  val    = values[v];
420         values [v] = sig;
444     lbool*   values;  
453     values  = s->assigns;
459         values [x] = l_Undef;
490     lbool*  values = s->assigns;
497         if (values[i] != l_Undef)
689     lbool*  values = s->assigns;
734                 if (values[lit_var(lits[0])] == sig){
742                         if (values[lit_var(*k)] != sig){
868                 lbool* values = s->assigns;
870                 for (i = 0; i < s->size; i++) veci_push(&s->model,(int)values[i]);
1077     lbool* values;
1095     values = s->assigns;
1100         //printf("lit: "L_LIT", value = %d\n", L_lit(*i), (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]));
1102         if (*i == lit_neg(last) || sig == values[lit_var(*i)])
1104         else if (*i != last && values[lit_var(*i)] == l_Undef)
1168     lbool*  values        = s->assigns;
1173         switch (lit_sign(*i) ? -values[lit_var(*i)] : values[lit_var(*i)]){