Defining injective functions in Z3

Question

My goal is to define an injective function f: Int -> Term, where Term is some new sort. Having referred to the definition of the injective function, I wrote the following:

(declare-sort Term)
(declare-fun f (Int) Term)
(assert (forall ((x Int) (y Int))
                (=> (= (f x) (f y)) (= x y))))
(check-sat)

This causes a timeout. I suspect that this is because the solver tries to validate the assertion for all values in the Int domain, which is infinite.

I also checked that the model described above works for some custom sort instead of Int:

(declare-sort Term)
(declare-sort A)
(declare-fun f (A) Term)
(assert (forall ((x A) (y A))
                (=> (= (f x) (f y)) (= x y))))
(declare-const x A)
(declare-const y A)
(assert (and (not (= x y)) (= (f x) (f y))))
(check-sat)
(get-model)

The first question is how to implement the same model for Int sort instead of A. Can solver do this?

I also found the injective function example in the tutorial in multi-patterns section. I don't quite get why :pattern annotation is helpful. So the second question is why :pattern is used and what does it brings to this example particularly.

Answer 1

What do you think about this

(declare-sort Term)
(declare-fun f (Int) Term)
(define-fun biyect () Bool
    (forall ((x Int) (y Int))
            (=> (= (f x) (f y)) (= x y))))
(assert (not biyect))
(check-sat)
(get-model)

and the output is

sat 
(model 
;; universe for Term: 
;; Term!val!0 
;; ----------- 
;; definitions for universe elements: 
(declare-fun Term!val!0 () Term) 
;; cardinality constraint: 
(forall ((x Term)) (= x Term!val!0))
;; ----------- 
(define-fun x!1 () Int 0)
(define-fun y!0 () Int 1) 
(define-fun f ((x!1 Int)) Term 
 (ite (= x!1 0) Term!val!0 
 (ite (= x!1 1) Term!val!0 
   Term!val!0))) 
)