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 в моем примере) в битовом вектор (любой длины).

Я подумал о создании функции с выражением ite на ZF, которая вернет бит-вектор, но я хотел бы знать, как это делается .

С благодарностью,

Хейджи.

Answer 1

Подход ite, который вы описали, является традиционным способом.