9

我对以下两个声明感到困惑。对我来说，它们描述的是同一件事：一个整数变量x。

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

是否有任何背景使它们在性能上有所不同或提供不同的模型？谢谢。

4

1 回答 1

10

是的，(declare-const x Int)只是语法糖(declare-fun x () Int)。性能上没有区别。请注意，这declare-const不是 SMT-Lib 2.0 标准的一部分。

于 2013-10-26T17:49:19.120 回答