9

次の 2 つの宣言について混乱します。私にとって、それらは同じことを説明しています:整数変数ですx。

  • (declare-const x Int)
  • (declare-fun x () Int)

パフォーマンスが異なる、または異なるモデルを提供するコンテキストはありますか? ありがとう。

4

1 に答える 1

10

はい、(declare-const x Int)ただの構文 sugar(declare-fun x () Int)です。性能に違いはありません。declare-constSMT-Lib 2.0 標準の一部ではないことに注意してください。

于 2013-10-26T17:49:19.120 に答える