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 方法是传统方法。