acl2 - 禁用太多如果启发式

Question

如何禁用太多ifs启发式？有时证明者出去吃午饭，当我打断它时，我可以看到证明者正忙于调用too-many-ifs0and count-ifs-lst。

Answer 1

您可以通过发出以下表格将太多的 ifs 启发式转换为有效的空操作。请注意，如果您在一本书中使用这些，您可能希望将以下每个表单都设置为“本地”：

(defn too-many-ifs-pre-rewrite-noop (args counts)
  (declare (ignore args counts))
  nil)

(defattach too-many-ifs-pre-rewrite too-many-ifs-pre-rewrite-noop)

(defn too-many-ifs-post-rewrite-noop (args counts)
  (declare (ignore args counts))
  nil)

(defattach too-many-ifs-post-rewrite too-many-ifs-post-rewrite-noop)