【发布时间】：2013-11-05 10:27:31
【问题描述】：
我对以下两个声明感到困惑。对我来说，他们描述的是同一个东西：一个整数变量x。
(declare-const x Int)(declare-fun x () Int)
是否有任何背景使它们在性能上有所不同或提供不同的模型？ 谢谢。
【问题讨论】：
标签： z3
【发布时间】：2013-11-05 10:27:31
【问题描述】：
是的，(declare-const x Int) 只是语法糖(declare-fun x () Int)。性能上没有区别。请注意，declare-const 不是 SMT-Lib 2.0 标准的一部分。
【讨论】：
-
谢谢。所以我猜 Z3 教程很旧，因为它用许多声明常量来说明。