I would like to assert in Z3 the fact that two (uninterpreted) functions are equal, but I am not entirely sure that Z3 is able to reason on this kind of equality. If, for example, Z3 receives this smtlib script:
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= (f 2) 2))
(assert (= (g 2) 3))
(assert (= f g))
(check-sat)
it answers unknown. On the other hand, by replacing (assert (= f g)) with (assert (forall ((x Int)) (= (f x) (g x)))) Z3 correctly answers unsat. Is it safe to use quantification to assert the equality (and possibly the inequality) of two functions?
Strictly speaking, the SMTLib language does not allow for equality over function types. The underlying logic is that of many-sorted first-order logic. In particular, this means equality is defined only over first-order values.
However, z3 does allow such equalities as an extension. This does not mean it can always decide such equalities. So getting unknown is to be expected. (In general, there's no decision procedure for function equality, i.e., there will always be inputs where the solver will either loop forever or will answer unknown. But that's a different discussion.)
Having said that, the next iteration of SMTLib (v3) will have a higher-order core logic. So, it'll be part of the language that you can write (= f g) where f and g are functions. (Again, this doesn't mean solver will be able to always decide such problems.)
CVC5 has preliminary support for such higher-order features:
$ cat a.smt2
(set-logic HO_ALL)
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= (f 2) 2))
(assert (= (g 2) 3))
(assert (= f g))
(check-sat)
$ cvc5 a.smt2
unsat
Note the special HO_ALL logic name, which is not part of the standard, but is a CVC5 extension.
So, long story short, what you wrote is perfectly fine. Whether a given solver will be able to decide any interesting functions for equality is a different discussion.
Practical Note
In practice, we do this sort of thing quite often in SMT actually. The idea is to declare an existential, and see if the solver can come up with an assignment that distinguishes f and g. So, we'd write:
(declare-fun f (Int) Int)
(declare-fun g (Int) Int)
(assert (= (f 2) 2))
(assert (= (g 2) 3))
(declare-fun x () Int)
(assert (distinct (f x) (g x)))
(check-sat)
(get-model)
And z3 would return:
sat
(
(define-fun x () Int
0)
(define-fun f ((x!0 Int)) Int
(ite (= x!0 0) 1
2))
(define-fun g ((x!0 Int)) Int
(ite (= x!0 0) 4
3))
)
This means the solver can distinguish between f and g, and furthermore it'll also give you a definition for each that is consistent with all your assertions. (In this case, f maps 0 to 1 and everything else to 2. And g maps 0 to 4 and everything else to 3.) From this we'd conclude that f and g are not equivalent.
This strategy is usually successful at determining if f and g are indeed different; but might suffer from decidability issues when they are equal. (i.e., the solver might loop forever, or respond unknown.) This is the essence of equivalence checking as found in many verification systems. (Typically f is some sort of an "implementation" and g is some sort of a "specification," or vice-versa.)