Function preprocess

tools/transform.cpp:398–444

}

static expr preprocess(const Transform &t, const set<expr> &qvars0,
                       const set<expr> &undef_qvars, expr &&e) {
  if (hit_half_memory_limit())
    return expr::mkForAll(qvars0, std::move(e));

  // eliminate all quantified boolean vars; Z3 gets too slow with those
  auto qvars = qvars0;
  unsigned num_qvars_subst = 0;
  for (auto I = qvars.begin(); I != qvars.end(); ) {
    auto &var = *I;
    if (!var.isBool()) {
      ++I;
      continue;
    }
    if (hit_half_memory_limit())
      break;

    expr t = e.subst(var, true);
    if (!t.eq(e)) {
      e = (t && e.subst(var, false)).simplify();
      ++num_qvars_subst;
    }
    I = qvars.erase(I);

    // Z3's subst is *super* slow; avoid exponential run-time
    if (++num_qvars_subst > 9)
      break;
  }

  if (config::disable_undef_input || undef_qvars.empty() ||
      hit_half_memory_limit())
    return expr::mkForAll(qvars, std::move(e));

  // manually instantiate undef masks
  map<expr, expr> instances({ { std::move(e), true } });

  for (auto &i : t.src.getInputs()) {
    if (auto in = dynamic_cast<const Input*>(&i))
      instantiate_undef(in, instances, i.getType(), 0);
  }

  expr insts(false);
  for (auto &[e, v] : instances) {
    insts |= expr::mkForAll(qvars, std::move(const_cast<expr&>(e))) && v;
  }
  return insts;
}


static expr