Home
last modified time | relevance | path

Searched refs:trail_lim (Results 1 – 25 of 59) sorted by relevance

123

/dports/math/chuffed/chuffed-e04bedd/chuffed/core/
H A Dsat.h192 …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 Dengine.h60 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 DSolver.cpp209 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 Dpropengine.h179 …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 Dpropengine.h179 …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 DSolver.cpp209 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 DSolver.h183 …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 DSolver.cc239 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 DSolver.h193 …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 DSolver.cc233 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 DSolver.h193 …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 DSolver.cc233 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 DSolver.h193 …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 DSolver.cc238 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 DSolver.h199 …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 DSolver.C180 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 DSolver.h136 …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 DSolver.cc356 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 DSolver.h267 …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 DGlucose.cpp473 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 DSolver.h238 …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 DSolver.h199 …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 DsatSolver3.c638 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 DsatSolver2.c131 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 Dsolver.c206 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()

123