acl2 - 如何跟踪 ACL2 重写器？

Question

如何跟踪 ACL2 重写器？我真的很想知道证明者内部发生了什么。寻找此类信息是可取的，还是我应该遵循“方法”？

Answer 1

以下是一些相关的跟踪表格，由 Matt Kaufmann 撰写：

(trace$ (rewrite :cond (null ancestors)
                 :entry (list 'rewrite term alist)
                 :exit (list 'rewrite (cadr values))))

(trace$ (rewrite-with-lemma
         :entry
         (list 'rewrite-with-lemma
               term
               (base-symbol (access rewrite-rule lemma :rune)))
         :exit
         (list 'rewrite-with-lemma (cadr values) (caddr values))))

(open-trace-file "my-trace-file") ; since renamed to big-trace.txt

然后运行你想要跟踪的证明

(close-trace-file)

在您喜欢的文本编辑器中打开跟踪文件，在本例中为 my-trace-file。

关于你的第二个问题，80% 或更多的 ACL2 专家会说，不，你不需要知道重写器发生了什么。我碰巧不同意他们的观点，这就是我写这篇问答的原因（因为我自己会通过谷歌间接引用它）。您还应该查看“break-rewrite”和“dmr”等选项。有关详细信息，请参阅 ACL2 文档主题“调试”。