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) を開きます。

2 番目の質問に関しては、ACL2 の専門家の 80% 以上が、いいえ、リライターで何が起こっているかを知る必要はないと言うでしょう。私はたまたま彼らの意見に同意しないので、この Q&A を書きました (Google 経由で間接的に参照するため)。「break-rewrite」や「​​dmr」などのオプションも検討する必要があります。詳細については、ACL2 ドキュメントのトピック「デバッグ」を参照してください。