如何在Z3 3.2中獲取統計信息？

(get-info statistics)

獲得Z3運行的統計數據。使用Z3 3.2我得到

(error "line _ column _: invalid command argument, keyword expected")

針對上述情況，並

(get-info :statistics)

Z3與

unsupported

什麼是獲得統計數據（比/ ST命令 - 其他的新的方式回覆線選項）？

雖然我們在這個參數： INI options page列出

(set-option :STATISTICS true)

爲一個有效的選擇，但Z3 3.2再次

unsupported

(get-info :all-statistics)

回答應該做的伎倆。

2012-01-09 10:01:58 pad

的確如此，謝謝！它在文檔中的某處提到過嗎？ – 2012-01-09 10:06:04

我在http://rise4fun.com/samples瀏覽Z3的示例時看到了它（請參閱我的更新）。 – pad 2012-01-09 10:09:02

是否有可能獲得特定統計信息的方式，例如「衝突」還是「量化實例化」？ – 2012-01-09 10:13:19

回答