z3 - 使用 Z3 的程序可满足性

Question

如何使用 Z3 检查程序的可满足性？例如：

Boolean x, y
while(x is False) {
    x = x or y
    y = x & y
}
y = x or y

Answer 1

您可以将程序表示为一组 Horn 子句。对于您的程序，您可以将其表示如下：

 (set-logic HORN)
 (set-option :fixedpoint.engine bmc)

 (declare-fun L0 (Bool Bool) Bool)
 (declare-fun L1 (Bool Bool) Bool)
 (declare-fun L2 (Bool Bool) Bool)
 (declare-fun L3 (Bool Bool) Bool)
 (assert (forall ((x Bool) (y Bool)) (L0 x y)))   ; all values of x,y are possible at L0
 (assert (forall ((x Bool) (y Bool)) (=> (L0 x y) (L1 x y)))) ; from L0 move to L1 without changing x, y
 (assert (forall ((x Bool) (y Bool) (x1 Bool) (y1 Bool)) 
     (=> (and (not x) (L1 x y) (= x1 (or x y)) (= y1 (and x1 y))) (L1 x1 y1)))); assignment in while loop
 (assert (forall ((x Bool) (y Bool)) (=> (and x (L1 x y)) (L2 x y))))         ; exit while loop
 (assert (forall ((x Bool) (y Bool)) (=> (L2 x y) (L3 x (or x y)))))        ; assignment after while loop

 (assert (forall ((x Bool) (y Bool)) (=> (L3 true true) false)))            ; say x = true, y = true is unreachable.
 (check-sat)

我添加了最后一个断言来做出可达性声明。我还指示 Z3 使用 BMC 引擎通过有界模型检查来展开 Horn 子句。其他引擎也可用，例如 PDR/IC3 引擎（set-option :fixedpoint.engine pdr），不展开转换关系。

现在，与展开的过渡关系的合取相比，Horn 子句的可达性与可满足性的含义将有所不同：上述子句是 UNSAT。这实际上对应于从 L0 到 (L3 true true) 的可行路径。如果您将最后一条语句更改为 (L3 true false)，您将得到答案“sat”（BMC 问题是 UNSAT）。虽然 BMC 本身不会以这样的循环终止，但事实证明，最后的转换和循环退出条件足以消除 (L3 true false) 的可能性，因此 Z3 通过预处理 horn 子句来解决这个问题。

当然，您也可以写下您拥有的程序语句的转换关系，然后自己将其直接展开为您检查可满足性的逻辑公式。