ACL2 的 GL 时钟用完了

【问题标题】：ACL2's GL clock ran outACL2 的 GL 时钟用完了
【发布时间】：2015-11-05 00:17:32
【问题描述】：

收到以下错误消息是什么意思？我已经加载了 GL。

| ACL2 Error in ( DEFTHM SOME-THEOREM-THAT-USES-GL ...):  The clock
| ran out.~%

【问题讨论】：

标签： acl2

【解决方案1】：

很可能当您加载了 GL 时，您还没有定义一个包含所有必要符号对应项的子句处理器。即使您已经定义了 GL 子句处理器，也可能发生这种情况——自定义 GL 子句处理器以来，您可能已经包含了一些其他书籍。

要解决它，只需定义另一个 GL 子句处理器：

(def-gl-clause-processor yet-another-gl-clause-processor)

【讨论】：