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
<< ") => ";
35 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
37 // If node is not visited at all, just return false
38 if (find
== d_visited
.end()) {
39 Debug("register::internal") << "1:false" << std::endl
;
45 TheoryId currentTheoryId
= Theory::theoryOf(current
);
46 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
48 // Remember the theories interested in this term
49 d_theories
[parent
] = theories
= Theory::setInsert(currentTheoryId
, d_theories
[parent
]);
50 // Check if there are multiple of those
51 d_multipleTheories
= d_multipleTheories
|| Theory::setRemove(parentTheoryId
, theories
);
53 theories
= (*find
).second
;
54 if (Theory::setContains(currentTheoryId
, theories
)) {
55 // The current theory has already visited it, so now it depends on the parent
56 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
57 return Theory::setContains(parentTheoryId
, theories
);
59 // If the current theory is not registered, it still needs to be visited
60 Debug("register::internal") << "3:false" << std::endl
;
65 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
69 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
70 if (Debug
.isOn("register::internal")) {
71 Debug("register::internal") << toString() << std::endl
;
74 // Get the theories of the terms
75 TheoryId currentTheoryId
= Theory::theoryOf(current
);
76 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
78 // Remember the theories interested in this term
79 d_theories
[parent
] = theories
= Theory::setInsert(currentTheoryId
, d_theories
[parent
]);
80 // If there are theories other than the parent itself, we are in multi-theory case
81 d_multipleTheories
= d_multipleTheories
|| Theory::setRemove(parentTheoryId
, theories
);
83 theories
= d_visited
[current
];
84 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
85 if (!Theory::setContains(currentTheoryId
, theories
)) {
86 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
87 d_engine
->theoryOf(currentTheoryId
)->preRegisterTerm(current
);
88 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
90 if (!Theory::setContains(parentTheoryId
, theories
)) {
91 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
92 d_engine
->theoryOf(parentTheoryId
)->preRegisterTerm(current
);
93 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
95 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
97 Assert(d_visited
.find(current
) != d_visited
.end());
98 Assert(alreadyVisited(current
, parent
));
101 void PreRegisterVisitor::start(TNode node
) {
102 d_multipleTheories
= false;
105 bool PreRegisterVisitor::done(TNode node
) {
106 return d_multipleTheories
;
109 std::string
SharedTermsVisitor::toString() const {
110 std::stringstream ss
;
111 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
112 for (; it
!= d_visited
.end(); ++ it
) {
113 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
118 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
120 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ") => ";
122 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
124 // If node is not visited at all, just return false
125 if (find
== d_visited
.end()) {
126 Debug("register::internal") << "1:false" << std::endl
;
130 Theory::Set theories
= (*find
).second
;
132 TheoryId currentTheoryId
= Theory::theoryOf(current
);
133 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
135 if (Theory::setContains(currentTheoryId
, theories
)) {
136 // The current theory has already visited it, so now it depends on the parent
137 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
138 return Theory::setContains(parentTheoryId
, theories
);
140 // If the current theory is not registered, it still needs to be visited
141 Debug("register::internal") << "2:false" << std::endl
;
146 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
148 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
149 Debug("register::internal") << toString() << std::endl
;
151 // Get the theories of the terms
152 TheoryId currentTheoryId
= Theory::theoryOf(current
);
153 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
155 Theory::Set theories
= d_visited
[current
];
156 unsigned theoriesCount
= theories
== 0 ? 0 : 1;
157 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
158 if (!Theory::setContains(currentTheoryId
, theories
)) {
159 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
161 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
163 if (!Theory::setContains(parentTheoryId
, theories
)) {
164 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
166 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
168 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
170 // If there is more than two theories and a new one has been added notify the shared terms database
171 if (theoriesCount
> 1) {
172 d_sharedTerms
.addSharedTerm(d_atom
, current
, theories
);
175 Assert(d_visited
.find(current
) != d_visited
.end());
176 Assert(alreadyVisited(current
, parent
));
179 void SharedTermsVisitor::start(TNode node
) {
184 void SharedTermsVisitor::done(TNode node
) {
188 void SharedTermsVisitor::clear() {