1

Z3 2.x では SMTLib2 コマンドを使用しました

(get-info statistics)

Z3 実行の統計を取得します。Z3 3.2 を使用すると、

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

上記のために、そして

(get-info :statistics)

Z3 は次のように応答します。

unsupported

統計情報を取得する新しい方法 (/st コマンド ライン オプション以外) は?

INIオプションページのリスト

(set-option :STATISTICS true)

は有効なオプションですが、Z3 3.2 は再び次のように応答します。

unsupported
4

1 に答える 1

2 
(get-info :all-statistics)

トリックを行う必要があります。

公式の例: http://rise4fun.com/Z3/doc_examples

于 2012-01-09T10:01:58.260 に答える