1 /********************* */
2 /*! \file term_registration_visitor.cpp
4 ** Top contributors (to current version):
5 ** Dejan Jovanovic, Andrew Reynolds, Morgan Deters
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
8 ** in the top-level source directory) and their institutional affiliations.
9 ** All rights reserved. See the file COPYING in the top-level source
10 ** directory for licensing information.\endverbatim
12 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "theory/term_registration_visitor.h"
18 #include "options/quantifiers_options.h"
19 #include "theory/theory_engine.h"
23 using namespace theory
;
25 std::string
PreRegisterVisitor::toString() const {
27 TNodeToTheorySetMap::const_iterator it
= d_visited
.begin();
28 for (; it
!= d_visited
.end(); ++ it
) {
29 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
34 bool PreRegisterVisitor::alreadyVisited(TNode current
, TNode parent
) {
36 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
38 if ((parent
.isClosure() || parent
.getKind() == kind::REWRITE_RULE
39 || parent
.getKind() == kind::SEP_STAR
40 || parent
.getKind() == kind::SEP_WAND
41 || (parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean())
42 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
46 Debug("register::internal") << "quantifier:true" << std::endl
;
50 TheoryId currentTheoryId
= Theory::theoryOf(current
);
51 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
53 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
54 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
56 // Should we use the theory of the type
58 TheoryId typeTheoryId
= THEORY_LAST
;
60 if (current
!= parent
) {
61 if (currentTheoryId
!= parentTheoryId
) {
62 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
63 TypeNode type
= current
.getType();
65 typeTheoryId
= Theory::theoryOf(type
);
67 TypeNode type
= current
.getType();
68 typeTheoryId
= Theory::theoryOf(type
);
69 if (typeTheoryId
!= currentTheoryId
) {
70 if (type
.isInterpretedFinite()) {
77 // Get the theories that have already visited this node
78 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
79 if (find
== d_visited
.end()) {
81 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
86 Theory::Set visitedTheories
= (*find
).second
;
87 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
88 // The current theory has already visited it, so now it depends on the parent and the type
89 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
91 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
92 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
93 return Theory::setContains(typeTheoryId
, visitedTheories
);
105 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
107 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
108 if (Debug
.isOn("register::internal")) {
109 Debug("register::internal") << toString() << std::endl
;
112 // Get the theories of the terms
113 TheoryId currentTheoryId
= Theory::theoryOf(current
);
114 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
116 // Should we use the theory of the type
117 bool useType
= false;
118 TheoryId typeTheoryId
= THEORY_LAST
;
120 if (current
!= parent
) {
121 if (currentTheoryId
!= parentTheoryId
) {
122 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
123 TypeNode type
= current
.getType();
125 typeTheoryId
= Theory::theoryOf(type
);
127 TypeNode type
= current
.getType();
128 typeTheoryId
= Theory::theoryOf(type
);
129 if (typeTheoryId
!= currentTheoryId
) {
130 if (type
.isInterpretedFinite()) {
137 Theory::Set visitedTheories
= d_visited
[current
];
138 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
139 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
140 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
141 d_visited
[current
] = visitedTheories
;
142 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
143 th
->preRegisterTerm(current
);
144 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
146 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
147 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
148 d_visited
[current
] = visitedTheories
;
149 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
150 th
->preRegisterTerm(current
);
151 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
154 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
155 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
156 d_visited
[current
] = visitedTheories
;
157 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
158 th
->preRegisterTerm(current
);
159 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
162 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
164 Assert(d_visited
.find(current
) != d_visited
.end());
165 Assert(alreadyVisited(current
, parent
));
168 std::string
SharedTermsVisitor::toString() const {
169 std::stringstream ss
;
170 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
171 for (; it
!= d_visited
.end(); ++ it
) {
172 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
177 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
179 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
181 if ((parent
.isClosure() || parent
.getKind() == kind::REWRITE_RULE
182 || parent
.getKind() == kind::SEP_STAR
183 || parent
.getKind() == kind::SEP_WAND
184 || (parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean())
185 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
187 && current
!= parent
)
189 Debug("register::internal") << "quantifier:true" << std::endl
;
192 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
194 // If node is not visited at all, just return false
195 if (find
== d_visited
.end()) {
196 Debug("register::internal") << "1:false" << std::endl
;
200 Theory::Set theories
= (*find
).second
;
202 TheoryId currentTheoryId
= Theory::theoryOf(current
);
203 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
205 // Should we use the theory of the type
206 bool useType
= false;
207 TheoryId typeTheoryId
= THEORY_LAST
;
209 if (current
!= parent
) {
210 if (currentTheoryId
!= parentTheoryId
) {
211 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
212 TypeNode type
= current
.getType();
214 typeTheoryId
= Theory::theoryOf(type
);
216 TypeNode type
= current
.getType();
217 typeTheoryId
= Theory::theoryOf(type
);
218 if (typeTheoryId
!= currentTheoryId
) {
219 if (type
.isInterpretedFinite()) {
225 if (current
!= parent
) {
226 if (currentTheoryId
!= parentTheoryId
) {
227 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
228 TypeNode type
= current
.getType();
230 typeTheoryId
= Theory::theoryOf(type
);
232 TypeNode type
= current
.getType();
233 typeTheoryId
= Theory::theoryOf(type
);
234 if (typeTheoryId
!= currentTheoryId
) {
235 if (type
.isInterpretedFinite()) {
242 if (Theory::setContains(currentTheoryId
, theories
)) {
243 if (Theory::setContains(parentTheoryId
, theories
)) {
245 return Theory::setContains(typeTheoryId
, theories
);
257 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
259 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
260 if (Debug
.isOn("register::internal")) {
261 Debug("register::internal") << toString() << std::endl
;
264 // Get the theories of the terms
265 TheoryId currentTheoryId
= Theory::theoryOf(current
);
266 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
268 // Should we use the theory of the type
269 bool useType
= false;
270 TheoryId typeTheoryId
= THEORY_LAST
;
272 if (current
!= parent
) {
273 if (currentTheoryId
!= parentTheoryId
) {
274 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
275 TypeNode type
= current
.getType();
277 typeTheoryId
= Theory::theoryOf(type
);
279 TypeNode type
= current
.getType();
280 typeTheoryId
= Theory::theoryOf(type
);
281 if (typeTheoryId
!= currentTheoryId
) {
282 if (type
.isInterpretedFinite()) {
289 Theory::Set visitedTheories
= d_visited
[current
];
290 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
291 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
292 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
293 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
295 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
296 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
297 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
300 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
301 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
302 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
305 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
307 // Record the new theories that we visited
308 d_visited
[current
] = visitedTheories
;
310 // If there is more than two theories and a new one has been added notify the shared terms database
311 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
312 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
315 Assert(d_visited
.find(current
) != d_visited
.end());
316 Assert(alreadyVisited(current
, parent
));
319 void SharedTermsVisitor::start(TNode node
) {
324 void SharedTermsVisitor::done(TNode node
) {
328 void SharedTermsVisitor::clear() {