Перегрузка оператора предиката оператора Z3 C++ не имеет неподписанной операции

Question

Я смотрел документ класса expr из Z3 C++ API по следующей ссылке http://research.microsoft.com/en-us/um/redmond/projects/z3/classz3_1_1expr.html.

Я нашел, что для оператора предиката, такого как «>», «> =» и «< =», для вектора бит он выполнил только подписанную операцию. Например, в оператор «> =», исходный код

{ 
     check_context(a, b); 
     Z3_ast r; 
     if (a.is_arith() && b.is_arith()) { 
      r = Z3_mk_ge(a.ctx(), a, b); 
     } 
     else if (a.is_bv() && b.is_bv()) { 
      r =Z3_mk_bvsge(a.ctx(), a, b);//This statement only did signed version, there actually is a Z3_mk_bvuge in C API 
     } 
     else { 
      assert(false); 
     } 
     a.check_error(); 
     return expr(a.ctx(), r); 
} 

Означает ли это, если я хочу, чтобы различать подписанные и неподписанные операции я могу использовать только C API? .

Answer 1

г ++ ч Файл содержит определения (Shorthands) для использования неподписанных бит-векторных операций, например:

/** 
    \brief unsigned less than or equal to operator for bitvectors. 
    */ 
    inline expr ule(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvule(a.ctx(), a, b)); }