| /dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
| H A D | Solver.C | 248 void Solver::analyze(Clause* confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
257 out_btlevel = 0; in analyze()
276 if (level[var(q)] > out_btlevel) in analyze()
277 out_btlevel = level[var(q)]; in analyze()
321 out_btlevel = 0; in analyze()
330 out_btlevel = level[var(p)]; in analyze()
|
| H A D | Solver.h | 165 …void analyze (Clause* confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
| H A D | Solver.cpp | 264 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
341 out_btlevel = 0; in analyze()
352 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 222 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
| H A D | Solver.cpp | 266 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
343 out_btlevel = 0; in analyze()
354 out_btlevel = level(var(pNew)); in analyze()
|
| /dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
| H A D | Solver.cc | 302 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
375 out_btlevel = 0; in analyze()
386 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 248 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/math/minisat/minisat-2.2.1/minisat/core/ |
| H A D | Solver.cc | 296 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
369 out_btlevel = 0; in analyze()
380 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 248 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
| H A D | Solver.cc | 296 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
369 out_btlevel = 0; in analyze()
380 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 248 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/math/vampire/vampire-4.5.1/Minisat/core/ |
| H A D | Solver.cc | 301 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
374 out_btlevel = 0; in analyze()
385 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 254 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|
| /dports/math/cvc3/cvc3-2.4.1/src/sat/ |
| H A D | minisat_solver.h | 443 Clause* analyze(int& out_btlevel);
|
| H A D | minisat_solver.cpp | 1091 Clause* Solver::analyze(int& out_btlevel) { in analyze() argument
1155 out_btlevel = 0; in analyze()
1209 out_btlevel = max(out_btlevel, getLevel(q)); in analyze()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.cc | 416 void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip) in analyze() argument
533 out_btlevel = 0; in analyze()
545 out_btlevel = level(var(p)); in analyze()
|
| H A D | Solver.h | 315 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip = UIP_FIRST…
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | Glucose.cpp | 529 void Solver::analyze(CRef confl, vec<Lit>& out_learnt,vec<Lit>&selectors, int& out_btlevel,unsigned… in analyze() argument
657 out_btlevel = 0; in analyze()
668 out_btlevel = level(var(p)); in analyze()
|
| /dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | searcher.h | 272 , uint32_t& out_btlevel //backtrack level
|
| H A D | searcher.cpp | 770 , uint32_t& out_btlevel in analyze_conflict() argument
840 out_btlevel = find_backtrack_level_of_learnt(); in analyze_conflict()
845 if ((int32_t)varData[var].level >= (int32_t)out_btlevel-1) { in analyze_conflict()
1006 , uint32_t& out_btlevel
1011 , uint32_t& out_btlevel
|
| /dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
| H A D | searcher.h | 272 , uint32_t& out_btlevel //backtrack level
|
| H A D | searcher.cpp | 770 , uint32_t& out_btlevel in analyze_conflict() argument
840 out_btlevel = find_backtrack_level_of_learnt(); in analyze_conflict()
845 if ((int32_t)varData[var].level >= (int32_t)out_btlevel-1) { in analyze_conflict()
1006 , uint32_t& out_btlevel
1011 , uint32_t& out_btlevel
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.cc | 698 int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel) in analyze() argument
822 out_btlevel = 0; in analyze()
833 out_btlevel = level(var(p)); in analyze()
|
| /dports/math/glucose/glucose-syrup-4.1/core/ |
| H A D | Solver.cc | 735 void Solver::analyze(CRef confl, vec <Lit> &out_learnt, vec <Lit> &selectors, int &out_btlevel, uns… in analyze() argument
881 out_btlevel = 0; in analyze()
892 out_btlevel = level(var(p)); in analyze()
|
| /dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
| H A D | Solver.h | 238 …void analyze (CRef confl, vec<Lit>& out_learnt, int& out_btlevel); // (bt = backtr…
|