z3 - 在Z3中定义内射功能

我的目标是定义一个内射函数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以及它对本示例有何特殊影响。

最佳答案

我正在尝试这个

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

关于z3 - 在Z3中定义内射功能，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/19599649/