mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-10 19:27:06 +00:00
Code Activity

na

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-06-08 07:00:59 -07:00
parent 51ed13f96a
commit 80604c7bc5
2 changed files with 10 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/sat/smt/euf_model.cpp
View file

@ -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";
}
);

6
src/util/top_sort.h
View file

@ -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<T> 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] &&