小编Ale*_*ler的帖子

我正在观看一个演讲,"算法效率,数据结构性能",并对以下评论感到惊讶:

#include <string>
#include <unordered_map>
#include <memory>

struct Foo {
  int x;
};

Foo* getFoo(std::string key,
            std::unordered_map<std::string,
                               std::unique_ptr<Foo>> &cache) {
  if (cache[key])
    return cache[key].get();

  cache[key] = std::unique_ptr<Foo>(new Foo());
  return cache[key].get();
}

Foo* getFooBetter(std::string key,
                  std::unordered_map<std::string,
                                     std::unique_ptr<Foo>> &cache) {
  std::unique_ptr<Foo> &entry = cache[key];
  if (entry)
    return entry.get();

  entry = std::unique_ptr<Foo>(new Foo());
  return entry.get();
}

getFooBetter()更好.我一直认为我可以依赖编译器来执行这种转换,就像我期望多次出现x+y只被评估一次一样.不出所料,生成的LLVM IR确实与演示者一致.即使使用-O9,我们也会cache[key]在getFoo()版本中留下3个电话.

我已经移动了两个长的LLVM IR,其中c ++符号没有被标记为脱节,以免在视觉上令人反感.

另一个StackOverflow问题揭示了这里的部分答案operator[] 是假设能够修改它所希望的任何全局状态,因此我们不能忽略调用. 关于引入注释的链接提议将 …

我有一个功能max：

Fixpoint max (n : nat) (m : nat) : nat :=
  match n, m with
    | O, O => O
    | O, S x => S x
    | S x, O => S x
    | S x, S y => S (max x y)
  end.

以及交换律的证明max如下：

Theorem max_comm :
  forall n m : nat, max n m = max m n.
Proof.
  intros n m.
  induction n as [|n'];
    induction m as [|m'];
      simpl; trivial. …