From 9f2bafbf10d44e5395c42666b5fbc95dbafcebc0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Jul 2018 08:52:13 -0700 Subject: [PATCH] tidy model generator Signed-off-by: Nikolaj Bjorner --- src/smt/smt_model_generator.cpp | 71 +++++++++++++++------------------ src/smt/smt_model_generator.h | 10 +++-- src/smt/theory_datatype.cpp | 1 + 3 files changed, 39 insertions(+), 43 deletions(-) diff --git a/src/smt/smt_model_generator.cpp b/src/smt/smt_model_generator.cpp index 5417785d6..190f7f79e 100644 --- a/src/smt/smt_model_generator.cpp +++ b/src/smt/smt_model_generator.cpp @@ -28,6 +28,15 @@ Revision History: namespace smt { + void fresh_value_proc::get_dependencies(buffer& result) { + result.push_back(model_value_dependency(m_value)); + } + + std::ostream& operator<<(std::ostream& out, model_value_dependency const& src) { + if (src.is_fresh_value()) return out << "fresh!" << src.get_value()->get_idx(); + else return out << "#" << src.get_enode()->get_owner_id(); + } + model_generator::model_generator(ast_manager & m): m_manager(m), m_context(nullptr), @@ -161,20 +170,20 @@ namespace smt { source2color & colors, obj_hashtable & already_traversed, svector & todo) { + if (src.is_fresh_value()) { - // there is an implicit dependency between a fresh value stub of sort S and the root enodes of sort S that are not associated with fresh values. + // there is an implicit dependency between a fresh value stub of + // sort S and the root enodes of sort S that are not associated with fresh values. + // sort * s = src.get_value()->get_sort(); if (already_traversed.contains(s)) return true; bool visited = true; - unsigned sz = roots.size(); - for (unsigned i = 0; i < sz; i++) { - enode * r = roots[i]; + for (enode * r : roots) { if (m_manager.get_sort(r->get_owner()) != s) continue; SASSERT(r == r->get_root()); - model_value_proc * proc = nullptr; - root2proc.find(r, proc); + model_value_proc * proc = root2proc[r]; SASSERT(proc); if (proc->is_fresh()) continue; // r is associated with a fresh value... @@ -192,17 +201,12 @@ namespace smt { enode * n = src.get_enode(); SASSERT(n == n->get_root()); bool visited = true; - model_value_proc * proc = nullptr; - root2proc.find(n, proc); - SASSERT(proc); + model_value_proc * proc = root2proc[n]; buffer dependencies; proc->get_dependencies(dependencies); for (model_value_dependency const& dep : dependencies) { visit_child(dep, colors, todo, visited); - TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> "; - if (dep.is_fresh_value()) tout << "fresh!" << dep.get_value()->get_idx(); - else tout << "#" << dep.get_enode()->get_owner_id(); - tout << "\n";); + TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << " -> " << dep << " already visited: " << visited << "\n";); } return visited; } @@ -215,9 +219,7 @@ namespace smt { svector & todo, svector & sorted_sources) { TRACE("mg_top_sort", tout << "process source, is_fresh: " << src.is_fresh_value() << " "; - if (src.is_fresh_value()) tout << "fresh!" << src.get_value()->get_idx(); - else tout << "#" << src.get_enode()->get_owner_id(); - tout << ", todo.size(): " << todo.size() << "\n";); + tout << src << ", todo.size(): " << todo.size() << "\n";); int color = get_color(colors, src); SASSERT(color != Grey); if (color == Black) @@ -227,17 +229,16 @@ namespace smt { while (!todo.empty()) { source curr = todo.back(); TRACE("mg_top_sort", tout << "current source, is_fresh: " << curr.is_fresh_value() << " "; - if (curr.is_fresh_value()) tout << "fresh!" << curr.get_value()->get_idx(); - else tout << "#" << curr.get_enode()->get_owner_id(); - tout << ", todo.size(): " << todo.size() << "\n";); + tout << curr << ", todo.size(): " << todo.size() << "\n";); switch (get_color(colors, curr)) { case White: set_color(colors, curr, Grey); visit_children(curr, roots, root2proc, colors, already_traversed, todo); break; case Grey: - SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo)); + // SASSERT(visit_children(curr, roots, root2proc, colors, already_traversed, todo)); set_color(colors, curr, Black); + TRACE("mg_top_sort", tout << "append " << curr << "\n";); sorted_sources.push_back(curr); break; case Black: @@ -266,18 +267,15 @@ namespace smt { // topological sort // traverse all extra fresh values... - unsigned sz = m_extra_fresh_values.size(); - for (unsigned i = 0; i < sz; i++) { - extra_fresh_value * f = m_extra_fresh_values[i]; + for (extra_fresh_value * f : m_extra_fresh_values) { process_source(source(f), roots, root2proc, colors, already_traversed, todo, sorted_sources); } // traverse all enodes that are associated with fresh values... - sz = roots.size(); + unsigned sz = roots.size(); for (unsigned i = 0; i < sz; i++) { enode * r = roots[i]; - model_value_proc * proc = nullptr; - root2proc.find(r, proc); + model_value_proc * proc = root2proc[r]; SASSERT(proc); if (!proc->is_fresh()) continue; @@ -303,43 +301,38 @@ namespace smt { TRACE("sorted_sources", for (source const& curr : sources) { if (curr.is_fresh_value()) { - tout << "fresh!" << curr.get_value()->get_idx() << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n"; + tout << curr << " " << mk_pp(curr.get_value()->get_sort(), m_manager) << "\n"; } else { enode * n = curr.get_enode(); SASSERT(n->get_root() == n); sort * s = m_manager.get_sort(n->get_owner()); - tout << "#" << n->get_owner_id() << " " << mk_pp(s, m_manager); - model_value_proc * proc = 0; - root2proc.find(n, proc); - SASSERT(proc); - tout << " is_fresh: " << proc->is_fresh() << "\n"; + tout << curr << " " << mk_pp(s, m_manager); + tout << " is_fresh: " << root2proc[n]->is_fresh() << "\n"; } }); for (source const& curr : sources) { if (curr.is_fresh_value()) { sort * s = curr.get_value()->get_sort(); - TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " : " << mk_pp(s, m_manager) << "\n";); + TRACE("model_fresh_bug", tout << curr << " : " << mk_pp(s, m_manager) << "\n";); expr * val = m_model->get_fresh_value(s); - TRACE("model_fresh_bug", tout << "mk fresh!" << curr.get_value()->get_idx() << " := #" << (val == 0 ? UINT_MAX : val->get_id()) << "\n";); + TRACE("model_fresh_bug", tout << curr << " := #" << (val == nullptr ? UINT_MAX : val->get_id()) << "\n";); m_asts.push_back(val); curr.get_value()->set_value(val); } else { enode * n = curr.get_enode(); SASSERT(n->get_root() == n); - TRACE("mg_top_sort", tout << "#" << n->get_owner_id() << "\n";); + TRACE("mg_top_sort", tout << curr << "\n";); dependencies.reset(); dependency_values.reset(); - model_value_proc * proc = nullptr; - VERIFY(root2proc.find(n, proc)); + model_value_proc * proc = root2proc[n]; SASSERT(proc); proc->get_dependencies(dependencies); for (model_value_dependency const& d : dependencies) { if (d.is_fresh_value()) { CTRACE("mg_top_sort", !d.get_value()->get_value(), - tout << "#" << n->get_owner_id() << " -> "; - tout << "fresh!" << d.get_value()->get_idx() << "\n";); + tout << "#" << n->get_owner_id() << " -> " << d << "\n";); SASSERT(d.get_value()->get_value()); dependency_values.push_back(d.get_value()->get_value()); } diff --git a/src/smt/smt_model_generator.h b/src/smt/smt_model_generator.h index 7466b8877..1f69eb324 100644 --- a/src/smt/smt_model_generator.h +++ b/src/smt/smt_model_generator.h @@ -100,14 +100,16 @@ namespace smt { extra_fresh_value * m_value; //!< When m_fresh == true, contains the sort of the fresh value }; public: - model_value_dependency():m_fresh(true), m_value(nullptr) {} - model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {} - model_value_dependency(extra_fresh_value * v):m_fresh(true), m_value(v) {} + model_value_dependency():m_fresh(true), m_value(nullptr) { } + explicit model_value_dependency(enode * n):m_fresh(false), m_enode(n->get_root()) {} + explicit model_value_dependency(extra_fresh_value * v) :m_fresh(true), m_value(v) { SASSERT(v); } bool is_fresh_value() const { return m_fresh; } enode * get_enode() const { SASSERT(!is_fresh_value()); return m_enode; } extra_fresh_value * get_value() const { SASSERT(is_fresh_value()); return m_value; } }; + std::ostream& operator<<(std::ostream& out, model_value_dependency const& d); + typedef model_value_dependency source; struct source_hash_proc { @@ -166,7 +168,7 @@ namespace smt { extra_fresh_value * m_value; public: fresh_value_proc(extra_fresh_value * v):m_value(v) {} - void get_dependencies(buffer & result) override { result.push_back(m_value); } + void get_dependencies(buffer & result) override; app * mk_value(model_generator & m, ptr_vector & values) override { return to_app(values[0]); } bool is_fresh() const override { return true; } }; diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 049555297..c3befced6 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -636,6 +636,7 @@ namespace smt { void add_dependency(enode * n) { m_dependencies.push_back(model_value_dependency(n)); } ~datatype_value_proc() override {} void get_dependencies(buffer & result) override { + for (model_value_dependency& d : m_dependencies) { } result.append(m_dependencies.size(), m_dependencies.c_ptr()); } app * mk_value(model_generator & mg, ptr_vector & values) override {