1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3 
4 Module Name:
5 
6     shared_occs.h
7 
8 Abstract:
9 
10     Functor for computing the shared subterms in a given
11     term.
12 
13 Author:
14 
15     Leonardo de Moura (leonardo) 2011-04-01.
16 
17 Revision History:
18 --*/
19 #pragma once
20 
21 #include "ast/ast.h"
22 #include "util/obj_hashtable.h"
23 
24 class shared_occs_mark {
25     ptr_buffer<ast> m_to_unmark;
26 public:
shared_occs_mark()27     shared_occs_mark() {}
28 
~shared_occs_mark()29     ~shared_occs_mark() {
30         reset();
31     }
32 
is_marked(ast * n)33     bool is_marked(ast * n) { return n->is_marked_so(); }
reset_mark(ast * n)34     void reset_mark(ast * n) { n->reset_mark_so(); }
mark(ast * n)35     void mark(ast * n) { if (is_marked(n)) return; n->mark_so(true); m_to_unmark.push_back(n); }
reset()36     void reset() {
37         ptr_buffer<ast>::iterator it  = m_to_unmark.begin();
38         ptr_buffer<ast>::iterator end = m_to_unmark.end();
39         for (; it != end; ++it) {
40             reset_mark(*it);
41         }
42         m_to_unmark.reset();
43     }
mark(ast * n,bool flag)44     void mark(ast * n, bool flag) { if (flag) mark(n); else reset_mark(n); }
45 };
46 
47 /**
48    \brief Functor for computing the shared subterms in a given term.
49 */
50 class shared_occs {
51     ast_manager &       m;
52     bool                m_track_atomic;
53     bool                m_visit_quantifiers;
54     bool                m_visit_patterns;
55     expr_ref_vector     m_shared;
56     typedef std::pair<expr*, unsigned> frame;
57     svector<frame>      m_stack;
58     bool process(expr * t, shared_occs_mark & visited);
59     void insert(expr * t);
60 public:
61     typedef obj_hashtable<expr>::iterator iterator;
62     shared_occs(ast_manager & _m, bool track_atomic = false, bool visit_quantifiers = true, bool visit_patterns = false):
m(_m)63         m(_m),
64         m_track_atomic(track_atomic),
65         m_visit_quantifiers(visit_quantifiers),
66         m_visit_patterns(visit_patterns),
67         m_shared(m) {
68     }
69     ~shared_occs();
70     void operator()(expr * t);
71     void operator()(expr * t, shared_occs_mark & visited);
is_shared(expr * t)72     bool is_shared(expr * t) const { return m_shared.get(t->get_id(), nullptr) != nullptr; }
73     unsigned num_shared() const;
74     void reset();
75     void cleanup();
76     void display(std::ostream & out, ast_manager & mgr) const;
77 };
78 
79