z3smtcvc4smt-lib

Is it possible to declare a function sort in smtlib?

For example,

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

This is OK.

However, I'd like to qualify it by as?

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

What should I fill in ????

It must be a sort, but what sort should I use?

I have tried ((Int Real) Int) or (-> (Int Real) Int) or (_ (Int Real) Int), but none of them are correct.

Is it possible to declare a function sort in smtlib?

If there is impossible to declare a function sort, how to disambiguate f in the following program:

$ 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")

Note that if I don’t use functions, it’s no problem:

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

Thanks.

Solution

  • The annotation

    (as f Int)

    is correct, even though (as you noticed) is very confusing. This annotation does not necessarily mean f is Int. Rather, it means f results in an Int, so it could also be a function.

    This is very confusing indeed, but it follows the standard http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2021-05-12.pdf, page 27:

    Recall that every function symbol f is separately associated with one or more ranks, each specifying the sorts of f ’s arguments and result. To simplify sort checking, a function symbol in a term can be annotated with one of its result sorts σ. Such an annotated function symbol is a qualified identifier of the form (as f σ).

    As indicated above in (as f σ), the type σ is the result sort of f.

    Note also that solver support for these annotations is rather inconsistent. For a previous discussion on this, see https://github.com/Z3Prover/z3/issues/2135