From 0bc8518cb5277e38b462c5a667945456ffb2e1b5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 7 Jan 2022 11:53:27 -0800 Subject: [PATCH] na Signed-off-by: Nikolaj Bjorner --- src/sat/smt/q_queue.cpp | 3 ++- src/smt/qi_queue.cpp | 4 +++- 2 files changed, 5 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp index c30009127..ff7dbc8ab 100644 --- a/src/sat/smt/q_queue.cpp +++ b/src/sat/smt/q_queue.cpp @@ -163,12 +163,13 @@ namespace q { m_stats.m_num_instances++; +#if 0 std::cout << "instantiate\n"; for (unsigned i = 0; i < num_bindings; ++i) std::cout << ctx.bpp(f[i]) << " "; std::cout << "\n"; std::cout << mk_pp(q, m) << "\n"; - +#endif // f.display(ctx, std::cout << mk_pp(f.q(), m) << "\n" << instance << "\n") << "\n"; diff --git a/src/smt/qi_queue.cpp b/src/smt/qi_queue.cpp index 7c21c1362..1cef2a0f1 100644 --- a/src/smt/qi_queue.cpp +++ b/src/smt/qi_queue.cpp @@ -245,13 +245,15 @@ namespace smt { return; } +#if 0 std::cout << "instantiate\n"; enode_vector _bindings(num_bindings, bindings); for (auto * b : _bindings) std::cout << enode_pp(b, m_context) << " "; std::cout << "\n"; std::cout << mk_pp(q, m) << "\n"; - +#endif + TRACE("qi_queue", tout << "simplified instance:\n" << s_instance << "\n";); stat->inc_num_instances(); if (stat->get_num_instances() % m_params.m_qi_profile_freq == 0) {