1 /********************* */
2 /*! \file term_registration_visitor.h
4 ** Original author: dejan
6 ** Minor contributors (to current version):
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
15 #include "theory/term_registration_visitor.h"
16 #include "theory/theory_engine.h"
20 using namespace theory
;
22 std::string
PreRegisterVisitor::toString() const {
24 TNodeToTheorySetMap::const_iterator it
= d_visited
.begin();
25 for (; it
!= d_visited
.end(); ++ it
) {
26 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
31 bool PreRegisterVisitor::alreadyVisited(TNode current
, TNode parent
) {
33 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
35 TheoryId currentTheoryId
= Theory::theoryOf(current
);
36 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
38 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
39 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
41 // Should we use the theory of the type
42 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
44 // Get the theories that have already visited this node
45 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
46 if (find
== d_visited
.end()) {
48 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
49 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
54 Theory::Set visitedTheories
= (*find
).second
;
55 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
56 // The current theory has already visited it, so now it depends on the parent and the type
57 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
59 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
60 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
61 return Theory::setContains(typeTheoryId
, visitedTheories
);
73 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
75 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
76 if (Debug
.isOn("register::internal")) {
77 Debug("register::internal") << toString() << std::endl
;
80 // Get the theories of the terms
81 TheoryId currentTheoryId
= Theory::theoryOf(current
);
82 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
84 // Should we use the theory of the type
85 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
87 Theory::Set visitedTheories
= d_visited
[current
];
88 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
89 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
90 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
91 d_visited
[current
] = visitedTheories
;
92 d_engine
->theoryOf(currentTheoryId
)->preRegisterTerm(current
);
93 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
95 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
96 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
97 d_visited
[current
] = visitedTheories
;
98 d_engine
->theoryOf(parentTheoryId
)->preRegisterTerm(current
);
99 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
102 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
103 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
104 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
105 d_visited
[current
] = visitedTheories
;
106 d_engine
->theoryOf(typeTheoryId
)->preRegisterTerm(current
);
107 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
110 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
112 Assert(d_visited
.find(current
) != d_visited
.end());
113 Assert(alreadyVisited(current
, parent
));
116 void PreRegisterVisitor::start(TNode node
) {
117 d_multipleTheories
= false;
120 bool PreRegisterVisitor::done(TNode node
) {
121 // We have multiple theories if removing the node theory from others is non-empty
122 return Theory::setRemove(Theory::theoryOf(node
), d_theories
);
125 std::string
SharedTermsVisitor::toString() const {
126 std::stringstream ss
;
127 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
128 for (; it
!= d_visited
.end(); ++ it
) {
129 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
134 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
136 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
138 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
140 // If node is not visited at all, just return false
141 if (find
== d_visited
.end()) {
142 Debug("register::internal") << "1:false" << std::endl
;
146 Theory::Set theories
= (*find
).second
;
148 TheoryId currentTheoryId
= Theory::theoryOf(current
);
149 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
151 // Should we use the theory of the type
152 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
154 if (Theory::setContains(currentTheoryId
, theories
)) {
155 if (Theory::setContains(parentTheoryId
, theories
)) {
157 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
158 return Theory::setContains(typeTheoryId
, theories
);
170 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
172 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
173 if (Debug
.isOn("register::internal")) {
174 Debug("register::internal") << toString() << std::endl
;
177 // Get the theories of the terms
178 TheoryId currentTheoryId
= Theory::theoryOf(current
);
179 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
181 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
183 Theory::Set visitedTheories
= d_visited
[current
];
184 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
185 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
186 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
187 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
189 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
190 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
191 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
194 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
195 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
196 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
197 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
200 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
202 // Record the new theories that we visited
203 d_visited
[current
] = visitedTheories
;
205 // If there is more than two theories and a new one has been added notify the shared terms database
206 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
207 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
210 Assert(d_visited
.find(current
) != d_visited
.end());
211 Assert(alreadyVisited(current
, parent
));
214 void SharedTermsVisitor::start(TNode node
) {
219 void SharedTermsVisitor::done(TNode node
) {
223 void SharedTermsVisitor::clear() {