
digraph G {
  graph [
    bgcolor="white", pad="0.28", nodesep="0.38", ranksep="0.58",
    fontname="WenQuanYi Zen Hei", fontcolor="#17212B", fontsize=24,
    labelloc="t", labeljust="l"
  ];
  node [
    shape=box, style="rounded,filled", margin="0.18,0.12",
    fontname="WenQuanYi Zen Hei", fontcolor="#17212B", fontsize=12,
    color="#CBD5E1", penwidth=1.3, fillcolor="#F8FAFC"
  ];
  edge [
    fontname="WenQuanYi Zen Hei", fontcolor="#64748B", fontsize=10,
    color="#64748B", penwidth=1.5, arrowsize=0.75
  ];

  label="图 2-1  同一比较在不同编译形态下形成的符号约束";
  rankdir=TB;

  src [label="源码语义\nmemcmp(buf, \"SYMC\", 4) == 0", fillcolor="#FEF3C7", color="#D97706"];
  b [label="-O0 / -fno-builtin\ncall 指令幸存", fillcolor="#DBEAFE", color="#2563EB"];
  a [label="常见 -O2\n内联、bswap、宽 icmp", fillcolor="#CCFBF1", color="#0F766E"];
  c [label="源码逐字节循环\nN 个独立分支", fillcolor="#FFEDD5", color="#C2410C"];
  sb [label="形态 B · libc 包装器\nn 个 Equal + And 链", fillcolor="#DBEAFE", color="#2563EB"];
  sa [label="形态 A · 宽整数比较\nEqual(Concat, Constant)", fillcolor="#CCFBF1", color="#0F766E"];
  sc [label="形态 C · 单字节约束\nN 条 icmp", fillcolor="#FFEDD5", color="#C2410C"];
  ob [label="否定后任一字节不同即可\n不自然形成逐前缀进展", fillcolor="#F1F5F9"];
  oa [label="纯 2–8 B 常量比较\nfastSolveConcat 可绕过 Z3", fillcolor="#DCFCE7", color="#15803D"];
  oc [label="依赖反馈迭代\nMULTI_SOLVE 可联合翻转", fillcolor="#F1F5F9"];

  src -> {b a c};
  b -> sb -> ob;
  a -> sa -> oa;
  c -> sc -> oc;

}
