如何在Python中根据另一个变量来增加Z3变量？

Question

我正在编写一个 Z3 Python 脚本，我试图根据涉及另一个变量

y

的条件来更改变量

x

。这是问题的简化版本：

from z3 import *

x = BitVec('x', 64)
y = BitVec('y', 64) # or y = BitVecVal(0, 64)

solver = Solver()
solver.add(x > 5555)

lsvec = [...] 

for i in range(1, 64):
    for j in range(i, 64):
        solver.add(y == If(x > 0, y + 1, y)) # I want to increment y if x > 0
        # Of course don't work because y == y + 1 cannot be satisfied
if solver.check() == sat:
        model = solver.model()
        x_value = model[x].as_long()    
        y_value = model[y].as_long()

目标是如果

y

则增加

x > 0

。然而，目前的表述存在一些无法令人满意的问题。

我正在寻求有关如何使用 Z3 基于

y

的值和其他条件正确建模

x

的条件增量的指导。

实际上，我正在尝试解决类似于下面的函数。然而，我在 XOR 运算中遇到了同样的问题。

def f_evaluate2(x, bits):
    y = 0
    cursor = 0
    for i in range(1, bits + 1):  # 1-64
        for j in range(i, 65):
            if (x & (1 << (64 - i))) and (x & (1 << (64 - j))):
                y ^= lsvec[cursor] # unsat
            cursor += 1

    return y

任何关于如何在 Z3 中处理这些类型的约束的建议或示例将不胜感激！

预先感谢您的协助。

Answer 1

这种事情在符号编程和代码生成/编译器算法中经常发生。标准解决方案是使用所谓的“静态单赋值形式”，又名 SSA。请参阅 https://en.wikipedia.org/wiki/Static_single-assignment_form 进行讨论。

基本思想是首先编写算法，以便每个变量仅分配一次。您可以通过为现有变量的每次赋值创建一个新变量来实现此目的。所以，就你而言：

y = y + 1

将变成：

y1 = y + 1

然后使用

y1

作为下一个对

y

的引用。当您有条件时，您可以根据条件“合并”作业。 （所谓的 Φ 函数。）当你有一个循环时，你“展开”循环，这需要你知道循环将迭代多少次（或至少迭代次数的上限），这样你就可以即时展开。

您可以计算主导节点以最小化 SSA 表示。幸运的是，一般情况下您并不总是需要这样做：大多数时候您可以简单地线性化代码并即时进行转换，假设问题的控制结构足够简单。

这是一个简单的例子，使用你关于建模的问题

y = if x > 0 then y+1 else y

你可以写成：

y1 = If(x > 0, y+1, y)`

并在后续表达式中使用

y1

。

希望这能让您开始。翻译命令式程序以使其符号友好可能会很棘手，但如果您专门使用 SSA 风格，那么您应该会更容易。 （即，首先以 SSA 形式编写原始程序，一旦确定它是正确的，然后将其转换为约束。）