| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | clausedumper.cpp | 275 tmpCl[0] = solver->map_inter_to_outer(tmpCl[0]); in dump_bin_cls()
276 tmpCl[1] = solver->map_inter_to_outer(tmpCl[1]); in dump_bin_cls()
|
| H A D | cnf.h | 253 uint32_t map_inter_to_outer(const uint32_t inter) const in map_inter_to_outer() function
257 Lit map_inter_to_outer(const Lit lit) const in map_inter_to_outer() function
269 void map_inter_to_outer(vector<Lit>& lits) const in map_inter_to_outer() function
|
| H A D | varreplacer.cpp | 945 const Lit lit1_outer = solver->map_inter_to_outer(lit1); in replace()
946 const Lit lit2_outer = solver->map_inter_to_outer(lit2); in replace()
1260 lit = solver->map_inter_to_outer(lit); in get_lit_replaced_with()
1267 var = solver->map_inter_to_outer(var); in get_var_replaced_with()
1275 var = solver->map_inter_to_outer(var); in get_vars_replacing()
|
| H A D | comphandler.cpp | 359 uint32_t outerVar = solver->map_inter_to_outer(var); in save_solution_to_savedstate()
384 const uint32_t outer = solver->map_inter_to_outer(lit.var()); in move_decision_level_zero_vars_here()
663 solver->map_inter_to_outer(lit) in saveClause()
|
| H A D | vardistgen.cpp | 136 uint32_t outer_var = solver->map_inter_to_outer(i); in dump()
|
| H A D | cms_breakid.cpp | 323 from = solver->map_inter_to_outer(from); in get_outer_permutations()
324 to = solver->map_inter_to_outer(to); in get_outer_permutations()
|
| H A D | solver.h | 476 tmpCl.push_back(map_inter_to_outer(cl[i])); in clause_outer_numbered()
487 tmpXor.push_back(map_inter_to_outer(cl[i])); in xor_outer_numbered()
|
| H A D | datasync.cpp | 382 lit1 = solver->map_inter_to_outer(lit1); in signalNewBinClause()
384 lit2 = solver->map_inter_to_outer(lit2); in signalNewBinClause()
|
| H A D | cnf.cpp | 791 uint32_t outer = map_inter_to_outer(i); in get_outside_var_incidence()
835 uint32_t outer = map_inter_to_outer(i); in get_outside_var_incidence_also_red()
|
| H A D | solver.cpp | 351 var = map_inter_to_outer(var); in sort_and_clean_clause()
1199 const Lit outer_lit = map_inter_to_outer(inter_lit); in set_assumptions()
1212 Lit outer_lit = map_inter_to_outer(assump); in add_assumption()
2751 lits.push_back(map_inter_to_outer(lit)); in get_zero_assigned_lits()
2772 lits.push_back(map_inter_to_outer(tmp_lit)); in get_zero_assigned_lits()
3638 uint32_t outer_var = map_inter_to_outer(var); in parse_v_line()
4230 uint32_t outer = map_inter_to_outer(i); in get_vsids_scores()
4300 l = map_inter_to_outer(l); in implied_by()
|
| H A D | occsimplifier.cpp | 217 const uint32_t outer = solver->map_inter_to_outer(i); in extend_model()
1895 var = solver->map_inter_to_outer(var); in uneliminate()
2277 solver->map_inter_to_outer(lits_outer); in add_clause_to_blck()
2661 << solver->map_inter_to_outer(lit) in set_var_as_eliminated()
2672 blkcls.push_back(solver->map_inter_to_outer(lit)); in create_dummy_blocked_clause()
|
| H A D | propengine.cpp | 664 uint64_t outer_var = map_inter_to_outer(v); in sql_dump_vardata_picktime()
|
| H A D | solutionextender_old-cpp | 334 << solver->map_inter_to_outer(blockedOn.var()) + 1
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | clausedumper.cpp | 275 tmpCl[0] = solver->map_inter_to_outer(tmpCl[0]); in dump_bin_cls()
276 tmpCl[1] = solver->map_inter_to_outer(tmpCl[1]); in dump_bin_cls()
|
| H A D | cnf.h | 253 uint32_t map_inter_to_outer(const uint32_t inter) const in map_inter_to_outer() function
257 Lit map_inter_to_outer(const Lit lit) const in map_inter_to_outer() function
269 void map_inter_to_outer(vector<Lit>& lits) const in map_inter_to_outer() function
|
| H A D | varreplacer.cpp | 945 const Lit lit1_outer = solver->map_inter_to_outer(lit1); in replace()
946 const Lit lit2_outer = solver->map_inter_to_outer(lit2); in replace()
1260 lit = solver->map_inter_to_outer(lit); in get_lit_replaced_with()
1267 var = solver->map_inter_to_outer(var); in get_var_replaced_with()
1275 var = solver->map_inter_to_outer(var); in get_vars_replacing()
|
| H A D | comphandler.cpp | 359 uint32_t outerVar = solver->map_inter_to_outer(var); in save_solution_to_savedstate()
384 const uint32_t outer = solver->map_inter_to_outer(lit.var()); in move_decision_level_zero_vars_here()
663 solver->map_inter_to_outer(lit) in saveClause()
|
| H A D | vardistgen.cpp | 136 uint32_t outer_var = solver->map_inter_to_outer(i); in dump()
|
| H A D | cms_breakid.cpp | 323 from = solver->map_inter_to_outer(from); in get_outer_permutations()
324 to = solver->map_inter_to_outer(to); in get_outer_permutations()
|
| H A D | solver.h | 476 tmpCl.push_back(map_inter_to_outer(cl[i])); in clause_outer_numbered()
487 tmpXor.push_back(map_inter_to_outer(cl[i])); in xor_outer_numbered()
|
| H A D | datasync.cpp | 382 lit1 = solver->map_inter_to_outer(lit1); in signalNewBinClause()
384 lit2 = solver->map_inter_to_outer(lit2); in signalNewBinClause()
|
| H A D | cnf.cpp | 791 uint32_t outer = map_inter_to_outer(i); in get_outside_var_incidence()
835 uint32_t outer = map_inter_to_outer(i); in get_outside_var_incidence_also_red()
|
| H A D | solver.cpp | 351 var = map_inter_to_outer(var); in sort_and_clean_clause()
1199 const Lit outer_lit = map_inter_to_outer(inter_lit); in set_assumptions()
1212 Lit outer_lit = map_inter_to_outer(assump); in add_assumption()
2751 lits.push_back(map_inter_to_outer(lit)); in get_zero_assigned_lits()
2772 lits.push_back(map_inter_to_outer(tmp_lit)); in get_zero_assigned_lits()
3638 uint32_t outer_var = map_inter_to_outer(var); in parse_v_line()
4230 uint32_t outer = map_inter_to_outer(i); in get_vsids_scores()
4300 l = map_inter_to_outer(l); in implied_by()
|
| H A D | occsimplifier.cpp | 217 const uint32_t outer = solver->map_inter_to_outer(i); in extend_model()
1895 var = solver->map_inter_to_outer(var); in uneliminate()
2277 solver->map_inter_to_outer(lits_outer); in add_clause_to_blck()
2661 << solver->map_inter_to_outer(lit) in set_var_as_eliminated()
2672 blkcls.push_back(solver->map_inter_to_outer(lit)); in create_dummy_blocked_clause()
|
| H A D | propengine.cpp | 664 uint64_t outer_var = map_inter_to_outer(v); in sql_dump_vardata_picktime()
|