Method get_apps_of

smt/expr.cpp:2408–2430

}

set<expr> expr::get_apps_of(const char *fn_name, const char *prefix) const {
  C();
  vector<expr> worklist = { *this };
  unordered_set<Z3_ast> seen;
  set<expr> ret;
  do {
    auto val = std::move(worklist.back());
    worklist.pop_back();

    for (unsigned i = 0, e = val.getFnNumArgs(); i < e; ++i) {
      expr arg = val.getFnArg(i);
      if (arg.isApp() && seen.emplace(arg()).second)
        worklist.emplace_back(std::move(arg));
    }

    auto str = val.fn_name();
    if (str == fn_name || str.starts_with(prefix)) {
      ret.emplace(std::move(val));
    }
  } while (!worklist.empty());

  return ret;
}

void expr::printUnsigned(ostream &os) const {
  os << numeral_string();