acl2 - 多すぎる場合のヒューリスティックを無効にする

Question

too many-ifs ヒューリスティックを無効にするにはどうすればよいですか? 証明者が昼食に出かけることがあり、それを中断すると、証明者が と の呼び出しで忙しいことがわかりtoo-many-ifs0ますcount-ifs-lst。

Answer 1

次のフォームを発行することにより、too-many-ifs ヒューリスティックを効果的な no-op に変換できます。これらを本で使用している場合は、おそらく以下の各フォームを「ローカル」にしたいことに注意してください。

(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)