如何在VST中丢弃不再需要的LOCAL变量？

VST提供了专门的策略和引理来清理局部上下文中不再需要的LOCAL变量，具体工具如下：

• remove_unused_locals 策略：这是最便捷的自动清理工具，它会扫描当前局部上下文，自动移除后续证明步骤不会用到的LOCAL变量。在证明脚本中直接调用 remove_unused_locals. 即可完成操作，无需手动指定变量。

• drop_local 引理：适合手动指定移除特定变量的场景。当你明确知道某个LOCAL变量后续不再被引用时，可以通过 apply drop_local with (v := 变量名) 或者结合其他定位策略来调用这个引理，精准剔除目标变量。

• 复合简化策略附带清理逻辑：像 cleanup、simplify 这类复合策略在简化证明目标的同时，也会自动清理冗余的LOCAL变量。不过这类策略还会执行其他简化操作，若仅需清理变量，优先使用 remove_unused_locals 更高效。

关于性能的补充：LOCAL上下文的大小确实会影响VST的运行效率——上下文越大，每次策略调用时遍历、检查变量的开销就越高。及时清理无用变量能有效减少上下文冗余，对提升证明运行速度有实际帮助。

内容的提问来源于stack exchange，提问作者Russell O'Connor