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 Debug("register::internal") << toString() << std::endl
;
72 // Get the theories of the terms
73 TheoryId currentTheoryId
= Theory::theoryOf(current
);
74 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
76 // Remember the theories interested in this term
77 d_theories
[parent
] = theories
= Theory::setInsert(currentTheoryId
, d_theories
[parent
]);
78 // If there are theories other than the parent itself, we are in multi-theory case
79 d_multipleTheories
= d_multipleTheories
|| Theory::setRemove(parentTheoryId
, theories
);
81 theories
= d_visited
[current
];
82 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
83 if (!Theory::setContains(currentTheoryId
, theories
)) {
84 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
85 d_engine
->theoryOf(currentTheoryId
)->preRegisterTerm(current
);
86 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
88 if (!Theory::setContains(parentTheoryId
, theories
)) {
89 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
90 d_engine
->theoryOf(parentTheoryId
)->preRegisterTerm(current
);
91 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
93 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
95 Assert(d_visited
.find(current
) != d_visited
.end());
96 Assert(alreadyVisited(current
, parent
));
99 void PreRegisterVisitor::start(TNode node
) {
100 d_multipleTheories
= false;
103 bool PreRegisterVisitor::done(TNode node
) {
104 return d_multipleTheories
;
107 std::string
SharedTermsVisitor::toString() const {
108 std::stringstream ss
;
109 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
110 for (; it
!= d_visited
.end(); ++ it
) {
111 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
116 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
118 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ") => ";
120 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
122 // If node is not visited at all, just return false
123 if (find
== d_visited
.end()) {
124 Debug("register::internal") << "1:false" << std::endl
;
128 Theory::Set theories
= (*find
).second
;
130 TheoryId currentTheoryId
= Theory::theoryOf(current
);
131 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
133 if (Theory::setContains(currentTheoryId
, theories
)) {
134 // The current theory has already visited it, so now it depends on the parent
135 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
136 return Theory::setContains(parentTheoryId
, theories
);
138 // If the current theory is not registered, it still needs to be visited
139 Debug("register::internal") << "2:false" << std::endl
;
144 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
146 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
147 Debug("register::internal") << toString() << std::endl
;
149 // Get the theories of the terms
150 TheoryId currentTheoryId
= Theory::theoryOf(current
);
151 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
153 Theory::Set theories
= d_visited
[current
];
154 unsigned theoriesCount
= theories
== 0 ? 0 : 1;
155 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
156 if (!Theory::setContains(currentTheoryId
, theories
)) {
157 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
159 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
161 if (!Theory::setContains(parentTheoryId
, theories
)) {
162 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
164 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
166 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
168 // If there is more than two theories and a new one has been added notify the shared terms database
169 if (theoriesCount
> 1) {
170 d_sharedTerms
.addSharedTerm(d_atom
, current
, theories
);
173 Assert(d_visited
.find(current
) != d_visited
.end());
174 Assert(alreadyVisited(current
, parent
));
177 void SharedTermsVisitor::start(TNode node
) {
182 void SharedTermsVisitor::done(TNode node
) {
186 void SharedTermsVisitor::clear() {