在 Z3Py 中索引 BitVec 的一个元素

Question

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

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

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

s.add(x & 5 != 5)

Answer 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

在 Z3Py 中索引 BitVec 的一个元素

Index an element of BitVec in Z3Py

smt

z3

z3py