问在SMT-LIB中，数组与返回数组的no函数之间是否有区别？
EN

Stack Overflow用户

提问于 2014-10-09 17:31:10

回答 1查看 147关注 0票数 0

以下两个声明/命令在SMT-LIB语言中语义上是否相同？

(declare-fun a1 () (Array Index Element))
(declare-const a2 (Array Index Element))

对于Z3，适用于a1的断言也适用于a2 (没有语法更改)。一种可能的方法是将a1的使用(没有参数)作为a1的一个应用程序。在Z3 (或者SMT语言)中是这样的吗？

回答已采纳

发布于 2014-10-09 21:12:05

在当前的SMT提案草案-LIB v2.5中，声明-const定义为：

(declare-const f σ) abbreviates the command (declare-fun f () σ)

其中f是函数名，σ是排序符号。所以第二个是第一个的宏。

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/26284537

复制

相似问题

问在SMT-LIB中，数组与返回数组的no函数之间是否有区别？EN