1

ラムダ関数の速度に問題があります。コードは次のとおりです。

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 倍の速度低下は大きすぎます。

4

1 に答える 1