Method concat

smt/expr.cpp:1862–1892

}

expr expr::concat(const expr &rhs) const {
  expr a, b, c, d;
  unsigned h, l, h2, l2;
  if (isExtract(a, h, l)) {
    if (rhs.isExtract(b, h2, l2) && l == h2+1) {
      if (a.eq(b))
        return a.extract(h, l2);

      // (concat (extract (concat const X)) (extract X))
      expr aa, ab;
      if (l2 == 0 && a.isConcat(aa, ab) && ab.eq(b) &&
          (h - aa.bits()) == b.bits())
        return aa.concat(b);
    }

    //  extract_l concat (concat extract_r foo)
    if (rhs.isConcat(b, c) && b.isExtract(d, h2, l2) && l == h2+1 && a.eq(d))
      return a.extract(h, l2).concat(c);
  }

  // (concat (concat x extract) extract)
  if (isConcat(a, b) && b.isExtract(c, h, l) && rhs.isExtract(d, h2, l2) &&
      l == h2+1 && c.eq(d))
    return a.concat(c.extract(h, l2));

  // (concat const (concat const2 x))
  if (isConst() && rhs.isConcat(a, b) && a.isConst())
    return concat(a).concat(b);

  return binop_fold(rhs, Z3_mk_concat);
}

expr expr::concat_zeros(unsigned bits) const {
  return bits ? concat(mkUInt(0, bits)) : *this;