1 /********************* */
2 /*! \file term_registration_visitor.cpp
4 ** Original author: dejan
5 ** Major contributors: mdeters, ajreynol
6 ** Minor contributors (to current version): taking, barrett
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009-2012 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
53 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
55 // Get the theories that have already visited this node
56 TNodeToTheorySetMap::iterator find
= d_visited
.find(current
);
57 if (find
== d_visited
.end()) {
59 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
60 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
65 Theory::Set visitedTheories
= (*find
).second
;
66 if (Theory::setContains(currentTheoryId
, visitedTheories
)) {
67 // The current theory has already visited it, so now it depends on the parent and the type
68 if (Theory::setContains(parentTheoryId
, visitedTheories
)) {
70 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
71 d_theories
= Theory::setInsert(typeTheoryId
, d_theories
);
72 return Theory::setContains(typeTheoryId
, visitedTheories
);
84 void PreRegisterVisitor::visit(TNode current
, TNode parent
) {
86 Debug("register") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
87 if (Debug
.isOn("register::internal")) {
88 Debug("register::internal") << toString() << std::endl
;
91 // Get the theories of the terms
92 TheoryId currentTheoryId
= Theory::theoryOf(current
);
93 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
95 // Should we use the theory of the type
96 bool useType
= current
!= parent
&& currentTheoryId
!= parentTheoryId
;
98 Theory::Set visitedTheories
= d_visited
[current
];
99 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
100 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
101 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
102 d_visited
[current
] = visitedTheories
;
103 Theory
* th
= d_engine
->theoryOf(currentTheoryId
);
104 th
->preRegisterTerm(current
);
105 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
107 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
108 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
109 d_visited
[current
] = visitedTheories
;
110 Theory
* th
= d_engine
->theoryOf(parentTheoryId
);
111 th
->preRegisterTerm(current
);
112 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
115 TheoryId typeTheoryId
= Theory::theoryOf(current
.getType());
116 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
117 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
118 d_visited
[current
] = visitedTheories
;
119 Theory
* th
= d_engine
->theoryOf(typeTheoryId
);
120 th
->preRegisterTerm(current
);
121 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
124 Debug("register::internal") << "PreRegisterVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
126 Assert(d_visited
.find(current
) != d_visited
.end());
127 Assert(alreadyVisited(current
, parent
));
130 void PreRegisterVisitor::start(TNode node
) {
131 d_multipleTheories
= false;
134 bool PreRegisterVisitor::done(TNode node
) {
135 // We have multiple theories if removing the node theory from others is non-empty
136 return Theory::setRemove(Theory::theoryOf(node
), d_theories
);
139 std::string
SharedTermsVisitor::toString() const {
140 std::stringstream ss
;
141 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
142 for (; it
!= d_visited
.end(); ++ it
) {
143 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
148 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
150 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
152 if( ( parent
.getKind() == kind::FORALL
||
153 parent
.getKind() == kind::EXISTS
||
154 parent
.getKind() == kind::REWRITE_RULE
/*||
155 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
156 current
!= parent
) {
157 Debug("register::internal") << "quantifier:true" << std::endl
;
160 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
162 // If node is not visited at all, just return false
163 if (find
== d_visited
.end()) {
164 Debug("register::internal") << "1:false" << std::endl
;
168 Theory::Set theories
= (*find
).second
;
170 TheoryId currentTheoryId
= Theory::theoryOf(current
);
171 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
173 // Should we use the theory of the type
174 bool useType
= false;
175 TheoryId typeTheoryId
= THEORY_LAST
;
177 if (current
!= parent
) {
178 if (currentTheoryId
!= parentTheoryId
) {
179 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
180 TypeNode type
= current
.getType();
182 typeTheoryId
= Theory::theoryOf(type
);
184 TypeNode type
= current
.getType();
185 typeTheoryId
= Theory::theoryOf(type
);
186 if (typeTheoryId
!= currentTheoryId
) {
187 if (options::finiteModelFind() && type
.isSort()) {
188 // We're looking for finite models
191 Cardinality card
= type
.getCardinality();
192 if (card
.isFinite()) {
200 if (Theory::setContains(currentTheoryId
, theories
)) {
201 if (Theory::setContains(parentTheoryId
, theories
)) {
203 return Theory::setContains(typeTheoryId
, theories
);
215 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
217 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
218 if (Debug
.isOn("register::internal")) {
219 Debug("register::internal") << toString() << std::endl
;
222 // Get the theories of the terms
223 TheoryId currentTheoryId
= Theory::theoryOf(current
);
224 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
226 // Should we use the theory of the type
227 bool useType
= false;
228 TheoryId typeTheoryId
= THEORY_LAST
;
230 if (current
!= parent
) {
231 if (currentTheoryId
!= parentTheoryId
) {
232 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
233 TypeNode type
= current
.getType();
235 typeTheoryId
= Theory::theoryOf(type
);
237 TypeNode type
= current
.getType();
238 typeTheoryId
= Theory::theoryOf(type
);
239 if (typeTheoryId
!= currentTheoryId
) {
240 if (options::finiteModelFind() && type
.isSort()) {
241 // We're looking for finite models
244 Cardinality card
= type
.getCardinality();
245 if (card
.isFinite()) {
253 Theory::Set visitedTheories
= d_visited
[current
];
254 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
255 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
256 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
257 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
259 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
260 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
261 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
264 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
265 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
266 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
269 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
271 // Record the new theories that we visited
272 d_visited
[current
] = visitedTheories
;
274 // If there is more than two theories and a new one has been added notify the shared terms database
275 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
276 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
279 Assert(d_visited
.find(current
) != d_visited
.end());
280 Assert(alreadyVisited(current
, parent
));
283 void SharedTermsVisitor::start(TNode node
) {
288 void SharedTermsVisitor::done(TNode node
) {
292 void SharedTermsVisitor::clear() {