如何跟踪 ACL2 重写器？答案

【问题标题】：How do I trace the ACL2 rewriter?如何跟踪 ACL2 重写器？
【发布时间】：2015-09-29 13:40:36
【问题描述】：

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

【问题讨论】：

标签： acl2

【解决方案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 文档主题“调试”。

【讨论】：