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
.getKind() == kind::FORALL
|| parent
.getKind() == kind::EXISTS
39 || parent
.getKind() == kind::LAMBDA
40 || parent
.getKind() == kind::CHOICE
41 || parent
.getKind() == kind::REWRITE_RULE
42 || parent
.getKind() == kind::SEP_STAR
43 || parent
.getKind() == kind::SEP_WAND
44 || (parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean())
45 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
49 Debug("register::internal") << "quantifier:true" << std::endl
;
53 TheoryId currentTheoryId
= Theory::theoryOf(current
);
54 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
56 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
57 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
59 // Should we use the theory of the type
61 TheoryId typeTheoryId
= THEORY_LAST
;
63 if (current
!= parent
) {
64 if (currentTheoryId
!= parentTheoryId
) {
65 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
66 TypeNode type
= current
.getType();
68 typeTheoryId
= Theory::theoryOf(type
);
70 TypeNode type
= current
.getType();
71 typeTheoryId
= Theory::theoryOf(type
);
72 if (typeTheoryId
!= currentTheoryId
) {
73 if (type
.isInterpretedFinite()) {
80 // Get the theories that have already visited this node
81 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
82 if (find
== d_visited
.end()) {
84 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
89 Theory::Set visitedTheories
= (*find
).second
;
90 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
91 // The current theory has already visited it, so now it depends on the parent and the type
92 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
94 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
95 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
96 return Theory::setContains(typeTheoryId
, visitedTheories
);
108 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
110 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
111 if (Debug
.isOn("register::internal")) {
112 Debug("register::internal") << toString() << std::endl
;
115 // Get the theories of the terms
116 TheoryId currentTheoryId
= Theory::theoryOf(current
);
117 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
119 // Should we use the theory of the type
120 bool useType
= false;
121 TheoryId typeTheoryId
= THEORY_LAST
;
123 if (current
!= parent
) {
124 if (currentTheoryId
!= parentTheoryId
) {
125 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
126 TypeNode type
= current
.getType();
128 typeTheoryId
= Theory::theoryOf(type
);
130 TypeNode type
= current
.getType();
131 typeTheoryId
= Theory::theoryOf(type
);
132 if (typeTheoryId
!= currentTheoryId
) {
133 if (type
.isInterpretedFinite()) {
140 Theory::Set visitedTheories
= d_visited
[current
];
141 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
142 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
143 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
144 d_visited
[current
] = visitedTheories
;
145 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
146 th
->preRegisterTerm(current
);
147 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
149 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
150 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
151 d_visited
[current
] = visitedTheories
;
152 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
153 th
->preRegisterTerm(current
);
154 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
157 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
158 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
159 d_visited
[current
] = visitedTheories
;
160 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
161 th
->preRegisterTerm(current
);
162 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
165 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
167 Assert(d_visited
.find(current
) != d_visited
.end());
168 Assert(alreadyVisited(current
, parent
));
171 std::string
SharedTermsVisitor::toString() const {
172 std::stringstream ss
;
173 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
174 for (; it
!= d_visited
.end(); ++ it
) {
175 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
180 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
182 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
184 if ((parent
.getKind() == kind::FORALL
|| parent
.getKind() == kind::EXISTS
185 || parent
.getKind() == kind::LAMBDA
186 || parent
.getKind() == kind::CHOICE
187 || parent
.getKind() == kind::REWRITE_RULE
188 || parent
.getKind() == kind::SEP_STAR
189 || parent
.getKind() == kind::SEP_WAND
190 || (parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean())
191 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
193 && current
!= parent
)
195 Debug("register::internal") << "quantifier:true" << std::endl
;
198 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
200 // If node is not visited at all, just return false
201 if (find
== d_visited
.end()) {
202 Debug("register::internal") << "1:false" << std::endl
;
206 Theory::Set theories
= (*find
).second
;
208 TheoryId currentTheoryId
= Theory::theoryOf(current
);
209 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
211 // Should we use the theory of the type
212 bool useType
= false;
213 TheoryId typeTheoryId
= THEORY_LAST
;
215 if (current
!= parent
) {
216 if (currentTheoryId
!= parentTheoryId
) {
217 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
218 TypeNode type
= current
.getType();
220 typeTheoryId
= Theory::theoryOf(type
);
222 TypeNode type
= current
.getType();
223 typeTheoryId
= Theory::theoryOf(type
);
224 if (typeTheoryId
!= currentTheoryId
) {
225 if (type
.isInterpretedFinite()) {
231 if (current
!= parent
) {
232 if (currentTheoryId
!= parentTheoryId
) {
233 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
234 TypeNode type
= current
.getType();
236 typeTheoryId
= Theory::theoryOf(type
);
238 TypeNode type
= current
.getType();
239 typeTheoryId
= Theory::theoryOf(type
);
240 if (typeTheoryId
!= currentTheoryId
) {
241 if (type
.isInterpretedFinite()) {
248 if (Theory::setContains(currentTheoryId
, theories
)) {
249 if (Theory::setContains(parentTheoryId
, theories
)) {
251 return Theory::setContains(typeTheoryId
, theories
);
263 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
265 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
266 if (Debug
.isOn("register::internal")) {
267 Debug("register::internal") << toString() << std::endl
;
270 // Get the theories of the terms
271 TheoryId currentTheoryId
= Theory::theoryOf(current
);
272 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
274 // Should we use the theory of the type
275 bool useType
= false;
276 TheoryId typeTheoryId
= THEORY_LAST
;
278 if (current
!= parent
) {
279 if (currentTheoryId
!= parentTheoryId
) {
280 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
281 TypeNode type
= current
.getType();
283 typeTheoryId
= Theory::theoryOf(type
);
285 TypeNode type
= current
.getType();
286 typeTheoryId
= Theory::theoryOf(type
);
287 if (typeTheoryId
!= currentTheoryId
) {
288 if (type
.isInterpretedFinite()) {
295 Theory::Set visitedTheories
= d_visited
[current
];
296 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
297 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
298 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
299 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
301 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
302 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
303 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
306 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
307 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
308 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
311 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
313 // Record the new theories that we visited
314 d_visited
[current
] = visitedTheories
;
316 // If there is more than two theories and a new one has been added notify the shared terms database
317 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
318 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
321 Assert(d_visited
.find(current
) != d_visited
.end());
322 Assert(alreadyVisited(current
, parent
));
325 void SharedTermsVisitor::start(TNode node
) {
330 void SharedTermsVisitor::done(TNode node
) {
334 void SharedTermsVisitor::clear() {