z3：如何将布尔类型转换为位向量排序

Question

我正在做x86指令的符号解释。例如，对于cmp指令，比较符号和操作数是否相等存储在eflags寄存器的两个位中。

这里是我的代码：

/* s1,s2 are source operands of sort bit-vector 
*  of 32 bits (defined somewhere else) 
* ctx is the context (defined somewhere else) 
* eflags is of sort bit-vector of 32 bits (initialized somewhere else) 
*/ 

#define ZF_INDEX 6 

Z3_ast ZF,OF,CF;    /* eflags bits */ 
ZF = Z3_mk_eq(ctx,s1,s2); 
Z3_ast zf_mask = Z3_mk_rotate_left(ctx, ZF_INDEX ,Z3_mk_zero_ext(ctx,31,ZF)); 
eflags = Z3_mk_bvand(ctx,eflags, zf_mask); 

的问题是，我不觉得在Z3 API任何功能，一个（假设的）布尔排序（ZF在我的例子）转换成位向量（任何长度）。

我曾想过用ZF上的ite语句创建一个函数，它会返回一个位向量，但我想知道传统的这样做的方法。

谢谢，

嘿嘿。

Answer 1

您所描述的ite方法是传统方式。