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 TNodeVisitedMap::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
) const {
33 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current
<< "," << parent
<< ") => ";
35 TNodeVisitedMap::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
;
43 Theory::Set theories
= (*find
).second
;
45 TheoryId currentTheoryId
= Theory::theoryOf(current
);
46 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
48 if (Theory::setContains(currentTheoryId
, theories
)) {
49 // The current theory has already visited it, so now it depends on the parent
50 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
51 return Theory::setContains(parentTheoryId
, theories
);
53 // If the current theory is not registered, it still needs to be visited
54 Debug("register::internal") << "2:false" << std::endl
;
59 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
61 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
62 Debug("register::internal") << toString() << std::endl
;
64 // Get the theories of the terms
65 TheoryId currentTheoryId
= Theory::theoryOf(current
);
66 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
68 Theory::Set theories
= d_visited
[current
];
69 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
70 if (!Theory::setContains(currentTheoryId
, theories
)) {
71 d_multipleTheories
= d_multipleTheories
|| (theories
!= 0);
72 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
73 d_engine
->theoryOf(currentTheoryId
)->preRegisterTerm(current
);
74 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
75 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
77 if (!Theory::setContains(parentTheoryId
, theories
)) {
78 d_multipleTheories
= d_multipleTheories
|| (theories
!= 0);
79 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
80 d_engine
->theoryOf(parentTheoryId
)->preRegisterTerm(current
);
81 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
82 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
84 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
86 Assert(d_visited
.find(current
) != d_visited
.end());
87 Assert(alreadyVisited(current
, parent
));
90 void PreRegisterVisitor::start(TNode node
) {
92 d_multipleTheories
= false;
95 bool PreRegisterVisitor::done(TNode node
) {
96 return d_multipleTheories
;
99 std::string
SharedTermsVisitor::toString() const {
100 std::stringstream ss
;
101 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
102 for (; it
!= d_visited
.end(); ++ it
) {
103 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
108 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
110 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ") => ";
112 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
114 // If node is not visited at all, just return false
115 if (find
== d_visited
.end()) {
116 Debug("register::internal") << "1:false" << std::endl
;
120 Theory::Set theories
= (*find
).second
;
122 TheoryId currentTheoryId
= Theory::theoryOf(current
);
123 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
125 if (Theory::setContains(currentTheoryId
, theories
)) {
126 // The current theory has already visited it, so now it depends on the parent
127 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
128 return Theory::setContains(parentTheoryId
, theories
);
130 // If the current theory is not registered, it still needs to be visited
131 Debug("register::internal") << "2:false" << std::endl
;
136 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
138 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
139 Debug("register::internal") << toString() << std::endl
;
141 // Get the theories of the terms
142 TheoryId currentTheoryId
= Theory::theoryOf(current
);
143 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
145 Theory::Set theories
= d_visited
[current
];
146 unsigned theoriesCount
= theories
== 0 ? 0 : 1;
147 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
148 if (!Theory::setContains(currentTheoryId
, theories
)) {
149 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
151 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
153 if (!Theory::setContains(parentTheoryId
, theories
)) {
154 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
156 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
158 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
160 // If there is more than two theories and a new one has been added notify the shared terms database
161 if (theoriesCount
> 1) {
162 d_sharedTerms
.addSharedTerm(d_atom
, current
, theories
);
165 Assert(d_visited
.find(current
) != d_visited
.end());
166 Assert(alreadyVisited(current
, parent
));
169 void SharedTermsVisitor::start(TNode node
) {
174 void SharedTermsVisitor::done(TNode node
) {
178 void SharedTermsVisitor::clear() {