Searched refs:nbclausesbeforereduce (Results 1 – 5 of 5) sorted by relevance
202 nbclausesbeforereduce = firstReduceDB; in Solver()290 nbclausesbeforereduce = s.nbclausesbeforereduce; in Solver()1260 …if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialIn… in reduceDB()1262 if(ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB; in reduceDB()1371 nbclausesbeforereduce = firstReduceDB; in adaptSolver()1372 curRestart = (conflicts / nbclausesbeforereduce) + 1; in adaptSolver()1616 (glureduce && conflicts >= ((unsigned int) curRestart * nbclausesbeforereduce))) { in search()1619 curRestart = (conflicts / nbclausesbeforereduce) + 1; in search()1622 nbclausesbeforereduce += incReduceDB; in search()1772 nbclausesbeforereduce, lbSizeMinimizingClause); in solve_()
361 int nbclausesbeforereduce; // To know when it is time to reduce clause database variable
157 nbclausesbeforereduce = firstReduceDB; in Solver()942 …if(ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd()<=3) nbclausesbeforereduce +=specialIncRe… in reduceDB()944 if(ca[learnts.last()].lbd()<=5) nbclausesbeforereduce +=specialIncReduceDB; in reduceDB()1127 if(conflicts>=curRestart* nbclausesbeforereduce) in search()1131 curRestart = (conflicts/ nbclausesbeforereduce)+1; in search()1133 nbclausesbeforereduce += incReduceDB; in search()1234 … | * size < %3d |\n",lbdQueue.maxSize(),nbclausesbeforereduce,lbSizeMini… in solve_()1473 nbclausesbeforereduce = firstReduceDB; in reset()
256 int nbclausesbeforereduce; // To know when it is time to reduce clause database variable
165 …if (ca[learnts[learnts.size() / RATIOREMOVECLAUSES]].lbd() <= 3) nbclausesbeforereduce += specialI… in reduceDB()167 if (ca[learnts.last()].lbd() <= 5) nbclausesbeforereduce += specialIncReduceDB; in reduceDB()