acl2 - 如何跟踪ACL2重写器？

如何跟踪ACL2重写器？我真的很想知道证明者内部的情况。建议您查找此类信息，还是应该只遵循“方法”？

最佳答案

这是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文档主题“调试”。

关于acl2 - 如何跟踪ACL2重写器？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/31346986/