z3 - 获取 Z3 中位向量的符号值

Question

我想使用 Z3 对位向量进行推理。除了可满足性决定之外，我还想要位向量的符号表示，以便我可以根据需要对它们应用我自己的计算。例如：

让，

1. X[3:0], Y[3:0], Z[4:0] 被声明为位向量而不初始化任何值
2. 打印 X[3:0]
3. X[3:0] <- X[3:0] >> 1（逻辑移位）
4. 打印 X[3:0]
5. Z[4:0] <- X[3:0] + Y[3:0]
6. 打印 Z[4:0]
7. …………

所需的输出（像这样的符号）：

> 2. [x3 x2 x1 x0]
> 4. [0 x3 x2 x1]
> 6. [s4 s3 s2 s1 s0]

使用Z3可以做到这一点吗？

Answer 1

一般来说，这是不可能的。简化公式后，Z3 使用了一个位冲击器（转换为布尔变量）并运行一个 SAT 求解器，它（通常）返回一个对所有布尔变量的赋值（因此，在转换之后，位向量变量）。

可以在这里看到 Z3 用于 QF_BV 公式的策略。对于某些（简单）公式，在您的情况下，在位爆破后提取公式可能就足够了；策略教程描述了如何构建和应用这些策略。