1

クリックしてファイルを表示

このファイルは SMT2.0 規格に準拠していますか? 少なくとも z3 はそれを受け入れることができます。ところで、'declare-const' と 'declare-fun' の違いは何ですか? たとえば、Bool 変数を宣言するために、declare-const a Boolorと書くことができますdeclare-fun a() Bool。

4

1 に答える 1

1

投稿で言及されているファイルを見つけることができませんが、declare-const に関する質問に答えるために:

(declare-const a Bool)

と同じ意味

(declare-fun a () Bool)

declare-const は、標準の SMT-LIB2 の一部ではありません。SMT-LIB2 ベンチマークを手動で入力するのに便利なように Z3 に追加されたコマンドです。ソルバー間で互換性を保つために、代わりにdeclare-funをいつでも使用できます。

Z3 は SMT-LIB2 準拠のファイルを処理できます。一方、Z3 の入力形式には、SMT-LIB2 標準の一部ではない他の拡張機能がいくつかあります。いくつか言及するには：

  • 宣言データ型。代数データ型の宣言は、Z3 固有の拡張機能です。

  • 戦術とソルバー。戦術の作成、構成、および適用は、Z3 に固有のものです。

  • 宣言-rel、宣言-var、ルール、クエリ。これらのコマンドは、Horn 式としてベンチマークを入力するのに便利なように、固定小数点ソルバーによって使用されます。

于 2013-01-06T10:29:21.417 に答える