Searched refs:get_lit_replaced_with (Results 1 – 10 of 10) sorted by relevance
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | varreplacer.cpp | 164 lit = get_lit_replaced_with(lit); in enqueueDelayedEnqueue()
903 const Lit lit1 = get_lit_replaced_with(Lit(var1, false)); in replace()
904 const Lit lit2 = get_lit_replaced_with(Lit(var2, false)) ^ xor_is_true; in replace()
995 const Lit repLit = get_lit_replaced_with(Lit(i, false)); in checkUnsetSanity()
1006 << get_lit_replaced_with(Lit(i, false)) in checkUnsetSanity()
1008 << solver->value(get_lit_replaced_with(Lit(i, false))) in checkUnsetSanity()
1248 fast_inter_replace_lookup.push_back(get_lit_replaced_with(Lit(var, false))); in build_fast_inter_replace_lookup()
1258 Lit VarReplacer::get_lit_replaced_with(Lit lit) const in get_lit_replaced_with() function in VarReplacer
|
| H A D | varreplacer.h | 69 Lit get_lit_replaced_with(Lit lit) const;
|
| H A D | solutionextender_old-cpp | 364 toSet = solver->varReplacer->get_lit_replaced_with(toSet);
383 Lit tmp = solver->varReplacer->get_lit_replaced_with(lit);
|
| H A D | solver.cpp | 639 const Lit updated_lit = varReplacer->get_lit_replaced_with(lit); in addClauseHelper()
691 const Lit updated_lit = varReplacer->get_lit_replaced_with(lit); in addClauseHelper()
2748 lit = varReplacer->get_lit_replaced_with(lit); in get_zero_assigned_lits()
2765 assert(varReplacer->get_lit_replaced_with(tmp_lit).var() == lit.var()); in get_zero_assigned_lits()
2766 if (lit != varReplacer->get_lit_replaced_with(tmp_lit)) { in get_zero_assigned_lits()
2769 assert(lit == varReplacer->get_lit_replaced_with(tmp_lit)); in get_zero_assigned_lits()
|
| H A D | datasync.cpp | 223 assert(solver->varReplacer->get_lit_replaced_with(lit) == lit); in syncBinFromOthers()
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | varreplacer.cpp | 164 lit = get_lit_replaced_with(lit); in enqueueDelayedEnqueue()
903 const Lit lit1 = get_lit_replaced_with(Lit(var1, false)); in replace()
904 const Lit lit2 = get_lit_replaced_with(Lit(var2, false)) ^ xor_is_true; in replace()
995 const Lit repLit = get_lit_replaced_with(Lit(i, false)); in checkUnsetSanity()
1006 << get_lit_replaced_with(Lit(i, false)) in checkUnsetSanity()
1008 << solver->value(get_lit_replaced_with(Lit(i, false))) in checkUnsetSanity()
1248 fast_inter_replace_lookup.push_back(get_lit_replaced_with(Lit(var, false))); in build_fast_inter_replace_lookup()
1258 Lit VarReplacer::get_lit_replaced_with(Lit lit) const in get_lit_replaced_with() function in VarReplacer
|
| H A D | varreplacer.h | 69 Lit get_lit_replaced_with(Lit lit) const;
|
| H A D | solutionextender_old-cpp | 364 toSet = solver->varReplacer->get_lit_replaced_with(toSet);
383 Lit tmp = solver->varReplacer->get_lit_replaced_with(lit);
|
| H A D | solver.cpp | 639 const Lit updated_lit = varReplacer->get_lit_replaced_with(lit); in addClauseHelper()
691 const Lit updated_lit = varReplacer->get_lit_replaced_with(lit); in addClauseHelper()
2748 lit = varReplacer->get_lit_replaced_with(lit); in get_zero_assigned_lits()
2765 assert(varReplacer->get_lit_replaced_with(tmp_lit).var() == lit.var()); in get_zero_assigned_lits()
2766 if (lit != varReplacer->get_lit_replaced_with(tmp_lit)) { in get_zero_assigned_lits()
2769 assert(lit == varReplacer->get_lit_replaced_with(tmp_lit)); in get_zero_assigned_lits()
|
| H A D | datasync.cpp | 223 assert(solver->varReplacer->get_lit_replaced_with(lit) == lit); in syncBinFromOthers()
|