Method factor

smt/exprs.cpp:195–245

// factor the common terms out
template<> AndExpr DisjointExpr<AndExpr>::factor() const {
  assert(!vals.empty());
  if (vals.size() == 1)
    return vals.begin()->first;

  AndExpr ret;
  vector<pair<AndExpr, expr>> vals2;
  vals2.insert(vals2.end(), vals.begin(), vals.end());

  vector<pair<set<expr>::iterator, set<expr>::iterator>> its;
  its.reserve(vals2.size());
  for (auto &v : vals2) {
    its.emplace_back(v.first.exprs.begin(), v.first.exprs.end());
  }

  auto &it0 = its[0].first;
  while (it0 != its[0].second) {
    const expr &e0 = *it0;
    bool in_all = true;
    for (unsigned i = 1, e = its.size(); i != e; ++i) {
      auto &it2 = its[i].first;
      if (it2 == its[i].second) {
        goto end;
      }
      auto cmp = *it2 <=> e0;
      if (cmp < 0) {
        ++it2;
        --i; // repeate this AndExpr
      } else if (cmp > 0) {
        ++it0;
        in_all = false;
        break;
      }
    }
    if (in_all) {
      ret.add(e0);
      unsigned i = 0;
      for (auto &v : vals2) {
        auto &it = its[i++].first;
        it = v.first.exprs.erase(it);
      }
    }
  }
end:
  DisjointExpr<expr> leftovers;
  for (auto &[v, domain] : vals2) {
    leftovers.add(std::move(v)(), std::move(domain));
  }
  ret.add(*std::move(leftovers)());
  return ret;
}


void FunctionExpr::add(const expr &key, expr &&val) {