| /dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
| H A D | engine.cpp | 147 int previousDecisionLevel, int newDecisionLevel, RewindStyle rewindStyle, in rewindPaths() argument
153 nodepath.resize(decisionLevelTip[newDecisionLevel]); in rewindPaths()
154 altpath.resize(decisionLevelTip[newDecisionLevel]-1); in rewindPaths()
158 std::cerr << "rewinding to level " << newDecisionLevel << "\n"; in rewindPaths()
175 while (nodepath.size() > decisionLevelTip[newDecisionLevel]) { in rewindPaths()
231 inline void Engine::newDecisionLevel() { in newDecisionLevel() function in Engine
242 sat.newDecisionLevel(); in newDecisionLevel()
243 if (so.mip) mip->newDecisionLevel(); in newDecisionLevel()
779 newDecisionLevel(); in search()
870 newDecisionLevel(); in search()
|
| H A D | sat.h | 187 void newDecisionLevel();
211 inline void SAT::newDecisionLevel() { in newDecisionLevel() function
|
| H A D | engine.h | 78 void newDecisionLevel();
|
| /dports/math/chuffed/chuffed-e04bedd/chuffed/mip/ |
| H A D | mip.h | 68 void newDecisionLevel();
|
| H A D | mip.cpp | 113 void MIP::newDecisionLevel() { in newDecisionLevel() function in MIP
|
| /dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
| H A D | Solver.h | 160 …void newDecisionLevel (); // Begins a new…
245 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.C | 635 newDecisionLevel(); in search()
679 newDecisionLevel(); in search()
|
| /dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
| H A D | Solver.cpp | 682 newDecisionLevel(); in search()
703 newDecisionLevel(); in search()
780 newDecisionLevel(); in search()
801 newDecisionLevel(); in search()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
| H A D | Solver.h | 217 …void newDecisionLevel (); // Begins a new…
317 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cpp | 680 newDecisionLevel(); in search()
701 newDecisionLevel(); in search()
|
| /dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
| H A D | Solver.h | 243 …void newDecisionLevel (); // Begins a new…
346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cc | 774 newDecisionLevel(); in search()
795 newDecisionLevel(); in search()
|
| /dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
| H A D | Solver.h | 233 …void newDecisionLevel (); // Begins a new…
335 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| /dports/math/minisat/minisat-2.2.1/minisat/core/ |
| H A D | Solver.h | 243 …void newDecisionLevel (); // Begins a new…
346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cc | 768 newDecisionLevel(); in search()
789 newDecisionLevel(); in search()
|
| /dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
| H A D | Solver.h | 243 …void newDecisionLevel (); // Begins a new…
346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cc | 768 newDecisionLevel(); in search()
789 newDecisionLevel(); in search()
|
| /dports/math/vampire/vampire-4.5.1/Minisat/core/ |
| H A D | Solver.h | 249 …void newDecisionLevel (); // Begins a new…
352 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cc | 775 newDecisionLevel(); in search()
796 newDecisionLevel(); in search()
|
| /dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
| H A D | Solver.h | 304 …void newDecisionLevel (); // Begins a new…
440 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| H A D | Solver.cc | 1119 newDecisionLevel(); in search()
1154 newDecisionLevel(); in search()
|
| /dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
| H A D | Solver.h | 296 …void newDecisionLevel (); // Begins a new…
408 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| /dports/math/glucose/glucose-syrup-4.1/core/ |
| H A D | Solver.h | 402 …void newDecisionLevel (); // Begins a new…
518 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() function
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/core/ |
| H A D | Solver.h | 390 …void newDecisionLevel (); // Begins a new…
523 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); fli… in newDecisionLevel() function
|
| /dports/math/cvc4/CVC4-1.7/src/prop/minisat/ |
| H A D | CVC4-README | 37 Minisat pushes the scope in the newDecisionLevel() method where we appropriately
|