mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

var_queue display

Browse source
This commit is contained in:
Jakob Rath 2022-08-01 12:08:38 +02:00 committed by Nikolaj Bjorner
parent 6a929f91c8
commit e31926d132
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/util/var_queue.h
View file

@ -52,7 +52,7 @@ public:
void mk_var_eh(var v) { void mk_var_eh(var v) {
m_queue.reserve(v+1); m_queue.reserve(v+1);
m_queue.insert(v); unassign_var_eh(v);
} }
void del_var_eh(var v) { void del_var_eh(var v) {
@ -76,5 +76,21 @@ public:
var min_var() { SASSERT(!empty()); return m_queue.min_value(); } 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); } 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);
}