Method extract

smt/expr.cpp:1898–1992

}

expr expr::extract(unsigned high, unsigned low, unsigned depth) const {
  C();
  assert(high >= low && high < bits());

  if (low == 0 && high == bits()-1)
    return *this;

  if (depth-- == 0)
    goto end;

  {
    expr sub;
    unsigned high_2, low_2;
    if (isExtract(sub, high_2, low_2))
      return sub.extract(high + low_2, low + low_2);
  }
  if (low == 0) {
    expr val;
    if (isSignExt(val)) {
      auto val_bits = val.bits();
      if (high < val_bits)
        return val.extract(high, 0);
      return val.sext(high - val_bits + 1);
    }
  }
  {
    expr a, b;
    if (isAShr(a, b)) {
      uint64_t shift;
      if (b.isUInt(shift) && shift < a.bits() && high + shift < a.bits())
        return a.extract(high + shift, low + shift);
    }
  }
  {
    expr a, b;
    if (isConcat(a, b)) {
      auto b_bw = b.bits();
      if (high < b_bw)
        return b.extract(high, low);
      if (low >= b_bw)
        return a.extract(high - b_bw, low - b_bw);
      if (low == 0)
        return a.extract(high - b_bw, 0).concat(b);
      if (a.isConst() || b.isConst())
        return a.extract(high - b_bw, 0).concat(b.extract(b_bw-1, low));
    }
  }
  {
    expr cond, then, els;
    if (isIf(cond, then, els)) {
      then = then.extract(high, low, depth);
      els = els.extract(high, low, depth);
      if (then.eq(els))
        return then;
      if (then.isConst() && els.isConst())
        return mkIf(cond, then, els);
    }
  }