Bit Vectors
比特向量：
- 数据结构
- 建模/性质推理
先看一个著名的BUG：
bug原因：
int mid = (low+high)/2;
这会造成溢出问题
如何解决？
int mid = low +(high+low)/2 ？ ×
比特向量
一个比特向量b是一个具有 l （是一个常数）长度的0或1的序列
语法
o 代表二元运算
语义
对于一个解释器 < b > ，我们可以看到，b的解释，可以按照无符号整型解释，也可以按照有符号整型解释，这会得到不同的解释结果
对于我们不熟悉的系统，把问题通过解释器映射到我们熟悉的模型中，然后再去解决问题，这是一个很重要的思路，比如把比特向量解释到整数域中
决策过程
对于给定的比特向量a,b,c，可以分别展开为 l 位，如下所示
通过比特爆炸算法，将其转化为布尔值的序列，然后再生成约束，扔进SAT求解器
Incremental Bit Blasting
我们先处理较容易求解的部分，如果不满足条件，则后面就不用再求解了
比特向量的应用：费马大定理
我们通过添加约束来限制位数
为什么要a&magic == 0？？？