期待 unsat 而不是坐在 Z3答案

【问题标题】：Expecting unsat instad of sat in Z3期待 unsat 而不是坐在 Z3
【发布时间】：2022-07-28 00:44:15
【问题描述】：

我正面临一种情况，我希望从 Z3 获得 UNSAT，但我却获得了 SAT。

以下是我认为 Z3 的 4 个约束：

1. (i = 0) ==> (forall j: 0 <= j < n ==> a[j] = b[j])

2. (i = 1) ==> (exists j: 0 <= j < n ==> a[j] != b[j])

3. i = 0

4. a[0] != b[0]

这显然应该是 UNSAT。因为根据 1 和 3，我们得出结论，数组的 a 和 b 在每个索引中都应该相等。因此a[0] 不能不等于b[0]。

这是上述每个约束的Z3_ast_to_string(...)（我使用的是 C API）的输出：

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000)))))
      (a!2 (forall ((fqv Int))
             (let ((a!1 (concat (select fqv #x00000003)
                                (concat (select fqv #x00000002)
                                        (concat (select fqv #x00000001)
                                                (select fqv #x00000000))))))
               (=> (and (bvsle #x00000000 a!1) (bvslt a!1 #x00000005))
                   (= (select a a!1) (select b a!1)))))))
  (=> (= #x00000000 a!1) a!2))

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000)))))
      (a!2 (exists ((eqv Int))
             (let ((a!1 (concat (select eqv #x00000003)
                                (concat (select eqv #x00000002)
                                        (concat (select eqv #x00000001)
                                                (select eqv #x00000000))))))
               (and (bvsle #x00000000 a!1)
                    (bvslt a!1 #x00000005)
                    (not (= (select a a!1) (select b a!1))))))))
  (=> (= #x00000001 a!1) a!2))

(let ((a!1 (concat (select memcmp_return_value #x00000003)
                   (concat (select memcmp_return_value #x00000002)
                           (concat (select memcmp_return_value #x00000001)
                                   (select memcmp_return_value #x00000000))))))
  (= #x00000000 a!1))

(let ((a!1 (concat (select a #x00000003)
                   (concat (select a #x00000002)
                           (concat (select a #x00000001) (select a #x00000000)))))
      (a!2 (concat (select b #x00000003)
                   (concat (select b #x00000002)
                           (concat (select b #x00000001) (select b #x00000000))))))
  (not (= a!1 a!2)))

注意memcmp_return_value代表i，fqv代表forall量化变量，eqv代表存在量化变量。

Z3_ast 的创建有什么问题吗？为什么这会给我SAT？

【问题讨论】：

你需要发布z3返回给你的模型是什么。请注意，memcmp_return_value 不能是 i，因为它在 select 语句中用作数组。一定是别的东西。

标签： z3 smt formal-verification

【解决方案1】：

您确实需要发布z3推测的模型。但似乎 z3 在那里打印的内容与您的叙述不符。

看看 (1)。 a!1 的值是多少？看起来它是数组 mem_cmp_return_value 中前 4 个值的串联，伪代码：

      memcmp_return_value[3:0]

这与您声称memcmp_return_value 对应于i 的说法相矛盾，因为它被清楚地用作数组。你暂时忽略了这一点，然后说：

  (and (bvsle #x00000000 a!1) (bvslt a!1 #x00000005))

这表示此串联必须小于 5。z3 可以轻松选择不正确的数组，这使得 (1) 空虚为真。

我也看到其他类似的问题。

看起来您的 C/C++ 程序混淆了那里的一些变量；最好用n 明确表示。

长话短说，如果不查看生成这些约束的程序，就无法回答。但是您向我们展示的部分与您给出的叙述不符；看起来这确实是 SAT，因为您将数组的长度 (n) 与存储在数组本身中的值的串联混为一谈。

【讨论】：