1 /*++ 2 Copyright (c) 2006 Microsoft Corporation 3 4 Module Name: 5 6 func_decl_dependencies.h 7 8 Abstract: 9 10 <abstract> 11 12 Author: 13 14 Leonardo de Moura (leonardo) 2010-12-15. 15 16 Revision History: 17 18 --*/ 19 #pragma once 20 21 #include "ast/ast.h" 22 #include "util/obj_hashtable.h" 23 24 // Set of dependencies 25 typedef obj_hashtable<func_decl> func_decl_set; 26 27 /** 28 \brief Collect uninterpreted function declarations (with arity > 0) occurring in \c n. 29 */ 30 void collect_func_decls(ast_manager & m, expr * n, func_decl_set & r, bool ng_only = false); 31 32 /** 33 \brief Auxiliary data-structure used for tracking dependencies between function declarations. 34 35 The following pattern of use is expected: 36 37 func_decl_dependencies & dm; 38 func_decl_set * S = dm.mk_func_decl_set(); 39 dm.collect_func_decls(t_1, S); 40 ... 41 dm.collect_func_decls(t_n, S); 42 dm.insert(f, S); 43 */ 44 class func_decl_dependencies { 45 typedef obj_map<func_decl, func_decl_set *> dependency_graph; 46 ast_manager & m_manager; 47 dependency_graph m_deps; 48 49 class top_sort; 50 51 public: func_decl_dependencies(ast_manager & m)52 func_decl_dependencies(ast_manager & m):m_manager(m) {} ~func_decl_dependencies()53 ~func_decl_dependencies() { 54 reset(); 55 } 56 57 void reset(); 58 59 /** 60 \brief Create a dependency set. 61 This set should be populated using #collect_func_decls. 62 After populating the set, it must be used as an argument for the #insert method. 63 64 \remark The manager owns the set. 65 66 \warning Failure to call #insert will produce a memory leak. 67 */ mk_func_decl_set()68 func_decl_set * mk_func_decl_set() { return alloc(func_decl_set); } 69 70 /** 71 \brief Store the uninterpreted function declarations used in \c n into \c s. 72 */ 73 void collect_func_decls(expr * n, func_decl_set * s); 74 75 /** 76 \brief Store the uninterpreted function declarations (in non ground terms) used in \c n into \c s. 77 */ 78 void collect_ng_func_decls(expr * n, func_decl_set * s); 79 80 /** 81 \brief Insert \c f in the manager with the given set of dependencies. 82 The insertion succeeds iff 83 1- no cycle is created between the new entry and 84 the already existing dependencies. 85 2- \c f was not already inserted into the manager. 86 87 Return false in case of failure. 88 89 \remark The manager is the owner of the dependency sets. 90 */ 91 bool insert(func_decl * f, func_decl_set * s); 92 93 /** 94 \brief Return true if \c f is registered in this manager. 95 */ contains(func_decl * f)96 bool contains(func_decl * f) const { return m_deps.contains(f); } 97 get_dependencies(func_decl * f)98 func_decl_set * get_dependencies(func_decl * f) const { func_decl_set * r = nullptr; m_deps.find(f, r); return r; } 99 100 /** 101 \brief Erase \c f (and its dependencies) from the manager. 102 */ 103 void erase(func_decl * f); 104 105 void display(std::ostream & out); 106 }; 107 108 109