mk_bvshl method

Z3_ast mk_bvshl(
  1. Z3_context c,
  2. Z3_ast t1,
  3. Z3_ast t2
)

\brief Shift left.

It is equivalent to multiplication by \ccode{2^x} where \c x is the value of the third argument.

NB. The semantics of shift operations varies between environments. This definition does not necessarily capture directly the semantics of the programming language or assembly architecture you are modeling.

The nodes \c t1 and \c t2 must have the same bit-vector sort.

def_API('Z3_mk_bvshl', AST, (_in(CONTEXT), _in(AST), _in(AST)))

Implementation

Z3_ast mk_bvshl(
  Z3_context c,
  Z3_ast t1,
  Z3_ast t2,
) {
  return _mk_bvshl(
    c,
    t1,
    t2,
  );
}