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

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-11-30 14:08:29 -08:00
parent b52fd8d954
commit 8a0dec1a4b
1 changed files with 7 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

12
src/util/dependency.h
View file

@ -100,7 +100,7 @@ private:
value_manager & m_vmanager; value_manager & m_vmanager;
allocator & m_allocator; allocator & m_allocator;
ptr_vector<dependency> m_todo; mutable ptr_vector<dependency> m_todo;
void inc_ref(value const & v) { void inc_ref(value const & v) {
if (C::ref_count) if (C::ref_count)
@ -138,7 +138,7 @@ private:
} }
} }
void unmark_todo() { void unmark_todo() const {
for (auto* d : m_todo) for (auto* d : m_todo)
d->unmark(); d->unmark();
m_todo.reset(); m_todo.reset();
@ -224,7 +224,7 @@ public:
void linearize(dependency * d, vector<value, false> & vs) { void linearize(dependency * d, vector<value, false> & vs) const {
if (!d) if (!d)
return; return;
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
@ -234,7 +234,7 @@ public:
m_todo.reset(); m_todo.reset();
} }
void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) { void linearize(ptr_vector<dependency>& deps, vector<value, false> & vs) const {
if (deps.empty()) if (deps.empty())
return; return;
SASSERT(m_todo.empty()); SASSERT(m_todo.empty());
@ -329,7 +329,7 @@ public:
return m_dep_manager.contains(d, v); return m_dep_manager.contains(d, v);
} }
void linearize(dependency * d, vector<value, false> & vs) { void linearize(dependency * d, vector<value, false> & vs) const {
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }
@ -338,7 +338,7 @@ public:
return vs; return vs;
} }
void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) { void linearize(ptr_vector<dependency>& d, vector<value, false> & vs) const {
return m_dep_manager.linearize(d, vs); return m_dep_manager.linearize(d, vs);
} }