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 = []和lock_1 = [2]和lock_2 = [1]和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 中。这种说法几乎是空洞的。它只是防止两个“集合”同时包含所有整数。您的 cmets 表明您实际上是在尝试断言

(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 是集合{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 的示例（也可以在线获取 here）。

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

结束编辑