1

我有一个关于declare-constsmtlib 的问题。

例如，

在z3/cvc4中，以下程序不报错：

C:\Users\Chansey>z3 -in
(declare-const x Int)
(declare-const x Bool)

在 smt-lib-reference 中，它说

(declare-fun f (s1 ... sn) s) ... 如果当前签名中已经存在名称为 f 的函数符号，该命令将报告错误。

所以排序s包含在 的整个签名中x，对吗？

但为什么会这样呢？其背后的动机是什么？

在我的理解中，xis 是变量标识符，一般来说（例如在一些通用编程语言中）我们不允许用不同的类型声明同一个变量。所以我觉得上面的代码最好是报错。

我曾经认为也许z3/smtlib可以支持重新定义？，但不是......

C:\Users\Chansey>z3 -in
(declare-const x Int)
(declare-const x Bool)
(assert (= x true))
(error "line 3 column 11: ambiguous constant reference, more than one constant with the same sort, use a qualified expre
ssion (as <symbol> <sort>) to disambiguate x")

那么上面的代码肯定是错的，为什么不早点报错呢？

PS。如果我使用相同的排序，那么它会报错（那太好了，我希望Bool案例也能报错）：

C:\Users\Chansey>z3 -in
(declare-fun x () Int)
(declare-fun x () Int)
(error "line 2 column 21: invalid declaration, constant 'x' (with the given signature) already declared")

谢谢。

4

1 回答 1

3

在 SMTLib 中，符号不仅由其名称标识，而且由其排序标识。正如您所观察到的，只要您有不同的类型，使用相同的名称就可以了。这是一个例子：

(set-logic ALL)
(set-option :produce-models true)
(declare-fun x () Int)
(declare-fun x () Bool)

(assert (= (as x Int) 4))
(assert (= (as x Bool) true))
(check-sat)
(get-model)
(get-value ((as x Int)))
(get-value ((as x Bool)))

这打印：

sat
(
  (define-fun x () Bool
    true)
  (define-fun x () Int
    4)
)
(((as x Int) 4))
(((as x Bool) true))

请注意我们如何使用as构造来消除两者之间的歧义x。这在http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf的第 3.6.4 节中进行了解释

话虽如此，我确实同意您引用的文件部分对此不是很清楚，也许可以使用一些澄清文本。

关于允许这种用法的动机是什么： 有两个主要原因。首先是简化生成 SMTLib。请注意，SMTLib 通常不是手写的。它通常由使用 SMT 求解器的高级系统生成。因此，当您将 SMTLib 用作高级系统和求解器本身之间的中间语言时，灵活地允许符号共享名称（只要它们可以通过显式排序注释区分）是有益的。但是，当您手动编写 SMTLib 时，如果可以的话，您可能应该避免这种重复，如果没有别的，为了清楚起见。

第二个原因是允许使用有限形式的“重载”。例如，想想 SMTLib 函数distinct。此函数可以对任何类型的对象（Int、Bool等Real）进行操作，但它总是被调用distinct。（我们没有distinct-int等distinct-bool。）求解器通过做一些分析“区分”你的意思，但如果它不能，你也可以通过as声明来帮助它。因此，理论符号可以以这种方式重载，对于=, +,*等也是如此。当然，SMTLib不允许用户定义这样的重载名称，但正如文档在第 91 页脚注 29 中所述，这将来可能会取消限制。

于 2021-08-18T14:38:05.573 回答