例如，
$ 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)or (-> (Int Real) Int)or (_ (Int Real) Int)，但没有一个是正确的。
是否可以在 smtlib 中声明函数排序？
如果无法声明函数排序，如何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
谢谢。