如何在 SMT (Z3) 中对变量交换建模？

Question

我有一个对变量进行排序的程序，我正在尝试使用 Z3 检查它的有效性，但是我有一个代码段在其中交换变量，但我不知道如何在 SMT 语法中对其建模.这是原始代码段：

if (x > y) {
  temp = x;
  x = y;
  y = temp;
}

关于SMT，我写了一个断言，但我想这并不完全正确：

(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun temp () Int)

(assert (=> (> s1 s2) (and (= tmp s1) (= s1 s2) (= s2 tmp))))

对如何在 SMT 中进行变量赋值有任何想法吗？

Answer 1

我们可以使用单个表达式作为元组重写您想要的内容：

(result1, result2) = x > y ? (x, y) : (y, x)

Z3 支持元组，但我对此经验不足。将其分解成多个部分可能更容易：

result1 = x > y ? x : y
result2 = x > y ? y : x

并且 ?: 运算符映射到 Z3 中的 ITE。

您甚至不需要 "temp variables"（但显然您可以）。

(assert (=> (> s1 s2) (and (= tmp s1) (= s1 s2) (= s2 tmp))))

我认为这表明您不了解 Z3 "variables" 实际上是常量，您实际上不能交换它们。在每个模型中，它们只取一个值。常量没有时间成分。 = 表示 "is equal?" 而不是 "make it equal!"。

Answer 2

您应该查看单一静态分配 [1]。这样你就可以改写你原来的代码如下。

if (x0 > y0) {
  temp0 = x0;
  x1 = y0;
  y1 = temp0;
}

很明显，您有两个不同的 x 和 y 实例。第一个 (x0, y0) 是您在 if 条件下比较的那个。第二个 (x1, y1) 是运算的结果。

这引入了隐含的时间概念，使编写有关代码的属性也变得更加容易。例如，

  ((x1 = x0) & (y1 = y0)) | ((x1 = y0) | (y1 = x0))

当然，这可能需要调整代码的其他部分，以便使用正确的变量。

How to model variable swap in SMT (Z3)?