Lines Matching refs:score_
359 score_.resize(s.numVars()+1, VarInfo(vars_.end())); in startInit()
365 if (s.value(v) == value_free && score_[v].pos_ == vars_.end()) { in endInit()
366 score_[v].activity(decay_); in endInit()
368 score_[v].activity_ = momsScore(s, v); in endInit()
369 score_[v].decay_ = decay_+1; in endInit()
371 score_[v].pos_ = vars_.insert(vars_.end(), v); in endInit()
375 vars_.sort(LessLevel(s, score_)); in endInit()
377 if (score_[*it].decay_ != decay_) { in endInit()
378 score_[*it].activity_ = 0; in endInit()
379 score_[*it].decay_ = decay_; in endInit()
388 growVecTo(score_, v+n, VarInfo(vars_.end())); in updateVar()
390 if (score_[v].pos_ == vars_.end()) { score_[v].pos_ = vars_.insert(vars_.end(), v); } in updateVar()
394 else if (v < score_.size()) { in updateVar()
395 if ((v + n) > score_.size()) { n = score_.size() - v; } in updateVar()
397 if (score_[x].pos_ != vars_.end()) { in updateVar()
398 vars_.erase(score_[x].pos_); in updateVar()
399 score_[x].pos_ = vars_.end(); in updateVar()
407 if (score_[s.trail()[i].var()].pos_ != vars_.end()) { in simplify()
408 vars_.erase(score_[s.trail()[i].var()].pos_); in simplify()
409 score_[s.trail()[i].var()].pos_ = vars_.end(); in simplify()
417 LessLevel comp(s, score_); in newConstraint()
422 score_[v].occ_ += 1 - (((int)first->sign())<<1); in newConstraint()
423 if (upAct) { ++score_[v].activity(decay_); } in newConstraint()
439 if (score_[v].pos_ != vars_.end()) { in newConstraint()
440 vars_.splice(vars_.begin(), vars_, score_[v].pos_); in newConstraint()
457 if (ms || !s.seen(lits[i])) { ++score_[lits[i].var()].activity(D); } in updateReason()
460 if (scType_ & 1u) { ++score_[r.var()].activity(decay_); } in updateReason()
465 score_[it->first.var()].activity(decay_) += static_cast<uint32>(it->second*adj); in bump()
481 c = (score_[*front_].activity(decay_) + (distance<<1)+ 3) > score_[*v2].activity(decay_) in doSelect()
482 ? selectLiteral(s, *front_, score_[*front_].occ_) in doSelect()
483 : selectLiteral(s, *v2, score_[*v2].occ_); in doSelect()
486 c = selectLiteral(s, *front_, score_[*front_].occ_); in doSelect()
494 if (score_[first->var()].activity(decay_) > score_[best.var()].activity(decay_)) { in selectRange()
512 : vars_(CmpScore(score_)) in ClaspVsids_t()
531 score_.resize(s.numVars()+1); in startInit()
543 mx = std::max(mx, score_[v].get()); in endInit()
553 double o = score_[v].get(), n; in updateVarActivity()
554 f = ScoreType::applyFactor(score_, v, f); in updateVarActivity()
559 score_[v].set(n); in updateVarActivity()
570 growVecTo(score_, v+n); in updateVar()
583 if (s.value(v) == value_free && score_[v].get() == 0.0 && (ms = (double)momsScore(s, v)) != 0.0) { in initScores()
585 score_[v].set(-ms); in initScores()
589 double d = score_[v].get(); in initScores()
593 score_[v].set(d); in initScores()
609 for (LitVec::size_type i = 0; i != score_.size(); ++i) { in normalize()
610 double d = score_[i].get(); in normalize()
617 score_[i].set(d); in normalize()
720 Var end = std::min(static_cast<Var>(score_.size()), static_cast<Var>(s.numVars() + 1)); in detach()
722 if (score_[v].sign) { s.setPref(v, ValueSet::user_value, value_free); } in detach()
740 if (score_[v].domP >= nKey) { in initScores()
741 bool sign = score_[v].sign; in initScores()
742 score_[v] = DomScore(score_[v].value); in initScores()
757 if (score_[it->var()].domP >= nKey){ in initScores()
758 score_[it->var()].setDom(nKey++); in initScores()
767 score_[x.first].value += x.second; in initScores()
768 score_[x.first].init = 0; in initScores()
804 if (e.type() == DomModType::Init && score_[e.var()].init == 0) { in addDomAction()
805 initOut.push_back(std::make_pair(e.var(), score_[e.var()].value)); in addDomAction()
806 score_[e.var()].init = 1; in addDomAction()
815 score_[e.var()].sign |= static_cast<uint32>(e.type() == DomModType::Sign); in addDomAction()
825 return score_[e.var()].domP + 1; in addDomAction()
829 if (s.value(x.var()) != value_free || score_[x.var()].domP < domKey) { return; } in addDefAction()
832 if (score_[x.var()].domP > domKey && lev && valMod) { in addDefAction()
833 if (defMod_ < HeuParams::mod_init) { score_[x.var()].level += lev; } in addDefAction()
834 else if (defMod_ == HeuParams::mod_init) { score_[x.var()].value += (lev*100); } in addDefAction()
835 …else if (defMod_ == HeuParams::mod_factor) { score_[x.var()].factor += 1 + (lev > 3) + (lev > 15);… in addDefAction()
840 if (oPref == value_free || (score_[x.var()].sign == 1 && domKey != score_[x.var()].domP)) { in addDefAction()
842 score_[x.var()].sign = 1; in addDefAction()
844 else if (score_[x.var()].sign == 1 && oPref != nPref) { in addDefAction()
846 score_[x.var()].sign = 0; in addDefAction()
852 score_[x.var()].setDom(domKey); in addDefAction()
858 s.stats.addDomChoice(score_[x.var()].isDom()); in doSelect()
885 score_[a.var].value = a.bias; in applyAction()
887 case DomModType::Factor: std::swap(score_[a.var].factor, a.bias); break; in applyAction()
889 std::swap(score_[a.var].level, a.bias); in applyAction()