mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 13:28:47 +00:00
Code Activity

#5376

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-07-06 14:20:03 +02:00
parent 8a33391708
commit ca05c66847
1 changed files with 17 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
src/smt/qi_queue.cpp
View file

@ -387,7 +387,7 @@ namespace smt {
bool result = true; bool result = true;
for (unsigned i = 0; i < sz; i++) { for (unsigned i = 0; i < sz; i++) {
entry & e = m_delayed_entries[i]; entry & e = m_delayed_entries[i];
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << " min-cost: " << min_cost << ", instantiated: " << e.m_instantiated << "\n";);
if (!e.m_instantiated && e.m_cost <= min_cost) { if (!e.m_instantiated && e.m_cost <= min_cost) {
TRACE("qi_queue", TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";);
@ -401,9 +401,11 @@ namespace smt {
} }
bool result = true; bool result = true;
bool has_delayed = false;
for (unsigned i = 0; i < m_delayed_entries.size(); i++) { for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
entry & e = m_delayed_entries[i]; entry & e = m_delayed_entries[i];
TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";); TRACE("qi_queue", tout << e.m_qb << ", cost: " << e.m_cost << ", instantiated: " << e.m_instantiated << "\n";);
has_delayed |= !e.m_instantiated;
if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) { if (!e.m_instantiated && e.m_cost <= m_params.m_qi_lazy_threshold) {
TRACE("qi_queue", TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";);
@ -413,6 +415,20 @@ namespace smt {
instantiate(e); instantiate(e);
} }
} }
if (result && has_delayed) {
for (unsigned i = 0; i < m_delayed_entries.size(); i++) {
entry& e = m_delayed_entries[i];
if (e.m_instantiated)
continue;
TRACE("qi_queue",
tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast<quantifier*>(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";);
result = false;
m_instantiated_trail.push_back(i);
m_stats.m_num_lazy_instances++;
instantiate(e);
break;
}
}
return result; return result;
} }