mk_extract method

Z3_ast mk_extract(
  1. Z3_context c,
  2. int high,
  3. int low,
  4. Z3_ast t1,
)

\brief Extract the bits \c high down to \c low from a bit-vector of size \c m to yield a new bit-vector of size \c n, where \ccode{n = high - low + 1}.

The node \c t1 must have a bit-vector sort.

def_API('Z3_mk_extract', AST, (_in(CONTEXT), _in(UINT), _in(UINT), _in(AST)))

Implementation

Z3_ast mk_extract(
  Z3_context c,
  int high,
  int low,
  Z3_ast t1,
) {
  return _mk_extract(
    c,
    high,
    low,
    t1,
  );
}