z3 - 在 Z3Py 中索引 BitVec 的一个元素
问题描述
有没有办法索引 a 中的元素BitVec
?我想要这样的事情:
s = Solver()
x = BitVec('x', 8)
s.add(Not(And(x[0], x[2])))
或者是屏蔽隔离位的唯一方法:
s.add(x & 5 != 5)
解决方案
您可以使用从类型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
推荐阅读
- cmake - 无法在 Debug / X64 的 Visual Studio 中调试 googletests
- python - pandas 中的“复制”参数是否按预期工作?
- python - 尝试连接到 API 并打开 MySQL 端口以便它可以工作,但终端只是挂起
- javascript - 使用javascript从表中删除列
- java - 如何在 Quartz Scheduler 中使用 JDBC 作业存储
- reactjs - 使用 react-window 防止 DOM 元素在虚拟化树组件中重新渲染
- php - Codeigniter 中的会话有什么问题?
- php - 使用 PHP 在 mysql 表中添加数据时出错
- oracle12c - 将行转置到转置列基于另一列发生变化的列
- javascript - Vuejs如何创建一个新数组以传递给图形