Method isExtract

smt/expr.cpp:503–512

}

bool expr::isExtract(expr &e, unsigned &high, unsigned &low) const {
  if (auto app = isAppOf(Z3_OP_EXTRACT)) {
    e = Z3_get_app_arg(ctx(), app, 0);
    auto d = decl();
    high = Z3_get_decl_int_parameter(ctx(), d, 0);
    low = Z3_get_decl_int_parameter(ctx(), d, 1);
    return true;
  }
  return false;
}

bool expr::isSignExt(expr &val) const {
  return isUnOp(val, Z3_OP_SIGN_EXT);