perf(kernel/metavar): improve performance of has_assigned_metavar by avoiding for_each+exception

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
Leonardo de Moura 2013-10-25 15:19:59 -07:00
parent 57d9d23bd4
commit ce10bfeaf6

View file

@ -256,25 +256,25 @@ expr instantiate_metavars(expr const & e, substitution const & s) {
} }
} }
struct found_assigned {};
bool has_assigned_metavar(expr const & e, substitution const & s) { bool has_assigned_metavar(expr const & e, substitution const & s) {
if (!has_metavar(e)) { if (!has_metavar(e)) {
return false; return false;
} else { } else {
bool result = false;
auto proc = [&](expr const & n, unsigned) { auto proc = [&](expr const & n, unsigned) {
if (result)
return false;
if (!has_metavar(n)) if (!has_metavar(n))
return false; return false;
if (is_metavar(n) && s.is_assigned(n)) if (is_metavar(n) && s.is_assigned(n)) {
throw found_assigned(); result = true;
return false;
}
return true; return true;
}; };
for_each_fn<decltype(proc)> visitor(proc); for_each_fn<decltype(proc)> visitor(proc);
try { visitor(e);
visitor(e); return result;
return false;
} catch (found_assigned&) {
return true;
}
} }
} }