| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.cc | 593 void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) { in analyzeFinal2() argument
598 out_conflict.clear(); in analyzeFinal2()
614 out_conflict.push(~trail[i]); in analyzeFinal2()
640 assert (out_conflict.size()); in analyzeFinal2()
652 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
654 out_conflict.clear(); in analyzeFinal()
656 out_conflict.push(p); in analyzeFinal()
683 out_conflict.push(~trail[i]); in analyzeFinal()
711 assert (out_conflict.size()); in analyzeFinal()
|
| H A D | Solver.h | 316 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
317 void analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict);
|
| /dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
| H A D | Solver.C | 378 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
380 out_conflict.clear(); in analyzeFinal()
381 out_conflict.push(p); in analyzeFinal()
393 out_conflict.push(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 166 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | searcher.cpp | 1039 out_conflict.clear(); in analyze_final_confl_with_assumptions()
1040 out_conflict.push_back(p); in analyze_final_confl_with_assumptions()
1061 out_conflict.push_back(~trail[i].lit); in analyze_final_confl_with_assumptions()
1107 learnt_clause = out_conflict; in analyze_final_confl_with_assumptions()
1109 out_conflict = learnt_clause; in analyze_final_confl_with_assumptions()
1125 std::sort(out_conflict.begin(), out_conflict.end()); in update_assump_conflict_to_orig_outside()
1126 assert(out_conflict.size() <= assumptions.size()); in update_assump_conflict_to_orig_outside()
1138 for(size_t i = 0; i < out_conflict.size(); i++) { in update_assump_conflict_to_orig_outside()
1139 Lit lit = out_conflict[i]; in update_assump_conflict_to_orig_outside()
1153 out_conflict[j++] = ~inter_assumptions[at_assump].lit_orig_outside; in update_assump_conflict_to_orig_outside()
[all …]
|
| H A D | searcher.h | 262 void update_assump_conflict_to_orig_outside(vector<Lit>& out_conflict);
289 void analyze_final_confl_with_assumptions(const Lit p, vector<Lit>& out_conflict);
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | searcher.cpp | 1039 out_conflict.clear(); in analyze_final_confl_with_assumptions()
1040 out_conflict.push_back(p); in analyze_final_confl_with_assumptions()
1061 out_conflict.push_back(~trail[i].lit); in analyze_final_confl_with_assumptions()
1107 learnt_clause = out_conflict; in analyze_final_confl_with_assumptions()
1109 out_conflict = learnt_clause; in analyze_final_confl_with_assumptions()
1125 std::sort(out_conflict.begin(), out_conflict.end()); in update_assump_conflict_to_orig_outside()
1126 assert(out_conflict.size() <= assumptions.size()); in update_assump_conflict_to_orig_outside()
1138 for(size_t i = 0; i < out_conflict.size(); i++) { in update_assump_conflict_to_orig_outside()
1139 Lit lit = out_conflict[i]; in update_assump_conflict_to_orig_outside()
1153 out_conflict[j++] = ~inter_assumptions[at_assump].lit_orig_outside; in update_assump_conflict_to_orig_outside()
[all …]
|
| H A D | searcher.h | 262 void update_assump_conflict_to_orig_outside(vector<Lit>& out_conflict);
289 void analyze_final_confl_with_assumptions(const Lit p, vector<Lit>& out_conflict);
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
| H A D | Solver.cpp | 399 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
401 out_conflict.clear(); in analyzeFinal()
402 out_conflict.push(p); in analyzeFinal()
414 out_conflict.push(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 223 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
|
| /dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
| H A D | Solver.cpp | 401 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
403 out_conflict.clear(); in analyzeFinal()
404 out_conflict.push(p); in analyzeFinal()
416 out_conflict.push(~trail[i]); in analyzeFinal()
|
| /dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
| H A D | Solver.cc | 462 void Solver::analyzeFinal(Lit p, LSet& out_conflict) in analyzeFinal() argument
464 out_conflict.clear(); in analyzeFinal()
465 out_conflict.insert(p); in analyzeFinal()
477 out_conflict.insert(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 249 …void analyzeFinal (Lit p, LSet& out_conflict); // COULD THIS B…
|
| /dports/math/minisat/minisat-2.2.1/minisat/core/ |
| H A D | Solver.cc | 456 void Solver::analyzeFinal(Lit p, LSet& out_conflict) in analyzeFinal() argument
458 out_conflict.clear(); in analyzeFinal()
459 out_conflict.insert(p); in analyzeFinal()
471 out_conflict.insert(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 249 …void analyzeFinal (Lit p, LSet& out_conflict); // COULD THIS B…
|
| /dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
| H A D | Solver.cc | 456 void Solver::analyzeFinal(Lit p, LSet& out_conflict) in analyzeFinal() argument
458 out_conflict.clear(); in analyzeFinal()
459 out_conflict.insert(p); in analyzeFinal()
471 out_conflict.insert(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 249 …void analyzeFinal (Lit p, LSet& out_conflict); // COULD THIS B…
|
| /dports/math/vampire/vampire-4.5.1/Minisat/core/ |
| H A D | Solver.cc | 461 void Solver::analyzeFinal(Lit p, LSet& out_conflict) in analyzeFinal() argument
463 out_conflict.clear(); in analyzeFinal()
464 out_conflict.insert(p); in analyzeFinal()
476 out_conflict.insert(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 255 …void analyzeFinal (Lit p, LSet& out_conflict); // COULD THIS B…
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | Glucose.cpp | 749 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
751 out_conflict.clear(); in analyzeFinal()
752 out_conflict.push(p); in analyzeFinal()
764 out_conflict.push(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 302 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.cc | 888 void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict) in analyzeFinal() argument
890 out_conflict.clear(); in analyzeFinal()
891 out_conflict.push(p); in analyzeFinal()
903 out_conflict.push(~trail[i]); in analyzeFinal()
|
| /dports/math/glucose/glucose-syrup-4.1/core/ |
| H A D | Solver.cc | 972 void Solver::analyzeFinal(Lit p, vec <Lit> &out_conflict) { in analyzeFinal() argument
973 out_conflict.clear(); in analyzeFinal()
974 out_conflict.push(p); in analyzeFinal()
986 out_conflict.push(~trail[i]); in analyzeFinal()
|
| H A D | Solver.h | 409 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
|
| /dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
| H A D | Solver.h | 239 …void analyzeFinal (Lit p, vec<Lit>& out_conflict); // COULD THIS B…
|