ラムダ関数の速度に問題があります。コードは次のとおりです。
Lit Simplifier::lit_diff_watches(const OccurClause& a, const OccurClause& b)
{
set_seen_for_lits(b, 1);
size_t num = 0;
Lit toret = lit_Undef;
const auto check_seen = [&] (const Lit lit) {
if (seen[lit.toInt()] == 0) {
toret = lit;
num++;
}
};
for_each_lit(a, check_seen);
/*switch(a.ws.getType()) {
case CMSat::watch_binary_t:
check_seen(a.lit);
check_seen(a.ws.lit2());
break;
case CMSat::watch_tertiary_t:
check_seen(a.lit);
check_seen(a.ws.lit2());
check_seen(a.ws.lit3());
break;
case CMSat::watch_clause_t: {
const Clause& clause = *solver->clAllocator->getPointer(a.ws.getOffset());
for(const Lit lit: clause) {
check_seen(lit);
}
break;
}
}*/
set_seen_for_lits(b, 0);
if (num == 1)
return toret;
else
return lit_Undef;
}
for_each_lit
関数のシグネチャは次のとおりです。
void for_each_lit(
const OccurClause& cl
, std::function<void (const Lit lit)> func
);
この関数lit_diff_watches
は何百万回も実行され、例では 3.3 秒かかります。ただし、スイッチのコメントを外してコメント アウトするとfor_each_line
(スイッチのコピー アンド ペースト)、まったく同じ実行で 1.7 秒が得られます。99% の確率で発生することに注意してくださいwatch_binary_t
。つまり、関数呼び出しwatch_tertiary_t
ごとに実行される命令はごくわずかです。lit_diff_watches
私が間違っていることを教えてください。動作は GCC 4.7 と現在の llvm-svn (2013 年 11 月 25 日) の両方で同じですが、タイミングの違いはわずかです。関数呼び出しはインライン化されていないと推測していますが、私は専門家ではありません。switch(..){..}
これはコードの多くの場所にあり、ラムダ & を使用するとコードfor_each_lit
が大幅にクリーンアップされるため、これを修正したいと思います。しかし、これ以上スピードを落とすわけにはいきません。10 ~ 20% であれば問題ありませんが、ほぼ 2 倍の速度低下は大きすぎます。