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