| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.h | 65 redBins(0) in ClausesStay()
70 redBins += other.redBins;
75 uint64_t redBins; variable
|
| H A D | completedetachreattacher.cpp | 55 assert(stay.redBins % 2 == 0);
56 solver->binTri.redBins = stay.redBins/2;
75 stay.redBins++;
|
| H A D | subsumeimplicit.cpp | 64 solver->binTri.redBins--; in try_subsume_bin()
|
| H A D | solver.cpp | 545 binTri.redBins++; in attach_bin_clause()
1704 && (binTri.irredBins + binTri.redBins) > 1 in check_reconfigure()
2873 + binTri.irredBins + binTri.redBins in verify_model()
2929 cout << " " << print_value_kilo_mega(binTri.redBins); in print_clause_stats()
2934 << ratio_for_stat(litStats.redLits + binTri.redBins*2 in print_clause_stats()
2935 , tot + binTri.redBins) in print_clause_stats()
3706 if (thisNumRedBins/2 != binTri.redBins) { in check_implicit_stats()
3711 << " binTri.redBins: " << binTri.redBins in check_implicit_stats()
3715 assert(thisNumRedBins/2 == binTri.redBins); in check_implicit_stats()
4385 binTri.redBins--; in detach_xor_clauses()
|
| H A D | comphandler.cpp | 527 solver->binTri.redBins--; in remove_bin_except_for_lit1()
632 solver->binTri.redBins -= numRemovedHalfRed/2; in moveClausesImplicit()
|
| H A D | xorfinder.cpp | 784 size_t origBins = solver->binTri.redBins; in add_new_truths_from_xors()
858 uint32_t num_bins_added = solver->binTri.redBins - origBins; in add_new_truths_from_xors()
|
| H A D | distillerlongwithimpl.cpp | 121 solver->binTri.redBins--; in subsume_clause_with_watch()
|
| H A D | clausecleaner.cpp | 262 solver->binTri.redBins -= remLBin/2; in update_solver_stats()
|
| H A D | solver.h | 223 binTri.redBins--;
|
| H A D | sqlitestats.cpp | 593 sqlite3_bind_int64(stmt, bindAt++, binTri.redBins); in restart()
915 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->binTri.redBins); in var_dist()
|
| H A D | cnf.h | 76 uint64_t redBins = 0; member
|
| H A D | searcher.cpp | 1910 && (binTri.irredBins + binTri.redBins) > 1 in check_calc_satzilla_features()
3227 solver->binTri.redBins--; in remove_useless_bins()
3444 f.put_uint64_t(binTri.redBins); in write_binary_cls()
3522 binTri.redBins =read_binary_cls(f, true); in load_state()
|
| H A D | subsumestrengthen.cpp | 965 solver->binTri.redBins--; in backw_sub_str_long_with_bins_watch()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | completedetachreattacher.h | 65 redBins(0) in ClausesStay()
70 redBins += other.redBins;
75 uint64_t redBins; variable
|
| H A D | completedetachreattacher.cpp | 55 assert(stay.redBins % 2 == 0); in detach_nonbins_nontris()
56 solver->binTri.redBins = stay.redBins/2; in detach_nonbins_nontris()
75 stay.redBins++; in clearWatchNotBinNotTri()
|
| H A D | subsumeimplicit.cpp | 64 solver->binTri.redBins--; in try_subsume_bin()
|
| H A D | solver.cpp | 545 binTri.redBins++; in attach_bin_clause()
1704 && (binTri.irredBins + binTri.redBins) > 1 in check_reconfigure()
2873 + binTri.irredBins + binTri.redBins in verify_model()
2929 cout << " " << print_value_kilo_mega(binTri.redBins); in print_clause_stats()
2934 << ratio_for_stat(litStats.redLits + binTri.redBins*2 in print_clause_stats()
2935 , tot + binTri.redBins) in print_clause_stats()
3706 if (thisNumRedBins/2 != binTri.redBins) { in check_implicit_stats()
3711 << " binTri.redBins: " << binTri.redBins in check_implicit_stats()
3715 assert(thisNumRedBins/2 == binTri.redBins); in check_implicit_stats()
4385 binTri.redBins--; in detach_xor_clauses()
|
| H A D | comphandler.cpp | 527 solver->binTri.redBins--; in remove_bin_except_for_lit1()
632 solver->binTri.redBins -= numRemovedHalfRed/2; in moveClausesImplicit()
|
| H A D | xorfinder.cpp | 784 size_t origBins = solver->binTri.redBins; in add_new_truths_from_xors()
858 uint32_t num_bins_added = solver->binTri.redBins - origBins; in add_new_truths_from_xors()
|
| H A D | distillerlongwithimpl.cpp | 121 solver->binTri.redBins--; in subsume_clause_with_watch()
|
| H A D | clausecleaner.cpp | 262 solver->binTri.redBins -= remLBin/2; in update_solver_stats()
|
| H A D | solver.h | 223 binTri.redBins--;
|
| H A D | sqlitestats.cpp | 593 sqlite3_bind_int64(stmt, bindAt++, binTri.redBins); in restart()
915 sqlite3_bind_int64(stmt_var_dist, bindAt++, solver->binTri.redBins); in var_dist()
|
| H A D | cnf.h | 76 uint64_t redBins = 0; member
|
| H A D | searcher.cpp | 1910 && (binTri.irredBins + binTri.redBins) > 1 in check_calc_satzilla_features()
3227 solver->binTri.redBins--; in remove_useless_bins()
3444 f.put_uint64_t(binTri.redBins); in write_binary_cls()
3522 binTri.redBins =read_binary_cls(f, true); in load_state()
|