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
;
43 TheoryId currentTheoryId
= Theory::theoryOf(current
);
44 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
46 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
47 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
49 Theory::Set visitedTheories
= (*find
).second
;
50 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
51 // The current theory has already visited it, so now it depends on the parent
52 Debug("register::internal") << (Theory::setContains(parentTheoryId
, visitedTheories
) ? "2:true" : "2:false") << std::endl
;
53 return Theory::setContains(parentTheoryId
, visitedTheories
);
55 // If the current theory is not registered, it still needs to be visited
56 Debug("register::internal") << "3:false" << std::endl
;
61 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
63 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
64 if (Debug
.isOn("register::internal")) {
65 Debug("register::internal") << toString() << std::endl
;
68 // Get the theories of the terms
69 TheoryId currentTheoryId
= Theory::theoryOf(current
);
70 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
72 Theory::Set visitedTheories
= d_visited
[current
];
73 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
74 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
75 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
76 d_visited
[current
] = visitedTheories
;
77 d_engine
->theoryOf(currentTheoryId
)->preRegisterTerm(current
);
78 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
80 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
81 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
82 d_visited
[current
] = visitedTheories
;
83 d_engine
->theoryOf(parentTheoryId
)->preRegisterTerm(current
);
84 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
86 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
88 Assert(d_visited
.find(current
) != d_visited
.end());
89 Assert(alreadyVisited(current
, parent
));
92 void PreRegisterVisitor::start(TNode node
) {
93 d_multipleTheories
= false;
96 bool PreRegisterVisitor::done(TNode node
) {
97 // We have multiple theories if removing the node theory from others is non-empty
98 return Theory::setRemove(Theory::theoryOf(node
), d_theories
);
101 std::string
SharedTermsVisitor::toString() const {
102 std::stringstream ss
;
103 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
104 for (; it
!= d_visited
.end(); ++ it
) {
105 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
110 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
112 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ") => ";
114 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
116 // If node is not visited at all, just return false
117 if (find
== d_visited
.end()) {
118 Debug("register::internal") << "1:false" << std::endl
;
122 Theory::Set theories
= (*find
).second
;
124 TheoryId currentTheoryId
= Theory::theoryOf(current
);
125 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
127 if (Theory::setContains(currentTheoryId
, theories
)) {
128 // The current theory has already visited it, so now it depends on the parent
129 Debug("register::internal") << (Theory::setContains(parentTheoryId
, theories
) ? "2:true" : "2:false") << std::endl
;
130 return Theory::setContains(parentTheoryId
, theories
);
132 // If the current theory is not registered, it still needs to be visited
133 Debug("register::internal") << "2:false" << std::endl
;
138 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
140 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
141 Debug("register::internal") << toString() << std::endl
;
143 // Get the theories of the terms
144 TheoryId currentTheoryId
= Theory::theoryOf(current
);
145 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
147 Theory::Set theories
= d_visited
[current
];
148 unsigned theoriesCount
= theories
== 0 ? 0 : 1;
149 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(theories
) << std::endl
;
150 if (!Theory::setContains(currentTheoryId
, theories
)) {
151 d_visited
[current
] = theories
= Theory::setInsert(currentTheoryId
, theories
);
153 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
155 if (!Theory::setContains(parentTheoryId
, theories
)) {
156 d_visited
[current
] = theories
= Theory::setInsert(parentTheoryId
, theories
);
158 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
160 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(theories
) << std::endl
;
162 // If there is more than two theories and a new one has been added notify the shared terms database
163 if (theoriesCount
> 1) {
164 d_sharedTerms
.addSharedTerm(d_atom
, current
, theories
);
167 Assert(d_visited
.find(current
) != d_visited
.end());
168 Assert(alreadyVisited(current
, parent
));
171 void SharedTermsVisitor::start(TNode node
) {
176 void SharedTermsVisitor::done(TNode node
) {
180 void SharedTermsVisitor::clear() {