【发布时间】：2015-09-15 20:09:22
【问题描述】：
我有许多针对 BitVec 中的位断言的约束，我想知道为 BitVec 中的特定位断言约束的最有效方法是什么？
假设我想断言 BitVec 中的第 5 位为 1，有没有比这更有效（检查时间更短）的方法？
bitvec = BitVec('bitvec',10)
s.add(Extract(5,5,bitvec)==1)
【问题讨论】：
【发布时间】：2015-09-15 20:09:22
【问题描述】：
根据我对 Z3 内部结构的了解（通过实验和查看源代码），这是最有效的方法。
据我了解，提取和连接没有求解器运行时成本。他们只是将这些位分成几部分。
唯一的选择是应用and 操作来提取位。但这应该在简化后变成一个提取物（实际上您可以通过运行简化策略来测试它。这是一个有趣的重写观察）。
【讨论】：
-
这很好，我会尝试按位应用并提取位。谢谢。