1 /********************* */
2 /*! \file term_registration_visitor.cpp
4 ** Original author: Dejan Jovanovic
5 ** Major contributors: Andrew Reynolds
6 ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2014 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** [[ Add lengthier description here ]]
13 ** \todo document this file
16 #include "theory/term_registration_visitor.h"
17 #include "theory/theory_engine.h"
18 #include "theory/quantifiers/options.h"
22 using namespace theory
;
24 std::string
PreRegisterVisitor::toString() const {
26 TNodeToTheorySetMap::const_iterator it
= d_visited
.begin();
27 for (; it
!= d_visited
.end(); ++ it
) {
28 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
33 bool PreRegisterVisitor::alreadyVisited(TNode current
, TNode parent
) {
35 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
37 if( ( parent
.getKind() == kind::FORALL
||
38 parent
.getKind() == kind::EXISTS
||
39 parent
.getKind() == kind::REWRITE_RULE
/*||
40 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
42 Debug("register::internal") << "quantifier:true" << std::endl
;
46 TheoryId currentTheoryId
= Theory::theoryOf(current
);
47 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
49 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
50 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
52 // Should we use the theory of the type
54 TheoryId typeTheoryId
= THEORY_LAST
;
56 if (current
!= parent
) {
57 if (currentTheoryId
!= parentTheoryId
) {
58 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
59 TypeNode type
= current
.getType();
61 typeTheoryId
= Theory::theoryOf(type
);
63 TypeNode type
= current
.getType();
64 typeTheoryId
= Theory::theoryOf(type
);
65 if (typeTheoryId
!= currentTheoryId
) {
66 if (options::finiteModelFind() && type
.isSort()) {
67 // We're looking for finite models
70 Cardinality card
= type
.getCardinality();
71 if (card
.isFinite()) {
79 // Get the theories that have already visited this node
80 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
81 if (find
== d_visited
.end()) {
83 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
88 Theory::Set visitedTheories
= (*find
).second
;
89 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
90 // The current theory has already visited it, so now it depends on the parent and the type
91 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
93 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
94 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
95 return Theory::setContains(typeTheoryId
, visitedTheories
);
107 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
109 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
110 if (Debug
.isOn("register::internal")) {
111 Debug("register::internal") << toString() << std::endl
;
114 // Get the theories of the terms
115 TheoryId currentTheoryId
= Theory::theoryOf(current
);
116 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
118 // Should we use the theory of the type
119 bool useType
= false;
120 TheoryId typeTheoryId
= THEORY_LAST
;
122 if (current
!= parent
) {
123 if (currentTheoryId
!= parentTheoryId
) {
124 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
125 TypeNode type
= current
.getType();
127 typeTheoryId
= Theory::theoryOf(type
);
129 TypeNode type
= current
.getType();
130 typeTheoryId
= Theory::theoryOf(type
);
131 if (typeTheoryId
!= currentTheoryId
) {
132 if (options::finiteModelFind() && type
.isSort()) {
133 // We're looking for finite models
136 Cardinality card
= type
.getCardinality();
137 if (card
.isFinite()) {
145 Theory::Set visitedTheories
= d_visited
[current
];
146 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
147 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
148 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
149 d_visited
[current
] = visitedTheories
;
150 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
151 th
->preRegisterTerm(current
);
152 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
154 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
155 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
156 d_visited
[current
] = visitedTheories
;
157 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
158 th
->preRegisterTerm(current
);
159 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
162 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
163 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
164 d_visited
[current
] = visitedTheories
;
165 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
166 th
->preRegisterTerm(current
);
167 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
170 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
172 Assert(d_visited
.find(current
) != d_visited
.end());
173 Assert(alreadyVisited(current
, parent
));
176 std::string
SharedTermsVisitor::toString() const {
177 std::stringstream ss
;
178 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
179 for (; it
!= d_visited
.end(); ++ it
) {
180 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
185 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
187 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
189 if( ( parent
.getKind() == kind::FORALL
||
190 parent
.getKind() == kind::EXISTS
||
191 parent
.getKind() == kind::REWRITE_RULE
/*||
192 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
193 current
!= parent
) {
194 Debug("register::internal") << "quantifier:true" << std::endl
;
197 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
199 // If node is not visited at all, just return false
200 if (find
== d_visited
.end()) {
201 Debug("register::internal") << "1:false" << std::endl
;
205 Theory::Set theories
= (*find
).second
;
207 TheoryId currentTheoryId
= Theory::theoryOf(current
);
208 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
210 // Should we use the theory of the type
211 bool useType
= false;
212 TheoryId typeTheoryId
= THEORY_LAST
;
214 if (current
!= parent
) {
215 if (currentTheoryId
!= parentTheoryId
) {
216 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
217 TypeNode type
= current
.getType();
219 typeTheoryId
= Theory::theoryOf(type
);
221 TypeNode type
= current
.getType();
222 typeTheoryId
= Theory::theoryOf(type
);
223 if (typeTheoryId
!= currentTheoryId
) {
224 if (options::finiteModelFind() && type
.isSort()) {
225 // We're looking for finite models
228 Cardinality card
= type
.getCardinality();
229 if (card
.isFinite()) {
236 if (current
!= parent
) {
237 if (currentTheoryId
!= parentTheoryId
) {
238 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
239 TypeNode type
= current
.getType();
241 typeTheoryId
= Theory::theoryOf(type
);
243 TypeNode type
= current
.getType();
244 typeTheoryId
= Theory::theoryOf(type
);
245 if (typeTheoryId
!= currentTheoryId
) {
246 if (options::finiteModelFind() && type
.isSort()) {
247 // We're looking for finite models
250 Cardinality card
= type
.getCardinality();
251 if (card
.isFinite()) {
259 if (Theory::setContains(currentTheoryId
, theories
)) {
260 if (Theory::setContains(parentTheoryId
, theories
)) {
262 return Theory::setContains(typeTheoryId
, theories
);
274 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
276 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
277 if (Debug
.isOn("register::internal")) {
278 Debug("register::internal") << toString() << std::endl
;
281 // Get the theories of the terms
282 TheoryId currentTheoryId
= Theory::theoryOf(current
);
283 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
285 // Should we use the theory of the type
286 bool useType
= false;
287 TheoryId typeTheoryId
= THEORY_LAST
;
289 if (current
!= parent
) {
290 if (currentTheoryId
!= parentTheoryId
) {
291 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
292 TypeNode type
= current
.getType();
294 typeTheoryId
= Theory::theoryOf(type
);
296 TypeNode type
= current
.getType();
297 typeTheoryId
= Theory::theoryOf(type
);
298 if (typeTheoryId
!= currentTheoryId
) {
299 if (options::finiteModelFind() && type
.isSort()) {
300 // We're looking for finite models
303 Cardinality card
= type
.getCardinality();
304 if (card
.isFinite()) {
312 Theory::Set visitedTheories
= d_visited
[current
];
313 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
314 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
315 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
316 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
318 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
319 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
320 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
323 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
324 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
325 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
328 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
330 // Record the new theories that we visited
331 d_visited
[current
] = visitedTheories
;
333 // If there is more than two theories and a new one has been added notify the shared terms database
334 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
335 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
338 Assert(d_visited
.find(current
) != d_visited
.end());
339 Assert(alreadyVisited(current
, parent
));
342 void SharedTermsVisitor::start(TNode node
) {
347 void SharedTermsVisitor::done(TNode node
) {
351 void SharedTermsVisitor::clear() {