diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 55c916aa8..84f435fc2 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -128,10 +128,11 @@ namespace euf { n->unmark1(); TRACE("model", - for (auto const& d : deps.deps()) - if (d.m_value) { - tout << bpp(d.m_key) << ":\n"; - for (auto* n : *d.m_value) + for (auto * t : deps.deps()) { + auto* v = deps.get_dep(t); + if (v) { + tout << bpp(t) << ":\n"; + for (auto* n : *v) tout << " " << bpp(n) << "\n"; } ); diff --git a/src/util/top_sort.h b/src/util/top_sort.h index 46fe45446..2943b68b6 100644 --- a/src/util/top_sort.h +++ b/src/util/top_sort.h @@ -41,7 +41,6 @@ class top_sort { static T_set* add_tag(T_set* t) { return TAG(T_set*, t, 1); } static T_set* del_tag(T_set* t) { return UNTAG(T_set*, t); } - T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id())); } bool contains_partition(T* f) const { @@ -108,6 +107,8 @@ public: m_dep_keys.push_back(t); } + ptr_vector const& deps() { return m_dep_keys; } + void add(T* t, T* s) { T_set* tb = get_dep(t); if (!tb) { @@ -125,6 +126,9 @@ public: bool contains_dep(T* t) const { return m_deps.get(t->get_small_id(), nullptr) != nullptr; } + T_set* get_dep(T* t) const { return del_tag(m_deps.get(t->get_small_id(), nullptr)); } + + bool is_singleton_partition(T* f) const { unsigned pid = m_partition_id(f); return f == m_top_sorted[pid] &&