是否可以在smtlib中声明函数排序?

Question

例如

$ z3 -in
(declare-fun f (Int Real) Int)
(assert (= f f))
(check-sat)
sat

可以。

但是，我想用as?

来限定它

$ z3 -in
(declare-fun f (Int Real) Int)
(assert (= (as f ???) (as f ???)))
(check-sat)
sat

???该怎么填?

它必须是一个排序，但是我应该使用什么排序呢?

我试过((Int Real) Int)或(-> (Int Real) Int)或(_ (Int Real) Int)，但它们都不正确。

是否可以在smtlib中声明一个函数排序?

如果不可能声明函数sort，如何在下列程序中消除f的歧义:

$ z3 -in
(declare-fun f (Int Real) Real)
(declare-fun f (Int Bool) Real)
(assert (= f f))
(error "line 3 column 11: ambiguous constant reference, more than one constant with the same sort, use a qualified expression (as <symbol> <sort>) to disambigua
te f")

请注意，如果我不使用函数，也没有问题:

$ z3 -in
(declare-fun f () Int)
(assert (= (as f Int) (as f Int)))
(check-sat)
sat

谢谢。

Answer 1

注释

(as f Int)

是正确的,尽管(当你注意到)非常混乱。这个注释并不一定意味着f就是Int。相反，它意味着f的结果是Int，所以它也可以是一个函数。

这确实很令人困惑，但它遵循标准http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf，第27页:

回想一下，每个函数符号f分别与一个或多个秩相关联，每个秩指定f的参数和结果的种类。为了简化排序检查，一个项中的函数符号可以用它的一个结果排序σ来注解。这样一个带注释的函数符号是一个形式为(如f σ)的限定标识符。

如上文(as f σ)所示，σ的类型为，即f的结果排序。

还要注意，求解器对这些注释的支持相当不一致。有关此问题的先前讨论，请参阅https://github.com/Z3Prover/z3/issues/2135