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方法是傳統方式。