From e31926d1321ab65abb3b024251f21345651ea20b Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 1 Aug 2022 12:08:38 +0200 Subject: [PATCH] var_queue display --- src/util/var_queue.h | 18 +++++++++++++++++- 1 file changed, 17 insertions(+), 1 deletion(-) diff --git a/src/util/var_queue.h b/src/util/var_queue.h index e5a21d9a4..62df77784 100644 --- a/src/util/var_queue.h +++ b/src/util/var_queue.h @@ -52,7 +52,7 @@ public: void mk_var_eh(var v) { m_queue.reserve(v+1); - m_queue.insert(v); + unassign_var_eh(v); } void del_var_eh(var v) { @@ -76,5 +76,21 @@ public: var min_var() { SASSERT(!empty()); return m_queue.min_value(); } bool more_active(var v1, var v2) const { return m_queue.less_than(v1, v2); } + + std::ostream& display(std::ostream& out) const { + bool first = true; + for (auto v : m_queue) { + if (first) { + first = false; + } else { + out << " "; + } + out << v; + } + return out; + } }; +inline std::ostream& operator<<(std::ostream& out, var_queue const& queue) { + return queue.display(out); +}