如何跟踪ACL2重写器？

Question

如何跟踪ACL2重写器？我真的很想知道prover内部发生了什么。寻找这种类型的信息是明智的，还是我应该只遵循这种方法？

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专家会说，不，你不需要知道重写器发生了什么。我碰巧不同意他们的观点，这就是为什么我写了这篇问答(因为我自己会通过Google间接引用它)。你还应该考虑像"break-rewrite“和"dmr”这样的选项。有关详细信息，请参阅ACL2文档主题“调试”。