Как я могу отследить ACL2 rewriter?

Question

Как я могу отследить ACL2 rewriter? Мне бы очень хотелось узнать, что происходит внутри прувера. Желательно ли искать этот тип информации или я должен просто следовать Методу?

Answer 1

Вот некоторые соответствующие формы следов, автором которых является Мэтт Кауфманн:

(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). Вам также следует обратить внимание на такие опции, как "перезапись" и "dmr". См. Раздел документации ACL2 "отладка" для получения дополнительной информации.