Lines Matching defs:cls
470 static void solver_record(solver* s, veci* cls)
472 lit* begin = veci_begin(cls);
473 lit* end = begin + veci_size(cls);
474 clause* c = (veci_size(cls) > 1) ? clause_new(s,begin,end,1) : (clause*)0;
477 assert(veci_size(cls) > 0);
483 s->stats.learnts_literals += veci_size(cls);
1142 clause** cls = (clause**)vecp_begin(cs);
1146 if (reasons[lit_var(*clause_begin(cls[i]))] != cls[i] &&
1147 clause_simplify(s,cls[i]) == l_True)
1148 clause_remove(s,cls[i]);
1150 cls[j++] = cls[i];