Method DisjointExpr

smt/exprs.cpp:124–192

template<>
DisjointExpr<expr>::DisjointExpr(const expr &e, unsigned depth_limit) {
  if (depth_limit-- == 0) {
    add(e, expr(true));
    return;
  }

  vector<pair<expr, expr>> worklist = { {e, true} };
  expr cond, then, els, a, b;
  unsigned high, low;

  do {
    // Limit exponential growth
    if ((worklist.size() + vals.size()) >= 32 ||
        hit_half_memory_limit()) {
      for (auto &[v, c] : worklist) {
        add(std::move(v), std::move(c));
      }
      break;
    }

    auto [v, c] = worklist.back();
    worklist.pop_back();

    if (v.isIf(cond, then, els)) {
      worklist.emplace_back(std::move(then), c && cond);
      worklist.emplace_back(std::move(els), c && !cond);
    }
    else if (v.isConcat(a, b)) {
      DisjointExpr<expr> lhs(a, depth_limit);
      DisjointExpr<expr> rhs(b, depth_limit);
      if (lhs.size() == 1 && rhs.size() == 1) {
        add(std::move(v), std::move(c));
        continue;
      }

      for (auto &[lhs_v, lhs_domain] : lhs) {
        if (auto rhs_val = rhs.lookup(lhs_domain)) {
          add(lhs_v.concat(*rhs_val), c && lhs_domain);
        } else {
          expr from;
          bool negate = true;
          if (!lhs_domain.isNot(from)) {
            from = lhs_domain;
            negate = false;
          }

          for (auto &[rhs_v, rhs_domain] : rhs) {
            add(lhs_v.concat(simplify(rhs_v, from, negate)),
                c && lhs_domain && rhs_domain);
          }
        }
      }
    }
    else if (v.isExtract(a, high, low)) {
      DisjointExpr<expr> vals(a, depth_limit);
      if (vals.size() == 1) {
        add(std::move(v), std::move(c));
        continue;