From ca05c668479d25cc5ae8496b068de16a988e3d91 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 6 Jul 2021 14:20:03 +0200 Subject: [PATCH] #5376 --- src/smt/qi_queue.cpp | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 875c728a4..26beb883f 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -387,7 +387,7 @@ namespace smt { bool result = true; for (unsigned i = 0; i < sz; 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) { TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); @@ -401,9 +401,11 @@ namespace smt { } bool result = true; + bool has_delayed = false; for (unsigned i = 0; i < m_delayed_entries.size(); i++) { entry & e = m_delayed_entries[i]; 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) { TRACE("qi_queue", tout << "lazy quantifier instantiation...\n" << mk_pp(static_cast(e.m_qb->get_data()), m) << "\ncost: " << e.m_cost << "\n";); @@ -413,6 +415,20 @@ namespace smt { 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(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; }