我正在对 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 语句的函数，该语句将返回一个位向量，但我想知道这样做的传统方式。
谢谢，
海吉。