From 0bbdee810d96357bd6e87f5b2477ec4c17764156 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 14 Feb 2018 21:46:20 -0800 Subject: [PATCH] fix #1488 Signed-off-by: Nikolaj Bjorner --- src/ast/ast_pp_util.cpp | 1 + src/ast/decl_collector.cpp | 78 +++++++++++++++++++++------- src/ast/decl_collector.h | 10 ++++ src/util/top_sort.h | 101 +++++++++++++++++++++++++++++++++++++ 4 files changed, 172 insertions(+), 18 deletions(-) create mode 100644 src/util/top_sort.h diff --git a/src/ast/ast_pp_util.cpp b/src/ast/ast_pp_util.cpp index 4579f2ffc..37785e072 100644 --- a/src/ast/ast_pp_util.cpp +++ b/src/ast/ast_pp_util.cpp @@ -38,6 +38,7 @@ void ast_pp_util::collect(expr_ref_vector const& es) { void ast_pp_util::display_decls(std::ostream& out) { smt2_pp_environment_dbg env(m); ast_smt_pp pp(m); + coll.order_deps(); unsigned n = coll.get_num_sorts(); for (unsigned i = 0; i < n; ++i) { pp.display_ast_smt2(out, coll.get_sorts()[i], 0, 0, nullptr); diff --git a/src/ast/decl_collector.cpp b/src/ast/decl_collector.cpp index e000f43df..1baac4515 100644 --- a/src/ast/decl_collector.cpp +++ b/src/ast/decl_collector.cpp @@ -18,6 +18,7 @@ Revision History: --*/ #include "ast/decl_collector.h" +#include "ast/ast_pp.h" void decl_collector::visit_sort(sort * n) { family_id fid = n->get_family_id(); @@ -25,19 +26,21 @@ void decl_collector::visit_sort(sort * n) { m_sorts.push_back(n); if (fid == m_dt_fid) { m_sorts.push_back(n); - unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(n); for (unsigned i = 0; i < num_cnstr; i++) { func_decl * cnstr = m_dt_util.get_datatype_constructors(n)->get(i); - m_decls.push_back(cnstr); + m_todo.push_back(cnstr); ptr_vector const & cnstr_acc = *m_dt_util.get_constructor_accessors(cnstr); unsigned num_cas = cnstr_acc.size(); for (unsigned j = 0; j < num_cas; j++) { - func_decl * accsr = cnstr_acc.get(j); - m_decls.push_back(accsr); + m_todo.push_back(cnstr_acc.get(j)); } } } + for (unsigned i = n->get_num_parameters(); i-- > 0; ) { + parameter const& p = n->get_parameter(i); + if (p.is_ast()) m_todo.push_back(p.get_ast()); + } } bool decl_collector::is_bool(sort * s) { @@ -63,43 +66,43 @@ decl_collector::decl_collector(ast_manager & m, bool preds): } void decl_collector::visit(ast* n) { - ptr_vector todo; - todo.push_back(n); - while (!todo.empty()) { - n = todo.back(); - todo.pop_back(); + datatype_util util(m()); + m_todo.push_back(n); + while (!m_todo.empty()) { + n = m_todo.back(); + m_todo.pop_back(); if (!m_visited.is_marked(n)) { m_visited.mark(n, true); switch(n->get_kind()) { case AST_APP: { app * a = to_app(n); - for (unsigned i = 0; i < a->get_num_args(); ++i) { - todo.push_back(a->get_arg(i)); + for (expr* arg : *a) { + m_todo.push_back(arg); } - todo.push_back(a->get_decl()); + m_todo.push_back(a->get_decl()); break; } case AST_QUANTIFIER: { quantifier * q = to_quantifier(n); unsigned num_decls = q->get_num_decls(); for (unsigned i = 0; i < num_decls; ++i) { - todo.push_back(q->get_decl_sort(i)); + m_todo.push_back(q->get_decl_sort(i)); } - todo.push_back(q->get_expr()); + m_todo.push_back(q->get_expr()); for (unsigned i = 0; i < q->get_num_patterns(); ++i) { - todo.push_back(q->get_pattern(i)); + m_todo.push_back(q->get_pattern(i)); } break; } - case AST_SORT: + case AST_SORT: visit_sort(to_sort(n)); break; case AST_FUNC_DECL: { func_decl * d = to_func_decl(n); for (unsigned i = 0; i < d->get_arity(); ++i) { - todo.push_back(d->get_domain(i)); + m_todo.push_back(d->get_domain(i)); } - todo.push_back(d->get_range()); + m_todo.push_back(d->get_range()); visit_func(d); break; } @@ -112,5 +115,44 @@ void decl_collector::visit(ast* n) { } } +void decl_collector::order_deps() { + top_sort st; + for (sort * s : m_sorts) st.insert(s, collect_deps(s)); + st.topological_sort(); + m_sorts.reset(); + for (sort* s : st.top_sorted()) m_sorts.push_back(s); +} + +decl_collector::sort_set* decl_collector::collect_deps(sort* s) { + sort_set* set = alloc(sort_set); + collect_deps(s, *set); + set->remove(s); + return set; +} + +void decl_collector::collect_deps(sort* s, sort_set& set) { + if (set.contains(s)) return; + set.insert(s); + if (s->is_sort_of(m_dt_util.get_family_id(), DATATYPE_SORT)) { + unsigned num_sorts = m_dt_util.get_datatype_num_parameter_sorts(s); + for (unsigned i = 0; i < num_sorts; ++i) { + set.insert(m_dt_util.get_datatype_parameter_sort(s, i)); + } + unsigned num_cnstr = m_dt_util.get_datatype_num_constructors(s); + for (unsigned i = 0; i < num_cnstr; i++) { + func_decl * cnstr = m_dt_util.get_datatype_constructors(s)->get(i); + set.insert(cnstr->get_range()); + for (unsigned j = 0; j < cnstr->get_arity(); ++j) + set.insert(cnstr->get_domain(j)); + } + } + + for (unsigned i = s->get_num_parameters(); i-- > 0; ) { + parameter const& p = s->get_parameter(i); + if (p.is_ast() && is_sort(p.get_ast())) { + set.insert(to_sort(p.get_ast())); + } + } +} diff --git a/src/ast/decl_collector.h b/src/ast/decl_collector.h index 053d6df41..041438864 100644 --- a/src/ast/decl_collector.h +++ b/src/ast/decl_collector.h @@ -20,6 +20,7 @@ Revision History: #ifndef SMT_DECL_COLLECTOR_H_ #define SMT_DECL_COLLECTOR_H_ +#include "util/top_sort.h" #include "ast/ast.h" #include "ast/datatype_decl_plugin.h" @@ -33,11 +34,17 @@ class decl_collector { family_id m_basic_fid; family_id m_dt_fid; datatype_util m_dt_util; + ptr_vector m_todo; void visit_sort(sort* n); bool is_bool(sort* s); void visit_func(func_decl* n); + typedef obj_hashtable sort_set; + sort_set* collect_deps(sort* s); + void collect_deps(top_sort& st); + void collect_deps(sort* s, sort_set& set); + public: // if preds == true, then predicates are stored in a separate collection. @@ -48,9 +55,12 @@ public: void visit(unsigned n, expr* const* es); void visit(expr_ref_vector const& es); + void order_deps(); + unsigned get_num_sorts() const { return m_sorts.size(); } unsigned get_num_decls() const { return m_decls.size(); } unsigned get_num_preds() const { return m_preds.size(); } + sort * const * get_sorts() const { return m_sorts.c_ptr(); } func_decl * const * get_func_decls() const { return m_decls.c_ptr(); } func_decl * const * get_pred_decls() const { return m_preds.c_ptr(); } diff --git a/src/util/top_sort.h b/src/util/top_sort.h new file mode 100644 index 000000000..d017d162b --- /dev/null +++ b/src/util/top_sort.h @@ -0,0 +1,101 @@ +/*++ +Copyright (c) 2018 Microsoft Corporation + +Module Name: + + top_sort.h + +Abstract: + Topological sort over objects + +Author: + + Nikolaj Bjorner (nbjorner) 2018-02-14 + +Revision History: + +--*/ + +#ifndef TOP_SORT_H_ +#define TOP_SORT_H_ + +#include "util/obj_hashtable.h" +#include "util/vector.h" +#include +#include +#include +#include "util/memory_manager.h" + + +template +class top_sort { + typedef obj_hashtable T_set; + obj_map m_partition_id; + obj_map m_dfs_num; + ptr_vector m_top_sorted; + ptr_vector m_stack_S; + ptr_vector m_stack_P; + unsigned m_next_preorder; + obj_map m_deps; + + void traverse(T* f) { + unsigned p_id = 0; + if (m_dfs_num.find(f, p_id)) { + if (!m_partition_id.contains(f)) { + while (!m_stack_P.empty() && m_partition_id[m_stack_P.back()] > p_id) { + m_stack_P.pop_back(); + } + } + } + else if (!m_deps.contains(f)) { + return; + } + else { + m_dfs_num.insert(f, m_next_preorder++); + m_stack_S.push_back(f); + m_stack_P.push_back(f); + for (T* g : *m_deps[f]) { + traverse(g); + } + if (f == m_stack_P.back()) { + + p_id = m_top_sorted.size(); + T* s_f; + do { + s_f = m_stack_S.back(); + m_stack_S.pop_back(); + m_top_sorted.push_back(s_f); + m_partition_id.insert(s_f, p_id); + } + while (s_f != f); + m_stack_P.pop_back(); + } + } + } + +public: + + ~top_sort() { + for (auto & kv : m_deps) dealloc(kv.m_value); + } + + void topological_sort() { + m_next_preorder = 0; + m_partition_id.reset(); + m_top_sorted.reset(); + for (auto & kv : m_deps) { + traverse(kv.m_key); + } + SASSERT(m_stack_S.empty()); + SASSERT(m_stack_P.empty()); + m_dfs_num.reset(); + } + + void insert(T* t, T_set* s) { + m_deps.insert(t, s); + } + + ptr_vector const& top_sorted() { return m_top_sorted; } +}; + +#endif /* TOP_SORT_H_ */