1 /*++
2 Copyright (c) 2011 Microsoft Corporation
3
4 Module Name:
5
6 shared_occs.cpp
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 #include "ast/shared_occs.h"
20 #include "ast/ast_smt2_pp.h"
21 #include "util/ref_util.h"
22
insert(expr * t)23 inline void shared_occs::insert(expr * t) {
24 m_shared.reserve(t->get_id() + 1);
25 m_shared[t->get_id()] = t;
26 }
27
reset()28 void shared_occs::reset() {
29 m_shared.reset();
30 }
31
cleanup()32 void shared_occs::cleanup() {
33 reset();
34 m_shared.finalize();
35 m_stack.finalize();
36 }
37
~shared_occs()38 shared_occs::~shared_occs() {
39 reset();
40 }
41
process(expr * t,shared_occs_mark & visited)42 inline bool shared_occs::process(expr * t, shared_occs_mark & visited) {
43 switch (t->get_kind()) {
44 case AST_APP: {
45 unsigned num_args = to_app(t)->get_num_args();
46 if (t->get_ref_count() > 1 && (m_track_atomic || num_args > 0)) {
47 if (visited.is_marked(t)) {
48 insert(t);
49 return true;
50 }
51 visited.mark(t);
52 }
53 if (num_args == 0)
54 return true; // done with t
55 m_stack.push_back(frame(t, 0)); // need to create frame if num_args > 0
56 return false;
57 }
58 case AST_VAR:
59 if (m_track_atomic && t->get_ref_count() > 1) {
60 if (visited.is_marked(t))
61 insert(t);
62 else
63 visited.mark(t);
64 }
65 return true; // done with t
66 case AST_QUANTIFIER:
67 if (t->get_ref_count() > 1) {
68 if (visited.is_marked(t)) {
69 insert(t);
70 return true; // done with t
71 }
72 visited.mark(t);
73 }
74 if (!m_visit_quantifiers)
75 return true;
76 m_stack.push_back(frame(t, 0));
77 return false;
78 default:
79 UNREACHABLE();
80 return true;
81 }
82 }
83
operator ()(expr * t,shared_occs_mark & visited)84 void shared_occs::operator()(expr * t, shared_occs_mark & visited) {
85 SASSERT(m_stack.empty());
86 if (process(t, visited)) {
87 return;
88 }
89 SASSERT(!m_stack.empty());
90 while (!m_stack.empty()) {
91 start:
92 frame & fr = m_stack.back();
93 expr * curr = fr.first;
94 switch (curr->get_kind()) {
95 case AST_APP: {
96
97 unsigned num_args = to_app(curr)->get_num_args();
98
99 while (fr.second < num_args) {
100 expr * arg = to_app(curr)->get_arg(fr.second);
101 fr.second++;
102 if (!process(arg, visited))
103 goto start;
104 }
105 break;
106 }
107 case AST_QUANTIFIER: {
108 SASSERT(m_visit_quantifiers);
109 unsigned num_children = m_visit_patterns ? to_quantifier(curr)->get_num_children() : 1;
110 while (fr.second < num_children) {
111 expr * child = to_quantifier(curr)->get_child(fr.second);
112 fr.second++;
113 if (!process(child, visited))
114 goto start;
115 }
116 break;
117 }
118 default:
119 UNREACHABLE();
120 break;
121 }
122 m_stack.pop_back();
123 }
124 }
125
126
operator ()(expr * t)127 void shared_occs::operator()(expr * t) {
128 SASSERT(m_stack.empty());
129 shared_occs_mark visited;
130 reset();
131 operator()(t, visited);
132 }
133
display(std::ostream & out,ast_manager & m) const134 void shared_occs::display(std::ostream & out, ast_manager & m) const {
135 for (expr* s : m_shared) {
136 if (s) {
137 out << mk_ismt2_pp(s, m) << "\n";
138 }
139 }
140 }
141
num_shared() const142 unsigned shared_occs::num_shared() const{
143 unsigned count = 0;
144 for (expr* s : m_shared) if (s) count++;
145 return count;
146 }
147