1
私はx86命令の象徴的な解釈をしています。たとえば、cmp命令の場合、比較の符号とオペランドが等しいかどうかは、eflagsレジスタの2ビットに格納されます。ここでz3：ブールソートをビットベクトルソートに変換する方法
は私のコードです：
/* 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);
問題は、私は、ビットベクター（仮定）ブールソート（私の例ではZF）に変換するZ3 APIで任意の関数が見つからないということです（任意の長さの）。
私は、ビットベクトルを返すZFのiteステートメントを使用して関数を作成することを考えましたが、伝統的な方法を知りたいと思います。
ありがとう、
Heyji。