在 Z3Py 中索引 BitVec 的元素答案

【问题标题】：Index an element of BitVec in Z3Py在 Z3Py 中索引 BitVec 的元素
【发布时间】：2020-03-15 03:36:20
【问题描述】：

有没有办法索引BitVec 中的元素？我想要这样的东西：

s = Solver()
x = BitVec('x', 8)
s.add(Not(And(x[0], x[2])))

或者是屏蔽位的唯一方法：

s.add(x & 5 != 5)

【问题讨论】：

标签： z3 smt z3py

【解决方案1】：

您可以使用Extract(high, low, a) 从BitVec 类型的术语中提取一个或多个位。

例如

from z3 import *

s = Solver()
x = BitVec("x", 8)

x_0 = Extract(0, 0, x)
x_2 = Extract(2, 2, x)

expr = Or(x_0 == 0, x_2 == 0)

s.add(expr)

while s.check() == sat:
    m = s.model()
    print("Model: " + str(m))

    v_0 = m.eval(x_0)
    v_2 = m.eval(x_2)

    bl = Or(x_0 != v_0, x_2 != v_2)

    s.add(bl)

输出：

Model: [x = 4]    # 0000 0100
Model: [x = 0]    # 0000 0000
Model: [x = 1]    # 0000 0001

【讨论】：

优秀的答案！真的应该进入某种 Z3 常见问题解答。
@patricktrentin 太好了，你知道这是如何在内部表示的吗？具体来说，您的答案是否允许内部 SAT 表示？我想我的屏蔽方法s.add(x & 5 != 5) 会更慢，因为它会生成无用的子句。一个后续问题是如何在内部表示位向量？它们是整数还是原子？
@HiDefender AFAIK，您和我的解决方案都承认 SAT 表示，请参阅，例如，A Tale of Two Solvers: Eager and Lazy Approaches to Bit-vectors；我宁愿避免在不先进行小型实验的情况下对编码效率做出任何猜测；
@PatrickTrentin 对我当前的项目使用每种类型的约束进行了快速实验。像 [ (G[i] & BitVecVal(5, 12)) != BitVecVal(5, 12) for i in range(len(grapheme)) ] 这样的约束平均为 1.86 秒。像 [ Not(And(Extract(2, 2, G[i]) == 1, Extract(0, 0, G[i]) == 1)) for i in range(len(grapheme)) ] 这样的约束平均为 1.43 秒。