z3 - Z3 中的不同集合

Question

我有以下程序：

;;; Sets
(declare-fun lock_0 (Int) Bool)
(declare-fun lock_1 (Int) Bool)
(declare-fun lock_2 (Int) Bool)
(declare-fun lock_3 (Int) Bool)

;;; verify if sets lock_0 and lock_1 haven't elements in common
(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

;;; verify if sets lock_2 and lock_3 haven't elements in common
(assert (exists ((x Int)) (=> (lock_2 x) (not (lock_3 x)))))

;;; Sets only contain 1 for Lock_0 and lock_1 or 2 for lock_2 or lock_3
(assert (forall ((x Int)) (= (lock_0 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_1 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_2 x)  (= x 1))))
(assert (forall ((x Int)) (= (lock_3 x)  (= x 1))))

;;; set [l1]
(declare-fun SL1 (Int) Bool) 
;;; set only contain 1
(assert (forall ((x Int)) (= (SL1 x) (= x 1))))
;;; SL1 subset lock_2
(assert (forall ((x Int)) (=> (SL1 x) (lock_2 x))))

;; sat
(check-sat)
( get-value (( lock_0 1 )))
( get-value (( lock_0 2 )))
( get-value (( lock_1 1 )))
( get-value (( lock_1 2 )))
( get-value (( lock_2 1 )))
( get-value (( lock_2 2 )))
( get-value (( lock_3 1 )))
( get-value (( lock_3 2 )))
( get-value (( SL1 1 )))
( get-value (( SL1 2 )))

结果：

sat
((( lock_0 1 ) false))
((( lock_0 2 ) true))
((( lock_1 1 ) false))
((( lock_1 2 ) true))
((( lock_2 1 ) true))
((( lock_2 2 ) false))
((( lock_3 1 ) true))
((( lock_3 2 ) false))
((( SL1 1 ) true))
((( SL1 2 ) false))

我需要生成lock_0以下lock_1集合：

[] - Empty set
[2]

lock_2并生成lock_3以下集合：

[] - Empty set
[1]

但集合lock_0并lock_1不能有共同的元素。

但最后我得到：

( get-value (( lock_0 2 ))) true
( get-value (( lock_1 2 ))) true

结果对每个人都是正确的，在一种情况下应该是错误的，例如：

( get-value (( lock_0 2 ))) false
( get-value (( lock_1 2 ))) true

因为集合不能包含相等的元素。

lock_2和的问题相同lock_3。

如果我添加：

;;; Set [l2]
(declare-fun SL2 (Int) Bool)

;;; set only contain 2
(assert (forall ((x Int)) (= (SL2 x) (= x 2))))
;;; SL2 is subset lock_0
(assert (forall ((x Int)) (=> (SL2 x) (lock_0 x))))

;; unsat
(check-sat)

我希望结果是不满意的，但是由于集合（lock_0 and lock_1或lock_2 and lock_3）相等，我会坐下来。

例如：如果我得到lock_0 = []andlock_1 = [2]和lock_2 = [1]and lock_3 = []，程序是正确的。

我怎么解决这个问题？

开始编辑

添加这段代码： (assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x)))))

结果不满意。它应该是坐着的。

那么如何为同一个集合、空集合或集合 {2} 生成？还是不可能做到？

如果这是不可能的，那么我们可以让元素 0 是空集吗？但为此，我只能拥有以下套装：

[0] - empty set 
[2]

所以我这样做：(assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (= x 2)))))

但是，如果我想要这些集合lock_0并且lock_1可能也有 3 作为一个元素应该得到：

[0] - empty set
[2]
[3]
[2,3] - may not include zero, since only the zero should be used as the singleton set [0]

所以我这样做：(assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (and (!= x 0) (or (= x 2) (= x 3)))))))

是对的吗？

另一个问题：如果我想创建一个接受集合的函数？因为集合是一个函数。例如：

(define-fun example ((s1 Set) (s2 Set) (x Int)) Int
  (if (and (s1 x) (not (s2 x)))
      (* x x)
      0))

但我不知道用什么来代替 Set (Set s1)，请帮帮我。

结束编辑

Answer 1

我发现您的编码存在一些问题。

一、命令

;;; verify if sets lock_0 and lock_1 haven't elements in common
(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

断言存在一个x不在x或lock_0不在x的元素lock_1。这种说法几乎是空洞的。它只是防止两个“集合”同时包含所有整数。您的评论表明您实际上是在尝试断言

(assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x)))))

也就是说，两个集合的交集都是空的。

其次，您说您期望/需要lock_0并且lock_2是空集，但是您断言

(assert (forall ((x Int)) (= (lock_0 x) (= x 2))))
(assert (forall ((x Int)) (= (lock_2 x)  (= x 1))))

这两个断言本质上说的lock_0是单例集{2}，并且lock_2是单例集{1}。

顺便说一句，如果我们更换

(assert (exists ((x Int)) (=> (lock_0 x) (not (lock_1 x)))))

和

(assert (forall ((x Int)) (or (not (lock_0 x)) (not (lock_1 x))))), (1)

在我们断言之后，问题变得微不足道

(assert (forall ((x Int)) (= (lock_0 x) (= x 2)))) (2)

(assert (forall ((x Int)) (= (lock_1 x) (= x 2)))) (3)

因为，(1) 是说lock_0并且lock_1没有共同的元素，并且 (2) 和 (3) 是说它们是单例集{2}。

编辑（额外问题）

如果我们想说那lock_0是空集，我们可以说它总是假的

(assert (forall ((x Int)) (not (lock_0 x))))

命令

(assert (forall ((x Int)) (= (lock_1 x) (or (= x 0) (= x 2)))))

断言那lock_1是 set {0, 2}。如果我们想说那lock_1是空集或集合{2}，我们应该断言：

(assert (or (forall ((x Int)) (not (lock_1 x))) 
            (forall ((x Int)) (= (lock_1 x) (= x 2)))))

要说它lock_1可能只包含值 2 和 3，我们应该断言：

(assert (forall ((x Int)) (=> (lock_1 x) (or (= x 2) (= x 3)))))

请注意，我使用的是蕴含 ( =>) 而不是相等。在这种情况下，我们有lock_1可能是以下集合之一：（{}空集）{2}、、、{3}或{2, 3}。

该命令define-fun不将函数作为参数。该命令define-fun只是定义一个宏。它不会为 Z3 增加任何额外的动力。

如果你想要一种更强大的语言来与 Z3 交互，你应该考虑 Z3Py，它是 Z3 的 Python 前端。这是一个使用 Z3Py 的示例（也可以在此处在线获得）。

# Declare a function from Int to Bool
lock_1 = Function('lock_1', IntSort(), BoolSort())
x = Int('x')

s = Solver()
# Assert that lock_1 is the empty set
s.add(ForAll(x, Not(lock_1(x))))
print(s.check())

# Declare a function that returns x*x if x is in s1 but not in s2
# Remark: example is a Python function that builds a Z3 expression.
def example(s1, s2, x):
    # Remark: the function If creates a Z3 if expression.
    return If(And(s1(x), Not(s2(x))), x*x, 0)

lock_2 = Function('lock_2', IntSort(), BoolSort())

s = Solver()
a = Int('a')
s.add(a == example(lock_1, lock_2, 3))
s.add(lock_1(3))
s.add(Not(lock_2(3)))
print(s)
print(s.check())
m = s.model()
print(m[a])

结束编辑