在Z3中定義內射函數

Question

我的目標是定義一個內射函數f: Int -> Term，其中Term是一種新類型。我提到the definition的內射函數，我寫了以下內容：

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

這會導致超時。我懷疑這是因爲求解器試圖驗證Int域中所有值的斷言，這是無限的。

我也檢查了上述模型適用於一些自定義排序，而不是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) 

的第一個問題是如何實現相同的模型Int排序，而不是A。可以解決這個問題嗎？

我還在the tutorial的多模式部分找到了內射函數示例。我不明白爲什麼:pattern註釋有幫助。所以第二個問題是爲什麼使用:pattern，特別是對這個例子有什麼影響。

Answer 1

我想這

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

，我獲得這個

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 y() Int 
    1) 
    (define-fun x() Int 
    0) 
    (define-fun f ((x!1 Int)) Term 
    (ite (= x!1 0) Term!val!0 
    (ite (= x!1 1) Term!val!0 
     Term!val!0))) 
) 

Answer 2

你怎麼看待這個

(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) 

什麼，輸出是

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