CODEWITHSUNDEEP
acl2
interestedparty333
interestedparty333

Reputation: 2536

How do I trace the ACL2 rewriter?

How do I trace the ACL2 rewriter? I would really like to know what's going on inside the prover. Is it advisable to seek out this type of information or should I just follow The Method?

Upvotes: 3

Views: 71

Answers (1)

interestedparty333
interestedparty333

Reputation: 2536

Here are some relevant trace forms, authored by 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

Then run your proof you want trace

(close-trace-file)

Open up the trace file, my-trace-file in this example, in your favorite text editor.

With regards to your second question, 80% or more of ACL2 experts would say that, no, you don't need to know what's going on with the rewriter. I happen to disagree with them, which is why I've written this Q&A (as I will reference it myself indirectly via Google). You should also look into options like "break-rewrite" and "dmr". See ACL2 documentation topic "debugging" for more information.

Upvotes: 3

Related Questions