| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.cpp | 52 solver->litStats.redLits = 0;
144 solver->litStats.redLits -= cl->size();
|
| H A D | clausecleaner.cpp | 165 solver->litStats.redLits -= origSize; in clean_clauses_inter()
241 solver->litStats.redLits -= i-j; in clean_clause()
|
| H A D | subsumestrengthen.cpp | 71 solver->litStats.redLits -= cl.size(); in subsume_and_unlink_and_markirred()
180 solver->litStats.redLits -= cl.size(); in strengthen_subsume_and_unlink_and_markirred()
582 solver->litStats.redLits--; in remove_literal()
|
| H A D | solver.cpp | 502 litStats.redLits += ps.size(); in add_clause_int()
524 litStats.redLits += cl.size(); in attachClause()
578 litStats.redLits -= origSize; in detach_modified_clause()
2932 << ratio_for_stat(litStats.redLits, tot) in print_clause_stats()
2934 << ratio_for_stat(litStats.redLits + binTri.redBins*2 in print_clause_stats()
3750 if (numLitsRed != litStats.redLits) { in check_stats()
3753 << "->litStats.redLits: " << litStats.redLits << endl; in check_stats()
3755 assert(numLitsRed == litStats.redLits); in check_stats()
4447 litStats.redLits -= cl->size(); in detach_xor_clauses()
|
| H A D | reducedb.cpp | 523 solver->litStats.redLits -= cl->size(); in handle_lev2_predictor()
781 solver->litStats.redLits -= cl->size(); in remove_cl_from_lev2()
|
| H A D | distillerlong.cpp | 204 if (solver->litStats.irredLits + solver->litStats.redLits < in distill_long_cls_all()
|
| H A D | varreplacer.cpp | 605 solver->litStats.redLits -= origSize; in handleUpdatedClause()
664 solver->litStats.redLits += c.size(); in handleUpdatedClause()
|
| H A D | cnf.h | 82 uint64_t redLits = 0; member
|
| H A D | occsimplifier.cpp | 314 solver->litStats.redLits -= cl.size(); in unlink_clause()
366 solver->litStats.redLits -= i-j; in clean_clause()
436 solver->litStats.redLits -= cl.size(); in complete_clean_clause()
625 solver->litStats.redLits -= cl->size(); in add_back_to_solver()
|
| H A D | sqlitestats.cpp | 597 sqlite3_bind_int64(stmt, bindAt++, solver->litStats.redLits); in restart()
|
| H A D | searcher.cpp | 2146 simpDB_props = (litStats.redLits + litStats.irredLits)<<5; in clean_clauses_if_needed()
3431 litStats.redLits += cl->size(); in read_long_cls()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.cpp | 52 solver->litStats.redLits = 0; in detach_nonbins_nontris()
144 solver->litStats.redLits -= cl->size(); in cleanAndAttachClauses()
|
| H A D | clausecleaner.cpp | 165 solver->litStats.redLits -= origSize; in clean_clauses_inter()
241 solver->litStats.redLits -= i-j; in clean_clause()
|
| H A D | subsumestrengthen.cpp | 71 solver->litStats.redLits -= cl.size(); in subsume_and_unlink_and_markirred()
180 solver->litStats.redLits -= cl.size(); in strengthen_subsume_and_unlink_and_markirred()
582 solver->litStats.redLits--; in remove_literal()
|
| H A D | solver.cpp | 502 litStats.redLits += ps.size(); in add_clause_int()
524 litStats.redLits += cl.size(); in attachClause()
578 litStats.redLits -= origSize; in detach_modified_clause()
2932 << ratio_for_stat(litStats.redLits, tot) in print_clause_stats()
2934 << ratio_for_stat(litStats.redLits + binTri.redBins*2 in print_clause_stats()
3750 if (numLitsRed != litStats.redLits) { in check_stats()
3753 << "->litStats.redLits: " << litStats.redLits << endl; in check_stats()
3755 assert(numLitsRed == litStats.redLits); in check_stats()
4447 litStats.redLits -= cl->size(); in detach_xor_clauses()
|
| H A D | reducedb.cpp | 523 solver->litStats.redLits -= cl->size(); in handle_lev2_predictor()
781 solver->litStats.redLits -= cl->size(); in remove_cl_from_lev2()
|
| H A D | distillerlong.cpp | 204 if (solver->litStats.irredLits + solver->litStats.redLits < in distill_long_cls_all()
|
| H A D | varreplacer.cpp | 605 solver->litStats.redLits -= origSize; in handleUpdatedClause()
664 solver->litStats.redLits += c.size(); in handleUpdatedClause()
|
| H A D | cnf.h | 82 uint64_t redLits = 0; member
|
| H A D | occsimplifier.cpp | 314 solver->litStats.redLits -= cl.size(); in unlink_clause()
366 solver->litStats.redLits -= i-j; in clean_clause()
436 solver->litStats.redLits -= cl.size(); in complete_clean_clause()
625 solver->litStats.redLits -= cl->size(); in add_back_to_solver()
|
| H A D | sqlitestats.cpp | 597 sqlite3_bind_int64(stmt, bindAt++, solver->litStats.redLits); in restart()
|
| H A D | searcher.cpp | 2146 simpDB_props = (litStats.redLits + litStats.irredLits)<<5; in clean_clauses_if_needed()
3431 litStats.redLits += cl->size(); in read_long_cls()
|