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-2013 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 std::string
SharedTermsVisitor::toString() const {
131 std::stringstream ss
;
132 TNodeVisitedMap::const_iterator it
= d_visited
.begin();
133 for (; it
!= d_visited
.end(); ++ it
) {
134 ss
<< (*it
).first
<< ": " << Theory::setToString((*it
).second
) << std::endl
;
139 bool SharedTermsVisitor::alreadyVisited(TNode current
, TNode parent
) const {
141 Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current
<< "," << parent
<< ")" << std::endl
;
143 if( ( parent
.getKind() == kind::FORALL
||
144 parent
.getKind() == kind::EXISTS
||
145 parent
.getKind() == kind::REWRITE_RULE
/*||
146 parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
147 current
!= parent
) {
148 Debug("register::internal") << "quantifier:true" << std::endl
;
151 TNodeVisitedMap::const_iterator find
= d_visited
.find(current
);
153 // If node is not visited at all, just return false
154 if (find
== d_visited
.end()) {
155 Debug("register::internal") << "1:false" << std::endl
;
159 Theory::Set theories
= (*find
).second
;
161 TheoryId currentTheoryId
= Theory::theoryOf(current
);
162 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
164 // Should we use the theory of the type
165 bool useType
= false;
166 TheoryId typeTheoryId
= THEORY_LAST
;
168 if (current
!= parent
) {
169 if (currentTheoryId
!= parentTheoryId
) {
170 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
171 TypeNode type
= current
.getType();
173 typeTheoryId
= Theory::theoryOf(type
);
175 TypeNode type
= current
.getType();
176 typeTheoryId
= Theory::theoryOf(type
);
177 if (typeTheoryId
!= currentTheoryId
) {
178 if (options::finiteModelFind() && type
.isSort()) {
179 // We're looking for finite models
182 Cardinality card
= type
.getCardinality();
183 if (card
.isFinite()) {
191 if (Theory::setContains(currentTheoryId
, theories
)) {
192 if (Theory::setContains(parentTheoryId
, theories
)) {
194 return Theory::setContains(typeTheoryId
, theories
);
206 void SharedTermsVisitor::visit(TNode current
, TNode parent
) {
208 Debug("register") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< ")" << std::endl
;
209 if (Debug
.isOn("register::internal")) {
210 Debug("register::internal") << toString() << std::endl
;
213 // Get the theories of the terms
214 TheoryId currentTheoryId
= Theory::theoryOf(current
);
215 TheoryId parentTheoryId
= Theory::theoryOf(parent
);
217 // Should we use the theory of the type
218 bool useType
= false;
219 TheoryId typeTheoryId
= THEORY_LAST
;
221 if (current
!= parent
) {
222 if (currentTheoryId
!= parentTheoryId
) {
223 // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
224 TypeNode type
= current
.getType();
226 typeTheoryId
= Theory::theoryOf(type
);
228 TypeNode type
= current
.getType();
229 typeTheoryId
= Theory::theoryOf(type
);
230 if (typeTheoryId
!= currentTheoryId
) {
231 if (options::finiteModelFind() && type
.isSort()) {
232 // We're looking for finite models
235 Cardinality card
= type
.getCardinality();
236 if (card
.isFinite()) {
244 Theory::Set visitedTheories
= d_visited
[current
];
245 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): previously registered with " << Theory::setToString(visitedTheories
) << std::endl
;
246 if (!Theory::setContains(currentTheoryId
, visitedTheories
)) {
247 visitedTheories
= Theory::setInsert(currentTheoryId
, visitedTheories
);
248 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << currentTheoryId
<< std::endl
;
250 if (!Theory::setContains(parentTheoryId
, visitedTheories
)) {
251 visitedTheories
= Theory::setInsert(parentTheoryId
, visitedTheories
);
252 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << parentTheoryId
<< std::endl
;
255 if (!Theory::setContains(typeTheoryId
, visitedTheories
)) {
256 visitedTheories
= Theory::setInsert(typeTheoryId
, visitedTheories
);
257 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): adding " << typeTheoryId
<< std::endl
;
260 Debug("register::internal") << "SharedTermsVisitor::visit(" << current
<< "," << parent
<< "): now registered with " << Theory::setToString(visitedTheories
) << std::endl
;
262 // Record the new theories that we visited
263 d_visited
[current
] = visitedTheories
;
265 // If there is more than two theories and a new one has been added notify the shared terms database
266 if (Theory::setDifference(visitedTheories
, Theory::setInsert(currentTheoryId
))) {
267 d_sharedTerms
.addSharedTerm(d_atom
, current
, visitedTheories
);
270 Assert(d_visited
.find(current
) != d_visited
.end());
271 Assert(alreadyVisited(current
, parent
));
274 void SharedTermsVisitor::start(TNode node
) {
279 void SharedTermsVisitor::done(TNode node
) {
283 void SharedTermsVisitor::clear() {