1 /********************* */
2 /*! \file term_registration_visitor.cpp
4 ** Original author: dejan
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): taking, barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/term_registration_visitor.h"
19 #include "theory/theory_engine.h"
20 #include "theory/quantifiers/options.h"
24 using namespace theory
;
26 std::string
PreRegisterVisitor::toString() const {
28 TNodeToTheorySetMap::const_iterator it
= d_visited
.begin();
29 for (; it
!= d_visited
.end(); ++ it
) {
30 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
35 bool PreRegisterVisitor::alreadyVisited(TNode current
, TNode parent
) {
37 Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
39 if( ( parent
.getKind() == kind::FORALL
||
40 parent
.getKind() == kind::EXISTS
||
41 parent
.getKind() == kind::REWRITE_RULE
/*||
42 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
44 Debug("register::internal") << "quantifier:true" << std::endl
;
48 TheoryId currentTheoryId
= Theory::theoryOf(current
);
49 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
51 d_theories
= Theory::setInsert(currentTheoryId
, d_theories
);
52 d_theories
= Theory::setInsert(parentTheoryId
, d_theories
);
54 // Should we use the theory of the type
55 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
57 // Get the theories that have already visited this node
58 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
59 if (find
== d_visited
.end()) {
61 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
62 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
67 Theory::Set visitedTheories
= (*find
).second
;
68 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
69 // The current theory has already visited it, so now it depends on the parent and the type
70 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
72 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
73 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
74 return Theory::setContains(typeTheoryId
, visitedTheories
);
86 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
88 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
89 if (Debug
.isOn("register::internal")) {
90 Debug("register::internal") << toString() << std::endl
;
93 // Get the theories of the terms
94 TheoryId currentTheoryId
= Theory::theoryOf(current
);
95 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
97 // Should we use the theory of the type
98 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
100 Theory::Set visitedTheories
= d_visited
[current
];
101 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
102 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
103 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
104 d_visited
[current
] = visitedTheories
;
105 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
106 th
->preRegisterTerm(current
);
107 if(th
->getInstantiator() != NULL
) {
108 th
->getInstantiator()->preRegisterTerm(current
);
110 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
112 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
113 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
114 d_visited
[current
] = visitedTheories
;
115 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
116 th
->preRegisterTerm(current
);
117 if(th
->getInstantiator() != NULL
) {
118 th
->getInstantiator()->preRegisterTerm(current
);
120 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
123 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
124 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
125 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
126 d_visited
[current
] = visitedTheories
;
127 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
128 th
->preRegisterTerm(current
);
129 if(th
->getInstantiator() != NULL
) {
130 th
->getInstantiator()->preRegisterTerm(current
);
132 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
135 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
137 Assert(d_visited
.find(current
) != d_visited
.end());
138 Assert(alreadyVisited(current
, parent
));
141 void PreRegisterVisitor::start(TNode node
) {
142 d_multipleTheories
= false;
145 bool PreRegisterVisitor::done(TNode node
) {
146 // We have multiple theories if removing the node theory from others is non-empty
147 return Theory::setRemove(Theory::theoryOf(node
), d_theories
);
150 std::string
SharedTermsVisitor::toString() const {
151 std::stringstream ss
;
152 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
153 for (; it
!= d_visited
.end(); ++ it
) {
154 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
159 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
161 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
163 if( ( parent
.getKind() == kind::FORALL
||
164 parent
.getKind() == kind::EXISTS
||
165 parent
.getKind() == kind::REWRITE_RULE
/*||
166 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
167 current
!= parent
) {
168 Debug("register::internal") << "quantifier:true" << std::endl
;
171 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
173 // If node is not visited at all, just return false
174 if (find
== d_visited
.end()) {
175 Debug("register::internal") << "1:false" << std::endl
;
179 Theory::Set theories
= (*find
).second
;
181 TheoryId currentTheoryId
= Theory::theoryOf(current
);
182 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
184 // Should we use the theory of the type
186 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
188 bool useType
= false;
189 TheoryId typeTheoryId
= THEORY_LAST
;
191 if (current
!= parent
) {
192 if (currentTheoryId
!= parentTheoryId
) {
193 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
194 TypeNode type
= current
.getType();
196 typeTheoryId
= Theory::theoryOf(type
);
198 TypeNode type
= current
.getType();
199 typeTheoryId
= Theory::theoryOf(type
);
200 if (typeTheoryId
!= currentTheoryId
) {
201 if (options::finiteModelFind() && type
.isSort()) {
202 // We're looking for finite models
205 Cardinality card
= type
.getCardinality();
206 if (card
.isFinite()) {
215 if (Theory::setContains(currentTheoryId
, theories
)) {
216 if (Theory::setContains(parentTheoryId
, theories
)) {
218 ////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
219 return Theory::setContains(typeTheoryId
, theories
);
231 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
233 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
234 if (Debug
.isOn("register::internal")) {
235 Debug("register::internal") << toString() << std::endl
;
238 // Get the theories of the terms
239 TheoryId currentTheoryId
= Theory::theoryOf(current
);
240 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
243 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
245 // Should we use the theory of the type
246 bool useType
= false;
247 TheoryId typeTheoryId
= THEORY_LAST
;
249 if (current
!= parent
) {
250 if (currentTheoryId
!= parentTheoryId
) {
251 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
252 TypeNode type
= current
.getType();
254 typeTheoryId
= Theory::theoryOf(type
);
256 TypeNode type
= current
.getType();
257 typeTheoryId
= Theory::theoryOf(type
);
258 if (typeTheoryId
!= currentTheoryId
) {
259 if (options::finiteModelFind() && type
.isSort()) {
260 // We're looking for finite models
263 Cardinality card
= type
.getCardinality();
264 if (card
.isFinite()) {
273 Theory::Set visitedTheories
= d_visited
[current
];
274 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
275 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
276 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
277 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
279 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
280 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
281 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
284 //////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
285 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
286 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
287 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
290 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
292 // Record the new theories that we visited
293 d_visited
[current
] = visitedTheories
;
295 // If there is more than two theories and a new one has been added notify the shared terms database
296 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
297 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
300 Assert(d_visited
.find(current
) != d_visited
.end());
301 Assert(alreadyVisited(current
, parent
));
304 void SharedTermsVisitor::start(TNode node
) {
309 void SharedTermsVisitor::done(TNode node
) {
313 void SharedTermsVisitor::clear() {