1

是否有任何用于位向量（QF_BV 逻辑）的工具，它将象征性地执行操作并根据位向量的符号值返回输出，以便我可以根据需要对它们应用我自己的计算？或者是否有任何 SMT 求解器可以在位爆破后提取变量的符号值？例如：

让，

  1. X[3:0], Y[3:0], Z[4:0], W[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. 打印 Y[3:0]
  8. W[4:0] <- Y[3:0] + 0000
  9. 打印 W[4:0]
  10. …………

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

2. [x3 x2 x1 x0]
4. [0 x3 x2 x1]
6. [s4 s3 s2 s1 s0]
7. [y3 y2 y1 y0]
9. [0 y3 y2 y1 y0]
4

0 回答 0