mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 14:17:47 +00:00
Code Activity

templatize vector for dependencies

Browse source
This commit is contained in:
Nikolaj Bjorner 2026-05-16 16:19:38 -07:00
parent d99f0ce230
commit 1198d9aaa5
1 changed files with 16 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

23
src/util/dependency.h
View file

@ -47,7 +47,8 @@ public:
value const& leaf_value() const { SASSERT(is_leaf()); return static_cast<leaf const*>(this)->m_value; } value const& leaf_value() const { SASSERT(is_leaf()); return static_cast<leaf const*>(this)->m_value; }
}; };
static void linearize_todo(ptr_vector<dependency>& todo, vector<value, false>& vs) { template <bool T = false>
static void linearize_todo(ptr_vector<dependency>& todo, vector<value, T>& vs) {
unsigned qhead = 0; unsigned qhead = 0;
while (qhead < todo.size()) { while (qhead < todo.size()) {
dependency* d = todo[qhead]; dependency* d = todo[qhead];
@ -69,7 +70,8 @@ public:
d->unmark(); d->unmark();
} }
static void s_linearize(dependency* d, vector<value, false>& vs) { template <bool T = false>
static void s_linearize(dependency* d, vector<value, T>& vs) {
if (!d) if (!d)
return; return;
ptr_vector<dependency> todo; ptr_vector<dependency> todo;
@ -223,10 +225,11 @@ public:
} }
template <bool T = false>
void linearize(dependency * d, vector<value, false> & vs) const { void linearize(dependency * d, vector<value, T> & vs) const {
if (!d) if (!d)
return; return;
std::cout << "linearize " << this << " " << d << "\n";
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
d->mark(); d->mark();
m_todo.push_back(d); m_todo.push_back(d);
@ -234,7 +237,8 @@ public:
m_todo.reset(); m_todo.reset();
} }
void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) const { template <bool T = false>
void linearize(ptr_vector<dependency>& deps, vector<value, T> & vs) const {
if (deps.empty()) if (deps.empty())
return; return;
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
@ -329,16 +333,19 @@ public:
return m_dep_manager.contains(d, v); return m_dep_manager.contains(d, v);
} }
void linearize(dependency * d, vector<value, false> & vs) const { template<bool T = false>
void linearize(dependency * d, vector<value, T> & vs) const {
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }
static vector<value, false> const& s_linearize(dependency* d, vector<value, false>& vs) { template <bool T = false>
static vector<value, T> const& s_linearize(dependency* d, vector<value, T>& vs) {
dep_manager::s_linearize(d, vs); dep_manager::s_linearize(d, vs);
return vs; return vs;
} }
void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) const { template <bool T = false>
void linearize(ptr_vector<dependency>& d, vector<value, T> & vs) const {
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }