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