/dports/math/chuffed/chuffed-e04bedd/chuffed/core/ |
H A D | sat.h | 192 …bool isRootLevel(int v) const { return engine.trail_lim.size()==0 || trailpos[v] < engine.trail_li… in isRootLevel() 193 bool isCurLevel(int v) const { return trailpos[v] >= engine.trail_lim.last(); } in isCurLevel() 195 for (int i = engine.trail_lim.size(); i--; ) { in getLevel() 196 if (trailpos[v] >= engine.trail_lim[i]) in getLevel()
|
H A D | engine.h | 60 vec<int> trail_lim; variable 107 int decisionLevel() const { return trail_lim.size(); } in decisionLevel() 110 for (int i = trail_lim.size(); i--; ) if (tp >= trail_lim[i]) return i+1; in tpToLevel()
|
/dports/math/ogdf/OGDF/src/ogdf/lib/minisat/core/ |
H A D | Solver.cpp | 209 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 212 if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) in cancelUntil() 215 qhead = trail_lim[level]; in cancelUntil() 216 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 217 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 411 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 656 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 754 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 823 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 824 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate()
|
/dports/math/py-cryptominisat/cryptominisat-5.8.0/src/ |
H A D | propengine.h | 179 …vector<uint32_t> trail_lim; ///< Separator indices for different decision levels in 'tra… variable 256 mem += trail_lim.capacity()*sizeof(uint32_t); in mem_used() 285 trail_lim.push_back(trail.size()); in new_decision_level() 287 cout << "New decision level: " << trail_lim.size() << endl; in new_decision_level() 293 return trail_lim.size(); in decisionLevel() 306 return trail_lim[0]; in getTrailSize()
|
/dports/math/cryptominisat/cryptominisat-5.8.0/src/ |
H A D | propengine.h | 179 …vector<uint32_t> trail_lim; ///< Separator indices for different decision levels in 'tra… variable 256 mem += trail_lim.capacity()*sizeof(uint32_t); in mem_used() 285 trail_lim.push_back(trail.size()); in new_decision_level() 287 cout << "New decision level: " << trail_lim.size() << endl; in new_decision_level() 293 return trail_lim.size(); in decisionLevel() 306 return trail_lim[0]; in getTrailSize()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat2/ |
H A D | Solver.cpp | 209 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 212 if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) in cancelUntil() 215 qhead = trail_lim[level]; in cancelUntil() 216 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 217 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 409 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 654 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 714 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 715 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate()
|
H A D | Solver.h | 183 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 317 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 319 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 329 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars()
|
/dports/cad/yosys/yosys-yosys-0.12/libs/minisat/ |
H A D | Solver.cc | 239 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 242 if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) in cancelUntil() 245 qhead = trail_lim[level]; in cancelUntil() 246 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 247 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 472 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 748 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 808 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 809 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() 895 trail_lim.push(trail.size()); in implies()
|
H A D | Solver.h | 193 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 348 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 359 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars() 394 return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); } in trailEnd()
|
/dports/math/minisat/minisat-2.2.1/minisat/core/ |
H A D | Solver.cc | 233 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 236 if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) in cancelUntil() 239 qhead = trail_lim[level]; in cancelUntil() 240 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 241 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 466 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 742 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 802 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 803 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() 889 trail_lim.push(trail.size()); in implies()
|
H A D | Solver.h | 193 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 348 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 359 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars() 394 return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); } in trailEnd()
|
/dports/textproc/link-grammar/link-grammar-5.8.0/link-grammar/minisat/minisat/core/ |
H A D | Solver.cc | 233 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 236 if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) in cancelUntil() 239 qhead = trail_lim[level]; in cancelUntil() 240 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 241 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 466 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 742 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 802 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 803 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() 889 trail_lim.push(trail.size()); in implies()
|
H A D | Solver.h | 193 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 346 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 348 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 359 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars() 394 return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); } in trailEnd()
|
/dports/math/vampire/vampire-4.5.1/Minisat/core/ |
H A D | Solver.cc | 238 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 241 if (phase_saving > 1 || (phase_saving == 1 && c > trail_lim.last())) in cancelUntil() 244 qhead = trail_lim[level]; in cancelUntil() 245 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 246 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 471 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 747 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 809 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 810 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() 896 trail_lim.push(trail.size()); in implies()
|
H A D | Solver.h | 199 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 352 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 354 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 365 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars() 401 return TrailIterator(&trail[decisionLevel() == 0 ? trail.size() : trail_lim[0]]); } in trailEnd()
|
/dports/lang/yap/yap-6.2.2/packages/swi-minisat2/C/ |
H A D | Solver.C | 180 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 184 qhead = trail_lim[level]; in cancelUntil() 185 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 186 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 388 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 692 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 693 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate()
|
H A D | Solver.h | 136 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 245 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 247 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel()
|
/dports/math/cvc4/CVC4-1.7/src/prop/bvminisat/core/ |
H A D | Solver.cc | 356 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 361 || ((phase_saving == 1) && c > trail_lim.last())) in cancelUntil() 366 qhead = trail_lim[level]; in cancelUntil() 367 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 368 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 605 int end = options::proof() ? 0 : trail_lim[0]; in analyzeFinal2() 673 int end = options::proof() ? 0 : trail_lim[0]; in analyzeFinal() 1071 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 1167 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 1168 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() [all …]
|
H A D | Solver.h | 267 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 440 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 442 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 452 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/glucose/ |
H A D | Glucose.cpp | 473 for (int c = trail.size()-1; c >= trail_lim[level]; c--){ in cancelUntil() 476 if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) in cancelUntil() 479 qhead = trail_lim[level]; in cancelUntil() 480 trail.shrink(trail.size() - trail_lim[level]); in cancelUntil() 481 trail_lim.shrink(trail_lim.size() - level); in cancelUntil() 759 for (int i = trail.size()-1; i >= trail_lim[0]; i--){ in analyzeFinal() 1058 …(int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]), nClauses(), (int)clauses_li… in search() 1178 int beg = i == 0 ? 0 : trail_lim[i - 1]; in progressEstimate() 1179 int end = i == decisionLevel() ? trail.size() : trail_lim[i]; in progressEstimate() 1489 trail_lim.clear(false); in reset()
|
H A D | Solver.h | 238 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 408 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 410 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 420 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars()
|
/dports/math/ogdf/OGDF/include/ogdf/lib/minisat/core/ |
H A D | Solver.h | 199 …vec<int> trail_lim; // Separator indices for different decision levels in 'trail… variable 335 inline void Solver::newDecisionLevel() { trail_lim.push(trail.size()); } in newDecisionLevel() 337 inline int Solver::decisionLevel () const { return trail_lim.size(); } in decisionLevel() 347 …eVars () const { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_l… in nFreeVars()
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/bsat/ |
H A D | satSolver3.c | 638 veci_push(&s->trail_lim,s->qtail); in sat_solver3_decision() 651 assert( veci_size(&s->trail_lim) > 0 ); in sat_solver3_canceluntil() 653 lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; in sat_solver3_canceluntil() 674 veci_resize(&s->trail_lim,level); in sat_solver3_canceluntil() 853 …start = (s->root_level >= veci_size(&s->trail_lim))? s->qtail-1 : (veci_begin(&s->trail_lim))[s->r… in sat_solver3_analyze_final() 1126 veci_new(&s->trail_lim); in sat_solver3_new() 1191 veci_new(&s->trail_lim); in zsat_solver3_new_seed() 1315 veci_delete(&s->trail_lim); in sat_solver3_delete() 1360 veci_resize(&s->trail_lim, 0); in sat_solver3_restart() 1406 veci_resize(&s->trail_lim, 0); in zsat_solver3_restart_seed() [all …]
|
H A D | satSolver2.c | 131 assert( level < veci_size(&s->trail_lim) ); in var_lev_set_mark() 132 veci_begin(&s->trail_lim)[level] |= 0x80000000; in var_lev_set_mark() 485 veci_push(&s->trail_lim,s->qtail); in solver2_assume() 498 bound = (veci_begin(&s->trail_lim))[level]; in solver2_canceluntil() 499 lastLev = (veci_begin(&s->trail_lim))[veci_size(&s->trail_lim)-1]; in solver2_canceluntil() 515 veci_resize(&s->trail_lim,level); in solver2_canceluntil() 632 assert( s->root_level >= veci_size(&s->trail_lim) ); in solver2_analyze_final() 1142 veci_new(&s->trail_lim); in sat_solver2_new() 1243 veci_delete(&s->trail_lim); in sat_solver2_delete() 1722 Mem += s->trail_lim.cap * sizeof(int); in sat_solver2_memory() [all …]
|
/dports/cad/abc/abc-a4518e6f833885c905964f1233d11e5b941ec24c/src/sat/satoko/ |
H A D | solver.c | 206 vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); in solver_new_decision() 374 for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, 0);) { in solver_analyze_final() 521 for (i = vec_uint_size(s->trail); i --> vec_uint_at(s->trail_lim, level);) { in solver_cancel_until() 529 s->i_qhead = vec_uint_at(s->trail_lim, level); in solver_cancel_until() 530 vec_uint_shrink(s->trail, vec_uint_at(s->trail_lim, level)); in solver_cancel_until() 531 vec_uint_shrink(s->trail_lim, level); in solver_cancel_until() 670 vec_uint_push_back(s->trail_lim, vec_uint_size(s->trail)); in solver_search()
|