fix #1488

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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);

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<func_decl> 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_todo.push_back(cnstr_acc.get(j));
-                m_decls.push_back(accsr);
             }
         }
     }
+    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<ast> todo;
+    datatype_util util(m());
-    todo.push_back(n);
+    m_todo.push_back(n);
-    while (!todo.empty()) {
+    while (!m_todo.empty()) {
-        n = todo.back();
+        n = m_todo.back();
-        todo.pop_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) {
+                for (expr* arg : *a) {
-                    todo.push_back(a->get_arg(i));
+                    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<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()));
+        }
+    }
+}
 
 

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<ast>       m_todo;
 
     void visit_sort(sort* n);
     bool is_bool(sort* s);
     void visit_func(func_decl* n);
 
+    typedef obj_hashtable<sort> sort_set;
+    sort_set* collect_deps(sort* s);
+    void collect_deps(top_sort<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(); }

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<algorithm>
+#include<type_traits>
+#include<memory.h>
+#include "util/memory_manager.h"
+
+
+template<typename T>
+class top_sort {
+    typedef obj_hashtable<T> T_set;
+    obj_map<T, unsigned> m_partition_id;
+    obj_map<T, unsigned> m_dfs_num;
+    ptr_vector<T>        m_top_sorted;
+    ptr_vector<T>        m_stack_S;
+    ptr_vector<T>        m_stack_P;
+    unsigned             m_next_preorder;    
+    obj_map<T, T_set*>   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<T> const& top_sorted() { return m_top_sorted; }    
+};
+
+#endif /* TOP_SORT_H_ */