z3 - Z3 或 Smt2 的 While 循环

Question

如何将简单的 while 循环(c 代码)转换为 smt2 语言或 z3？
例如:

int x,a;
while(x > 10 && x < 100){
    a = x + a;
    x++;
}

Answer 1

SMT 求解器的输入语言是一阶逻辑(带有理论)，因此没有循环等计算操作的概念。

你可以

要么使用循环不变量对任意循环迭代(以及循环的前后状态)进行编码，并证明与该任意迭代相关的属性，这就是演绎程序验证器(例如 Boogie、Dafny 或 Viper)所做的

或者，如果迭代次数是静态已知的，则展开循环并基本上使用单个静态分配形式来编码不同的展开

对于您的循环，后者将如下所示(这里没有使用正确的 SMT 语法，因为我很懒惰):

declare x0, a0 // initial values
declare a1, x1 // values after first unrolling
x0 > 10 && x0 < 100 ==> a1 == a0 + x0 && x1 == x0 + 1
declare a2, x2 // values after second unrolling
x1 > 10 && x1 < 100 ==> a2 == a1 + x1 && x2 == x1 + 1
...