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-2016 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
||
39 parent
.getKind() == kind::EXISTS
||
40 parent
.getKind() == kind::REWRITE_RULE
||
41 parent
.getKind() == kind::SEP_STAR
||
42 parent
.getKind() == kind::SEP_WAND
||
43 ( parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean() )
44 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
47 Debug("register::internal") << "quantifier:true" << std::endl
;
51 TheoryId currentTheoryId
= Theory::theoryOf(current
);
52 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
54 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
55 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
57 // Should we use the theory of the type
59 TheoryId typeTheoryId
= THEORY_LAST
;
61 if (current
!= parent
) {
62 if (currentTheoryId
!= parentTheoryId
) {
63 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
64 TypeNode type
= current
.getType();
66 typeTheoryId
= Theory::theoryOf(type
);
68 TypeNode type
= current
.getType();
69 typeTheoryId
= Theory::theoryOf(type
);
70 if (typeTheoryId
!= currentTheoryId
) {
71 if (type
.isInterpretedFinite()) {
78 // Get the theories that have already visited this node
79 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
80 if (find
== d_visited
.end()) {
82 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
87 Theory::Set visitedTheories
= (*find
).second
;
88 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
89 // The current theory has already visited it, so now it depends on the parent and the type
90 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
92 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
93 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
94 return Theory::setContains(typeTheoryId
, visitedTheories
);
106 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
108 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
109 if (Debug
.isOn("register::internal")) {
110 Debug("register::internal") << toString() << std::endl
;
113 // Get the theories of the terms
114 TheoryId currentTheoryId
= Theory::theoryOf(current
);
115 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
117 // Should we use the theory of the type
118 bool useType
= false;
119 TheoryId typeTheoryId
= THEORY_LAST
;
121 if (current
!= parent
) {
122 if (currentTheoryId
!= parentTheoryId
) {
123 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
124 TypeNode type
= current
.getType();
126 typeTheoryId
= Theory::theoryOf(type
);
128 TypeNode type
= current
.getType();
129 typeTheoryId
= Theory::theoryOf(type
);
130 if (typeTheoryId
!= currentTheoryId
) {
131 if (type
.isInterpretedFinite()) {
138 Theory::Set visitedTheories
= d_visited
[current
];
139 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
140 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
141 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
142 d_visited
[current
] = visitedTheories
;
143 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
144 th
->preRegisterTerm(current
);
145 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
147 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
148 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
149 d_visited
[current
] = visitedTheories
;
150 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
151 th
->preRegisterTerm(current
);
152 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
155 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
156 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
157 d_visited
[current
] = visitedTheories
;
158 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
159 th
->preRegisterTerm(current
);
160 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
163 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
165 Assert(d_visited
.find(current
) != d_visited
.end());
166 Assert(alreadyVisited(current
, parent
));
169 std::string
SharedTermsVisitor::toString() const {
170 std::stringstream ss
;
171 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
172 for (; it
!= d_visited
.end(); ++ it
) {
173 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
178 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
180 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
182 if( ( parent
.getKind() == kind::FORALL
||
183 parent
.getKind() == kind::EXISTS
||
184 parent
.getKind() == kind::REWRITE_RULE
||
185 parent
.getKind() == kind::SEP_STAR
||
186 parent
.getKind() == kind::SEP_WAND
||
187 ( parent
.getKind() == kind::SEP_LABEL
&& current
.getType().isBoolean() )
188 // parent.getKind() == kind::CARDINALITY_CONSTRAINT
190 current
!= parent
) {
191 Debug("register::internal") << "quantifier:true" << std::endl
;
194 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
196 // If node is not visited at all, just return false
197 if (find
== d_visited
.end()) {
198 Debug("register::internal") << "1:false" << std::endl
;
202 Theory::Set theories
= (*find
).second
;
204 TheoryId currentTheoryId
= Theory::theoryOf(current
);
205 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
207 // Should we use the theory of the type
208 bool useType
= false;
209 TheoryId typeTheoryId
= THEORY_LAST
;
211 if (current
!= parent
) {
212 if (currentTheoryId
!= parentTheoryId
) {
213 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
214 TypeNode type
= current
.getType();
216 typeTheoryId
= Theory::theoryOf(type
);
218 TypeNode type
= current
.getType();
219 typeTheoryId
= Theory::theoryOf(type
);
220 if (typeTheoryId
!= currentTheoryId
) {
221 if (type
.isInterpretedFinite()) {
227 if (current
!= parent
) {
228 if (currentTheoryId
!= parentTheoryId
) {
229 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
230 TypeNode type
= current
.getType();
232 typeTheoryId
= Theory::theoryOf(type
);
234 TypeNode type
= current
.getType();
235 typeTheoryId
= Theory::theoryOf(type
);
236 if (typeTheoryId
!= currentTheoryId
) {
237 if (type
.isInterpretedFinite()) {
244 if (Theory::setContains(currentTheoryId
, theories
)) {
245 if (Theory::setContains(parentTheoryId
, theories
)) {
247 return Theory::setContains(typeTheoryId
, theories
);
259 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
261 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
262 if (Debug
.isOn("register::internal")) {
263 Debug("register::internal") << toString() << std::endl
;
266 // Get the theories of the terms
267 TheoryId currentTheoryId
= Theory::theoryOf(current
);
268 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
270 // Should we use the theory of the type
271 bool useType
= false;
272 TheoryId typeTheoryId
= THEORY_LAST
;
274 if (current
!= parent
) {
275 if (currentTheoryId
!= parentTheoryId
) {
276 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
277 TypeNode type
= current
.getType();
279 typeTheoryId
= Theory::theoryOf(type
);
281 TypeNode type
= current
.getType();
282 typeTheoryId
= Theory::theoryOf(type
);
283 if (typeTheoryId
!= currentTheoryId
) {
284 if (type
.isInterpretedFinite()) {
291 Theory::Set visitedTheories
= d_visited
[current
];
292 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
293 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
294 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
295 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
297 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
298 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
299 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
302 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
303 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
304 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
307 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
309 // Record the new theories that we visited
310 d_visited
[current
] = visitedTheories
;
312 // If there is more than two theories and a new one has been added notify the shared terms database
313 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
314 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
317 Assert(d_visited
.find(current
) != d_visited
.end());
318 Assert(alreadyVisited(current
, parent
));
321 void SharedTermsVisitor::start(TNode node
) {
326 void SharedTermsVisitor::done(TNode node
) {
330 void SharedTermsVisitor::clear() {