我的目标是定义一个单射函数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/