z3 - Z3 中的不同值

Question

我想问一个关于在 Z3 中分配不同值的问题。

假设我有 6 个变量 A、B、C、D、E、F。现在，我想为其中一些分配不同的值，其中一些将为零。有多少变量是不同的，有多少变量为零，事先是未知的。这取决于某些其他条件。

通常对于我要写的所有变量

(assert (distinct A B C D E F))

但是，是否可以编写诸如A, B, D为零而其他不同的约束？再次记住，这A,B, D只是示例变量。它们可以根据约束动态变化。

谢谢 ！

Answer 1

据我了解，您有一组V变量v ₁，...，v _n，其中每个变量v _i要么为零，要么与所有其他变量v _j， j ≠ i不同。

例如，让V = {a, b, c, d}.

(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(declare-const d Int)

您可以将约束编码为

(assert (or (= a 0) (not (or (= a b) (= a c) (= a d)))))
(assert (or (= b 0) (not (or (= b a) (= b c) (= b d)))))
(assert (or (= c 0) (not (or (= c a) (= c b) (= c d)))))
(assert (or (= d 0) (not (or (= d a) (= d b) (= d c)))))

添加两个约束并查询 Z3 的模型

(assert (= a 0))
(assert (not (= b 0)))

(check-sat)
(get-model)

然后产生

sat
(model 
  (define-fun b () Int
    (- 2))
  (define-fun c () Int
    (- 1))
  (define-fun d () Int
    0)
  (define-fun a () Int
    0)
)

由于生成“零或不同”约束是一项繁琐的任务，您可能希望使用诸如 PyZ3 或 Scala^Z3 之类的 Z3 前端。