Lines Matching refs:learnts
159 sort(learnts, reduceDBAct_lt(ca)); in reduceDB()
161 sort(learnts, reduceDB_lt(ca)); in reduceDB()
165 …if (ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialI… in reduceDB()
167 if (ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB; in reduceDB()
173 limit = learnts.size() / 2; in reduceDB()
180 for (i = j = 0; i < learnts.size(); i++) { in reduceDB()
182 Clause& c = ca[learnts[i]]; in reduceDB()
183 if (i == learnts.size() / 2) in reduceDB()
187 removeClause(learnts[i]); in reduceDB()
193 learnts[j++] = learnts[i]; in reduceDB()
196 learnts.shrink(i - j); in reduceDB()
198 if (learnts.size() > 0) in reduceDB()
199 goodlimitsize = 1 + (double) sumsize / (double) learnts.size(); in reduceDB()
203 limit = unaryWatchedClauses.size() - (learnts.size() * (chanseokStrategy?4:2)); in reduceDB()
260 …tarts,(int)decisions,(int)conflicts,(int)stats[originalClausesSeen],(int)learnts.size(),(int)stats… in reportProgress()
361 learnts.push(cr); in parallelImportClauses()