Revision b5c43319c7bf98bf39593fde909d1379d12cbe21 authored by Alexander Nadel on 26 April 2022, 10:39:57 UTC, committed by Alexander Nadel on 26 April 2022, 10:39:57 UTC
1 parent 4006699
TopiDecision.cc
// Copyright(C) 2021 Intel Corporation
// SPDX - License - Identifier: MIT
#include "Topi.hpp"
using namespace Topor;
using namespace std;
TULit CTopi::Decide()
{
// #topor : we should try other decision heuristics
// Maple uses DISTANCE for the first 50000 conflicts, then switches between VSIDS and LRB
// Cadical switches between VSIDS and VMTF
// Fiver uses CBH
while (!m_VsidsHeap.empty())
{
TUVar v = m_VsidsHeap.remove_min();
if (!IsAssignedVar(v))
{
++m_Stat.m_Decisions;
m_Stat.m_SumOfAllDecLevels += m_DecLevel;
return GetLit(v, GetNextPolarityIsNegated(v));
}
}
return BadULit;
}
bool CTopi::GetNextPolarityIsNegated(TUVar v)
{
assert(!IsAssignedVar(v));
if (IsNotForced(v))
{
return m_ParamPolarityStrat == 1 ? (bool)(rand() % 2) : m_AssignmentInfo[v].m_IsNegated;
}
else
{
return m_PolarityInfo[v].GetNextPolarityIsNegated();
}
}
void CTopi::UpdateDecisionStrategyOnNewConflict(TUV glueLearnt, TUVar lowestGlueUpdateVar, TUVar fakeTrailEnd)
{
auto D1LowerOrEqD2UpToPrecision = [](double d1, double d2)
{
static constexpr double precision = 0.000001;
return d1 <= d2 || d1 - d2 <= precision;
};
assert(m_Stat.m_VarDecay != 0.0);
if (m_ParamVarDecayUpdateConfRate > 0 && (m_Stat.m_Conflicts % m_ParamVarDecayUpdateConfRate == 0)
&& D1LowerOrEqD2UpToPrecision(m_Stat.m_VarDecay + m_ParamVarDecayInc, m_ParamVarDecayMax))
{
m_Stat.m_VarDecay += m_ParamVarDecayInc;
}
if (m_ParamVarActivityGlueUpdate && glueLearnt != 0)
{
assert(fakeTrailEnd != lowestGlueUpdateVar);
for (TUVar v = fakeTrailEnd; v != BadUVar && m_VarInfo[v].m_TrailNext != lowestGlueUpdateVar; v = m_VarInfo[v].m_TrailPrev)
{
auto& ai = m_AssignmentInfo[v];
assert(ai.m_IsAssigned || fakeTrailEnd != m_TrailEnd);
auto& vi = m_VarInfo[v];
if (ai.m_Visit && (ai.IsAssignedBinary() ||
(vi.m_ParentClsInd != BadUVar && ClsGetIsLearnt(vi.m_ParentClsInd) && ClsGetGlue(vi.m_ParentClsInd) < glueLearnt)))
{
UpdateScoreVar(v);
}
}
}
// Decay activity
m_VsidsHeap.var_inc_update(m_Stat.m_VarDecay);
}
void CTopi::DecisionInit()
{
assert(m_QueryCurr != TQueryType::QUERY_NONE);
if ((m_QueryCurr == TQueryType::QUERY_INIT) || (m_QueryCurr == TQueryType::QUERY_INC_NORMAL && m_ParamVarActivityIncDecayReinitN) ||
(m_QueryCurr == TQueryType::QUERY_INC_SHORT && m_ParamVarActivityIncDecayReinitS &&
(m_ParamVarActivityIncDecayStopReinitSInv == 0 || m_Stat.m_ShortIncSolveInvs < (uint64_t)m_ParamVarActivityIncDecayStopReinitSInv) &&
(m_ParamVarActivityIncDecayStopReinitRestart == 0 || m_Stat.m_Restarts < (uint64_t)m_ParamVarActivityIncDecayStopReinitRestart) &&
(m_ParamVarActivityIncDecayStopReinitConflict == 0 || m_Stat.m_Conflicts < (uint64_t)m_ParamVarActivityIncDecayStopReinitConflict) &&
(m_ParamVarActivityIncDecayStopReinitTime == 0.0 || m_Stat.m_OverallTime.WallTimePassedSinceStartOrResetConst() < m_ParamVarActivityIncDecayStopReinitTime)))
{
m_Stat.m_VarDecay = m_QueryCurr == TQueryType::QUERY_INIT ? m_ParamVarActivityIncDecay : m_ParamVarActivityIncDecayReinitVal;
}
if (InitClssBoostScoreStratOn())
{
m_CurrInitClssBoostScoreMult = InitClssBoostScoreStratIsReversedOrder() ? m_ParamInitClssBoostMultLowest : m_ParamInitClssBoostMultHighest;
}
}
void CTopi::UpdateScoreVar(TUVar v, double mult)
{
const bool isRescaled = m_VsidsHeap.increase_score(v, mult);
if (m_ParamCustomBtStrat > 0)
{
if (isRescaled)
{
for (auto& s : m_BestScorePerDecLevel.get_span_cap())
{
s *= 1e-100;
}
}
if (IsAssignedVar(v))
{
const auto decLevel = GetAssignedDecLevelVar(v);
const auto currScore = m_VsidsHeap.get_var_score(v);
if (decLevel >= m_BestScorePerDecLevel.cap())
{
assert(decLevel <= GetNextVar());
ReserveExactly(m_BestScorePerDecLevel, GetNextVar(), 0, "m_ParamCustomBtStrat in UpdateScoreVar");
if (unlikely(IsUnrecoverable())) return;
}
if (currScore > m_BestScorePerDecLevel[decLevel])
{
m_BestScorePerDecLevel[decLevel] = currScore;
assert(NV(2) || P("m_BestScorePerDecLevel[" + to_string(decLevel) + "] updated to " + to_string(currScore) + " in UpdateScoreVar\n"));
}
assert(m_ParamAssertConsistency < 1 || CalcMaxDecLevelScore(decLevel) == m_BestScorePerDecLevel[decLevel]);
}
}
}
![swh spinner](/static/img/swh-spinner.gif)
Computing file changes ...